package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

Dune Dependency

frama-c.com Readme Edit opam file Versions (23)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

doc/frama-c-e-acsl.core/E_ACSL/Misc/index.html

Module `E_ACSL.Misc`

Utilities for E-ACSL.

Handling \result

val result_lhost : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.lhost

returns
the lhost corresponding to \result in the given function

val result_vi : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Cil_types.varinfo

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.

val cty : Frama_c_kernel.Cil_types.logic_type -> Frama_c_kernel.Cil_types.typ

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

val ptr_base : 
  loc:Frama_c_kernel.Cil_types.location ->
  Frama_c_kernel.Cil_types.exp ->
  Frama_c_kernel.Cil_types.exp

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

val ptr_base_and_base_addr : 
  loc:Frama_c_kernel.Cil_types.location ->
  Frama_c_kernel.Cil_types.exp ->
  Frama_c_kernel.Cil_types.exp * Frama_c_kernel.Cil_types.exp

val term_of_li : 
  Frama_c_kernel.Cil_types.logic_info ->
  Frama_c_kernel.Cil_types.term

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.

val finite_min_and_max : 
  Frama_c_kernel.Ival.t ->
  Frama_c_kernel.Integer.t * Frama_c_kernel.Integer.t

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

module Id_term : 
  Frama_c_kernel.Datatype.S_with_collections
    with type t = Frama_c_kernel.Cil_types.term

Datatype for terms that relies on 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.

On This Page

Handling \result
Other stuff