package frama-c

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

Module Studia.ReadsSource

Computations of the statements that read a given memory zone.

Sourcetype t =
  1. | Direct of Frama_c_kernel.Cil_types.stmt
    (*

    Direct read by a statement.

    *)
  2. | Indirect of Frama_c_kernel.Cil_types.stmt
    (*

    Indirect read through a function call.

    *)

compute z finds all the statements that read z. The effects information indicates whether the read occur on the given statement, or through an inner call for Call instructions.