package frama-c

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

Create a statement from a statement kind.

Create a block statement from a block to replace a given statement. Requires that (1) the block is not empty, or (2) the statement is a skip.

Create a block statement from a block

Create a block statement from a statement list.

assigns ~loc ~result value creates a statement to assign the value expression to the result lval.

assigns_field ~loc vi field value creates a statement to assign the value expression to the field of the structure in the variable vi.

if ~loc ~cond ~then_blk ~else_blk creates an if statement with cond as condition and then_blk and else_blk as respectively "then" block and "else" block.

Create a break statement

struct_local_init ~loc vi fields creates a local initialization for the structure variable vi. fields is a list of couple (name, e) where name is the name of a field in the structure and e is the expression to initialize that field.

Construct a call to a function with the given name.

  • raises Not_found

    if the given string does not represent a function in the AST, for instance if the function does not exist.

Construct a call to a library function with the given name.

prefix defaults to the E-ACSL RTL API prefix and can be explicitely provided to call functions without this prefix.

  • raises Rtl.Symbols.Unregistered

    if the given string does not represent such a function or if library functions were never registered (only possible when using E-ACSL through its API).

Construct a call to __e_acsl_store_block that observes the allocation of the given varinfo. See share/e-acsl/e_acsl.h for details about this function.

Same as store_stmt for __e_acsl_duplicate_store_block that first checks for a previous allocation of the given varinfo.

Same as store_stmt for __e_acsl_delete_block that observes the de-allocation of the given varinfo. If is_addr is false (default), take the address of varinfo.

Same as store_stmt for __e_acsl_full_init that observes the initialization of the given varinfo. The varinfo is the address to fully initialize, no addrOf is taken.

Same as store_stmt for __e_acsl_initialize that observes the initialization of the given left-value.

Same as store_stmt for __e_acsl_markreadonly that observes the read-onlyness of the given varinfo.

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