package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
val equation : Sigs.equation -> Lang.F.pred

Pretty Printing

type 'a printer = Format.formatter -> 'a -> unit
val pp_acs : Sigs.acs printer
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 pp_sloc : 'a printer -> 'a Sigs.sloc printer
val pp_rloc : 'a printer -> 'a Sigs.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

test for null pointer value

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 Sigs.value -> Lang.F.pred
val cdomain : Ctypes.c_object -> (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_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 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 Sigs.sloc -> 'b Sigs.sloc
val map_value : ('a -> 'b) -> 'a Sigs.value -> 'b Sigs.value
val map_logic : ('a -> 'b) -> 'a Sigs.logic -> 'b Sigs.logic

ACSL Utilities

type polarity = [
  1. | `Positive
  2. | `Negative
  3. | `NoPolarity
]

positive goal negative hypothesis

val negate : polarity -> polarity
module Logic (M : Sigs.Model) : sig ... end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct