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