package frama-c

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

Functions used by the Inout and From plugins to interpret predicate and assigns clauses. This API may change according to these plugins development.

predicate_deps ~pre ~here p computes the logic dependencies needed to evaluate the predicate p in cvalue state here, in a function whose pre-state is pre. Returns None on either an evaluation error or on unsupported construct.

term_deps state t computes the logic dependencies needed to evaluate the term t in cvalue state state. Returns None on either an evaluation error or on unsupported construct.

Returns the list of behaviors of the given function that are active for the given initial state.

Evaluation of the memory zone read by the \from part of an assigns clause, in the given cvalue state.

Evaluation of the memory zone written by an assigns clauses, in the given cvalue state.

type tlval_zones = {
  1. under : Frama_c_kernel.Locations.Zone.t;
    (*

    Under-approximation of the memory zone.

    *)
  2. over : Frama_c_kernel.Locations.Zone.t;
    (*

    Over-approximation of the memory zone.

    *)
  3. deps : Frama_c_kernel.Locations.Zone.t;
    (*

    Dependencies needed to evaluate the address.

    *)
}

Zones of an lvalue term of an assigns clause.

Evaluation of the memory zones and dependencies of an lvalue term from an assigns clause, in the given cvalue state for a read or write access.

Evaluate the assigns clauses of the given function in its given pre-state, and compare them with the given froms (computed by the from plugin). Emits warnings if needed, and sets statuses to the assigns clauses.

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