Cvalues (frama-c-wp.Wp.Cvalues)

val equation : Memory.equation -> Lang.F.pred

Pretty Printing

type 'a printer = Stdlib.Format.formatter -> 'a -> unit

val pp_acs : Memory.acs printer

val pp_bound : Lang.F.term option printer

val pp_value : 'a printer -> 'a Memory.value printer

val pp_logic : 'a printer -> 'a Memory.logic printer

val pp_region : 'a printer -> 'a Memory.region printer

val pp_sloc : 'a printer -> 'a Memory.sloc printer

val pp_rloc : 'a printer -> 'a Memory.rloc printer

Int-As-Booleans

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

Null Values

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

Start of Arrays

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

Typing and Sub-Typing for C and ACSL Types

val is_object : Ctypes.c_object -> 'a Memory.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

Volatile Access

val volatile : ?warn:string -> unit -> bool

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.

ACSL Equality

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

C and ACSL Constants

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

Lifting Operations over Memory Values

val map_sloc : ('a -> 'b) -> 'a Memory.sloc -> 'b Memory.sloc

val map_value : ('a -> 'b) -> 'a Memory.value -> 'b Memory.value

val map_logic : ('a -> 'b) -> 'a Memory.logic -> 'b Memory.logic

val plain : 
  Frama_c_kernel.Cil_types.logic_type ->
  Lang.F.term ->
  'a Memory.logic

ACSL Utilities

type polarity = [

| `Positive
| `Negative
| `NoPolarity

]

positive goal negative hypothesis

val negate : polarity -> polarity

module Logic (M : Memory.Model) : sig ... end