package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

Utilities for E-ACSL.

Handling \result

  • returns

    the lhost corresponding to \result in the given function

  • returns

    the varinfo corresponding to \result in the given function

Other stuff

val is_fc_or_compiler_builtin : Frama_c_kernel.Cil_types.varinfo -> bool
val is_fc_stdlib_generated : Frama_c_kernel.Cil_types.varinfo -> bool

Returns true if the varinfo is a generated stdlib function. (For instance generated function by the Variadic plug-in.

Assume that the logic type is indeed a C type. Just return it.

Takes an expression e and return base where base is the address p if e is of the form p + i and e otherwise.

term_of_li li assumes that li.l_body matches LBterm t and returns t.

val is_set_of_ptr_or_array : Frama_c_kernel.Cil_types.logic_type -> bool

Checks whether the given logic type is a set of pointers.

val is_range_free : Frama_c_kernel.Cil_types.term -> bool
  • returns

    true iff the given term does not contain any range.

val is_bitfield_pointers : Frama_c_kernel.Cil_types.logic_type -> bool
  • returns

    true iff the given logic type is a bitfield pointer or a set of bitfield pointers.

val term_has_lv_from_vi : Frama_c_kernel.Cil_types.term -> bool
  • returns

    true iff the given term contains a variables that originates from a C varinfo, that is a non-purely logic variable.

val name_of_binop : Frama_c_kernel.Cil_types.binop -> string
  • returns

    the name of the given binop as a string.

finite_min_and_max i takes the finite ival i and returns its bounds.

Datatype for terms that relies on physical equality. Note that of its collections only Hashtbl can be used. Using Map and Set raises a fatal error as they require a comparison function, which cannot be defined in a sound way for physical equality.

val extract_uncoerced_lval : Frama_c_kernel.Cil_types.exp -> Frama_c_kernel.Cil_types.exp option

Unroll the CastE part of the expression until an Lval is found, and return it.

If at some point the expression is neither a CastE nor an Lval, then return None.

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