Cvalues (p.frama-c.28.0.doc.frama-c-wp.core.Wp.Cvalues)

frama-c
- README
- Library Pdg_types
  - Pdg_types
- Library frama-c-alias.core
  - Alias
- Library frama-c-aorai.core
  - Aorai
- Library frama-c-api-generator.core
  - Api_generator
- Library frama-c-callgraph.core
  - Callgraph
- Library frama-c-constant_propagation.core
  - Constant_Propagation
- Library frama-c-dive.core
  - Dive
- Library frama-c-e-acsl.core
  - E_ACSL
- Library frama-c-eva.core
  - Eva
- Library frama-c-eva.gui
  - Eva_gui
- Library frama-c-from.core
  - From
- Library frama-c-from.gui
  - From_gui
- Library frama-c-impact.core
  - Impact
- Library frama-c-impact.gui
  - Impact_gui
- Library frama-c-inout.core
  - Inout
- Library frama-c-instantiate.core
  - Instantiate
- Library frama-c-loop-analysis.core
  - LoopAnalysis
- Library frama-c-markdown-report.core
  - Markdown_report
- Library frama-c-markdown-report.eva-info
- Library frama-c-metrics.core
  - Metrics
- Library frama-c-metrics.gui
  - Metrics_gui
- Library frama-c-nonterm.core
  - Nonterm
- Library frama-c-obfuscator.core
  - Obfuscator
- Library frama-c-occurrence.core
  - Occurrence
- Library frama-c-occurrence.gui
  - Occurrence_gui
- Library frama-c-pdg.core
  - Pdg
- Library frama-c-pdg.types
- Library frama-c-postdominators.core
  - Postdominators
- Library frama-c-reduc.core
  - Reduc
- Library frama-c-report.core
  - Report
- Library frama-c-rtegen.core
  - RteGen
- Library frama-c-rtegen.gui
  - Rtegen_gui
- Library frama-c-scope.core
  - Scope
- Library frama-c-scope.gui
  - Scope_gui
- Library frama-c-security_slicing.core
  - Security_slicing
- Library frama-c-security_slicing.gui
  - Security_slicing_gui
- Library frama-c-server.core
  - Server
- Library frama-c-slicing.core
  - Slicing
- Library frama-c-slicing.gui
  - Slicing_gui
- Library frama-c-sparecode.core
  - Sparecode
- Library frama-c-studia.core
  - Studia
- Library frama-c-studia.gui
  - Studia_gui
- Library frama-c-users.core
  - Users
- Library frama-c-variadic.core
  - Variadic
- Library frama-c-wp.core
  - Wp
- Library frama-c-wp.gui
  - Wp_gui
- Library frama-c.analysis-scripts
  - Analysis_scripts
- Library frama-c.boot
  - Frama_c_boot
- Library frama-c.gui
  - Frama_c_gui
- Library frama-c.init
- Library frama-c.kernel
  - Frama_c_kernel
- Library frama_c_very_first_cmdline
- Library frama_c_very_first_gui
- Library markdown_report_eva_info
  - Markdown_report_eva_info
- Library qed
  - Qed
- Sources

Sourceval equation : Sigs.equation -> Lang.F.pred

Pretty Printing

Sourcetype 'a printer = Format.formatter -> 'a -> unit

Sourceval pp_acs : Sigs.acs printer

Sourceval pp_bound : Lang.F.term option printer

Sourceval pp_value : 'a printer -> 'a Sigs.value printer

Sourceval pp_logic : 'a printer -> 'a Sigs.logic printer

Sourceval pp_region : 'a printer -> 'a Sigs.region printer

Sourceval pp_sloc : 'a printer -> 'a Sigs.sloc printer

Sourceval pp_rloc : 'a printer -> 'a Sigs.rloc printer

Int-As-Booleans

Sourceval bool_val : Lang.F.unop

Sourceval bool_eq : Lang.F.binop

Sourceval bool_lt : Lang.F.binop

Sourceval bool_neq : Lang.F.binop

Sourceval bool_leq : Lang.F.binop

Sourceval bool_and : Lang.F.binop

Sourceval bool_or : Lang.F.binop

Sourceval is_true : Lang.F.pred -> Lang.F.term

p ? 1 : 0

Sourceval is_false : Lang.F.pred -> Lang.F.term

p ? 0 : 1

Null Values

Sourceval null : (Lang.F.term -> Lang.F.pred) Context.value

test for null pointer value

Sourceval is_null : Ctypes.c_object -> Lang.F.term -> Lang.F.pred

Start of Arrays

Source

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

Sourceval is_object : Ctypes.c_object -> 'a Sigs.value -> Lang.F.pred

Sourceval has_ctype : Frama_c_kernel.Cil_types.typ -> Lang.F.term -> Lang.F.pred

Sourceval cdomain : Ctypes.c_object -> (Lang.F.term -> Lang.F.pred) option

Source

val ldomain : 
  Frama_c_kernel.Cil_types.logic_type ->
  (Lang.F.term -> Lang.F.pred) option

Volatile Access

Sourceval 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

Sourcetype matrixinfo = Ctypes.c_object * int option list

Sourceval equal_object : Ctypes.c_object -> Lang.F.term -> Lang.F.term -> Lang.F.pred

Source

val equal_comp : 
  Frama_c_kernel.Cil_types.compinfo ->
  Lang.F.term ->
  Lang.F.term ->
  Lang.F.pred

Sourceval equal_array : matrixinfo -> Lang.F.term -> Lang.F.term -> Lang.F.pred

C and ACSL Constants

Sourceval ainf : Lang.F.term option

Array lower-bound, ie `Some(0)`

Sourceval asup : int -> Lang.F.term option

Array upper-bound, ie `Some(n-1)`

Sourceval constant : Frama_c_kernel.Cil_types.constant -> Lang.F.term

Sourceval logic_constant : Frama_c_kernel.Cil_types.logic_constant -> Lang.F.term

Sourceval constant_exp : Frama_c_kernel.Cil_types.exp -> Lang.F.term

Sourceval constant_term : Frama_c_kernel.Cil_types.term -> Lang.F.term

Sourceval always_initialized : Frama_c_kernel.Cil_types.varinfo -> bool

Sourceval initialized_obj : Ctypes.c_object -> Lang.F.term

Sourceval uninitialized_obj : Ctypes.c_object -> Lang.F.term

Source

val bytes_length_of_opaque_comp : 
  Frama_c_kernel.Cil_types.compinfo ->
  Lang.F.term

Lifting Operations over Memory Values

Sourceval map_sloc : ('a -> 'b) -> 'a Sigs.sloc -> 'b Sigs.sloc

Sourceval map_value : ('a -> 'b) -> 'a Sigs.value -> 'b Sigs.value

Sourceval map_logic : ('a -> 'b) -> 'a Sigs.logic -> 'b Sigs.logic

Sourceval plain : Frama_c_kernel.Cil_types.logic_type -> Lang.F.term -> 'a Sigs.logic

ACSL Utilities

Sourcetype polarity = [

| `Positive
| `Negative
| `NoPolarity

]

positive goal negative hypothesis

Sourceval negate : polarity -> polarity

Sourcemodule Logic (M : Sigs.Model) : sig ... end