Module SharedFunctions.AssertionModule

Parameters

module V : SV
module AD : AssertionRelS
module Arg : ConvertArg

Signature

include module type of struct include AD end
type t = AD.t
module Bounds = AD.Bounds
val is_bot_env : t -> bool
val assert_constraint : Queries.ask -> t -> GoblintCil.exp -> bool -> bool Stdlib.Lazy.t -> t
val eval_interval : Queries.ask -> t -> GobApron.Texpr1.t -> Z.t option * Z.t option
type nonrec var = V.t
module Tracked = Tracked
module Convert : sig ... end
val exp_is_constraint : GoblintCil.exp -> bool
val assert_inv : Queries.ask -> t -> GoblintCil.exp -> bool -> bool Stdlib.Lazy.t -> t

Assert any expression.

val check_assert : Queries.ask -> t -> GoblintCil.exp -> bool Stdlib.Lazy.t -> [> `False | `Top | `True ]
val eval_interval_expr : Queries.ask -> Bounds.t -> GoblintCil.Cil.exp -> bool Stdlib.Lazy.t -> Z.t option * Z.t option

Evaluate non-constraint expression as interval.

val eval_int : Queries.ask -> t -> GoblintCil.exp -> bool Stdlib.Lazy.t -> [> `Lifted of IntDomain.IntDomTuple.t | `Top ]

Evaluate constraint or non-constraint expression as integer.