Convert (goblint.Goblint_lib.SharedFunctions.Convert)

Parameters

module V : SV

module Bounds : ConvBounds

module Arg : ConvertArg

module Tracked : RelationDomain.Tracked

Signature

include sig ... end

exception Unsupported_CilExp of unsupported_cilExp

val overflow_handling : 
  bool Stdlib.Lazy.t ->
  'a ->
  Apron.Environment.t ->
  GobApron.Texpr1.expr ->
  Bounds.t ->
  GoblintCil.exp ->
  unit

val texpr1_expr_of_cil_exp : 
  Queries.ask ->
  Bounds.t ->
  GobApron.Environment.t ->
  GoblintCil.Cil.exp ->
  bool Stdlib.Lazy.t ->
  GobApron.Texpr1.expr

val texpr1_of_cil_exp : 
  Queries.ask ->
  Bounds.t ->
  GobApron.Environment.t ->
  GoblintCil.Cil.exp ->
  bool Stdlib.Lazy.t ->
  GobApron.Texpr1.t

val tcons1_of_cil_exp : 
  Queries.ask ->
  Bounds.t ->
  GobApron.Environment.t ->
  GoblintCil.Cil.exp ->
  bool ->
  bool Stdlib.Lazy.t ->
  GobApron.Tcons1.t

include sig ... end

exception Unsupported_Linexpr1

val longlong : GoblintCil.typ

val coeff_to_const : 
  scalewith:Z.t option ->
  GobApron.Coeff.union_5 ->
  bool * GoblintCil.exp

val cil_exp_of_linexpr1_term : 
  scalewith:Z.t option ->
  GobApron.Coeff.t ->
  V.t ->
  bool * GoblintCil.exp

val cil_exp_of_linexpr1 : 
  ?scalewith:Z.t ->
  GobApron.Linexpr1.t ->
  (bool * GoblintCil.exp) list

val lcm_den : GobApron.Linexpr1.t -> Z.t

val cil_exp_of_lincons1 : GobApron.Lincons1.t -> GoblintCil.Cil.exp option