Module SharedFunctions.CilOfApron

Conversion from Apron to CIL expressions.

Parameters

module V : SV

Signature

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

Returned boolean indicates whether returned expression should be negated.

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

Returned boolean indicates whether returned expression should be negated.

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

Returned booleans indicates whether returned expressions should be negated.

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