sig
module M : Model
type loc = M.loc
type nonrec value = Sigs.CodeSemantics.loc Sigs.value
type nonrec result = Sigs.CodeSemantics.loc Sigs.result
type sigma = M.Sigma.t
val pp_value : Format.formatter -> Sigs.CodeSemantics.value -> unit
val cval : Sigs.CodeSemantics.value -> Lang.F.term
val cloc : Sigs.CodeSemantics.value -> Sigs.CodeSemantics.loc
val cast :
Cil_types.typ ->
Cil_types.typ -> Sigs.CodeSemantics.value -> Sigs.CodeSemantics.value
val equal_typ :
Cil_types.typ ->
Sigs.CodeSemantics.value -> Sigs.CodeSemantics.value -> Lang.F.pred
val not_equal_typ :
Cil_types.typ ->
Sigs.CodeSemantics.value -> Sigs.CodeSemantics.value -> Lang.F.pred
val equal_obj :
Ctypes.c_object ->
Sigs.CodeSemantics.value -> Sigs.CodeSemantics.value -> Lang.F.pred
val not_equal_obj :
Ctypes.c_object ->
Sigs.CodeSemantics.value -> Sigs.CodeSemantics.value -> Lang.F.pred
val exp :
Sigs.CodeSemantics.sigma -> Cil_types.exp -> Sigs.CodeSemantics.value
val cond : Sigs.CodeSemantics.sigma -> Cil_types.exp -> Lang.F.pred
val lval :
Sigs.CodeSemantics.sigma -> Cil_types.lval -> Sigs.CodeSemantics.loc
val call :
Sigs.CodeSemantics.sigma -> Cil_types.exp -> Sigs.CodeSemantics.loc
val instance_of :
Sigs.CodeSemantics.loc -> Cil_types.kernel_function -> Lang.F.pred
val loc_of_exp :
Sigs.CodeSemantics.sigma -> Cil_types.exp -> Sigs.CodeSemantics.loc
val val_of_exp : Sigs.CodeSemantics.sigma -> Cil_types.exp -> Lang.F.term
val result :
Sigs.CodeSemantics.sigma ->
Cil_types.typ -> Sigs.CodeSemantics.result -> Lang.F.term
val return :
Sigs.CodeSemantics.sigma -> Cil_types.typ -> Cil_types.exp -> Lang.F.term
val is_zero :
Sigs.CodeSemantics.sigma ->
Ctypes.c_object -> Sigs.CodeSemantics.loc -> Lang.F.pred
val is_exp_range :
Sigs.CodeSemantics.sigma ->
Sigs.CodeSemantics.loc ->
Ctypes.c_object ->
Lang.F.term ->
Lang.F.term -> Sigs.CodeSemantics.value option -> Lang.F.pred
val unchanged : M.sigma -> M.sigma -> Cil_types.varinfo -> Lang.F.pred
type warned_hyp = Warning.Set.t * Lang.F.pred
val init :
sigma:M.sigma ->
Cil_types.varinfo ->
Cil_types.init option -> Sigs.CodeSemantics.warned_hyp list
end