Module SharedFunctions.ApronOfCil

Conversion from CIL expressions to Apron. This is used by the domains "affine equalities" and "linear two variable equalities". It also handles the overflow through the flag "no_ov". For this reason it was divided from the Convert module for the pure apron domains "ApronOfCilForApronDomains",

Parameters

module V : SV
module Arg : ConvertArg

Signature

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

This still tries to establish bounds via Bounds.bound_texpr, which may be more precise in case ana.int.interval is disabled and the relational analysis manages to evaluate a value to an interval, which can then not be represented as the result of an EvalInt query. This is a workaround and works as long as only one relational domain is used. With multiple domains and disabled interval domain, the queries will not be able to exchange interval information, and each analysis will only be able to establish constant bounds, but only its own interval bounds and not interval bounds established by other analyses.

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