Wp.Cvalues
val equation : Sigs.equation -> Lang.F.pred
val pp_bound : Lang.F.term option printer
val pp_value : 'a printer -> 'a Sigs.value printer
val pp_logic : 'a printer -> 'a Sigs.logic printer
val pp_region : 'a printer -> 'a Sigs.region printer
val bool_val : Lang.F.unop
val bool_eq : Lang.F.binop
val bool_lt : Lang.F.binop
val bool_neq : Lang.F.binop
val bool_leq : Lang.F.binop
val bool_and : Lang.F.binop
val bool_or : Lang.F.binop
val is_true : Lang.F.pred -> Lang.F.term
p ? 1 : 0
val is_false : Lang.F.pred -> Lang.F.term
p ? 0 : 1
val null : ( Lang.F.term -> Lang.F.pred ) Context.value
test for null pointer value
val is_null : Ctypes.c_object -> Lang.F.term -> Lang.F.pred
val startof :
shift:( 'a -> Ctypes.c_object -> Lang.F.term -> 'a ) ->
'a ->
Frama_c_kernel.Cil_types.typ ->
'a
Shift a location with 0-indices wrt to its array type
val is_object : Ctypes.c_object -> 'a Sigs.value -> Lang.F.pred
val has_ctype : Frama_c_kernel.Cil_types.typ -> Lang.F.term -> Lang.F.pred
val cdomain : Ctypes.c_object -> ( Lang.F.term -> Lang.F.pred ) option
val ldomain :
Frama_c_kernel.Cil_types.logic_type ->
( Lang.F.term -> Lang.F.pred ) option
Check if a volatile access must be properly modelled or ignored. In case the volatile attribute comes to be ignored, the provided warning is emitted, if any.
type matrixinfo = Ctypes.c_object * int option list
val equal_object : Ctypes.c_object -> Lang.F.term -> Lang.F.term -> Lang.F.pred
val equal_comp :
Frama_c_kernel.Cil_types.compinfo ->
Lang.F.term ->
Lang.F.term ->
Lang.F.pred
val equal_array : matrixinfo -> Lang.F.term -> Lang.F.term -> Lang.F.pred
val ainf : Lang.F.term option
Array lower-bound, ie `Some(0)`
val asup : int -> Lang.F.term option
Array upper-bound, ie `Some(n-1)`
val constant : Frama_c_kernel.Cil_types.constant -> Lang.F.term
val logic_constant : Frama_c_kernel.Cil_types.logic_constant -> Lang.F.term
val constant_exp : Frama_c_kernel.Cil_types.exp -> Lang.F.term
val constant_term : Frama_c_kernel.Cil_types.term -> Lang.F.term
val always_initialized : Frama_c_kernel.Cil_types.varinfo -> bool
val initialized_obj : Ctypes.c_object -> Lang.F.term
val uninitialized_obj : Ctypes.c_object -> Lang.F.term
val bytes_length_of_opaque_comp :
Frama_c_kernel.Cil_types.compinfo ->
Lang.F.term
val map_value : ( 'a -> 'b ) -> 'a Sigs.value -> 'b Sigs.value
val map_logic : ( 'a -> 'b ) -> 'a Sigs.logic -> 'b Sigs.logic
val plain : Frama_c_kernel.Cil_types.logic_type -> Lang.F.term -> 'a Sigs.logic
module Logic (M : Sigs.Model) : sig ... end