package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type
type effects = {
  1. direct : bool;
    (*

    Direct affectation lv = ..., or modification through a call to a leaf function.

    *)
  2. indirect : bool;
    (*

    Modification inside the body of called function f(...)

    *)
}

Given an effect e, something is directly modified by e (through an affectation, or through a call to a leaf function) if direct holds, and indirectly (through the effects of a call) otherwise.

compute z finds all the statements that modifies z, and for each statement, indicates whether the modification is direct or indirect.