Module Eva.Logic_inout

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.

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.

type annotation =
  1. | Code_annot
  2. | Assigns

Context of an evaluation: in a statement annotation or an assigns clause.

Evaluation of the memory zones and dependencies of an lvalue term, 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 dependencies computed by the from plugin. Emits warnings if needed, and sets statuses to the assigns clauses.

val accept_base : formals:bool -> locals:bool -> Frama_c_kernel.Kernel_function.t -> Frama_c_kernel.Base.t -> bool

accept_base ~formals ~locals kf b returns true if and only if b is:

  • a global
  • a formal or local of one of the callers of kf
  • a formal or local of kf and the corresponding argument is true.