Module `Inout`Source

Source

val expr_inputs : 
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.exp ->
  Frama_c_kernel.Locations.Zone.t

Returns the memory zone needed to evaluate the given expression at the given statement.

Source

val stmt_inputs : 
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Locations.Zone.t

Returns the memory zone read by the given statement.

Source

val stmt_outputs : 
  Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Locations.Zone.t

Returns the memory zone modified by the given statement.

Source

val kf_inputs : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Locations.Zone.t

Returns the memory zone read by the given function, including its local and formal variables.

Source

val kf_external_inputs : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Locations.Zone.t

Returns the memory zone read by the given function, without its local and formal variables.

Source

val kf_outputs : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Locations.Zone.t

Returns the memory zone modified by the given function, including its local and formal variables.

Source

val kf_external_outputs : 
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Locations.Zone.t

Returns the memory zone modified by the given function, without its local and formal variables.

Source

val get_precise_inout : 
  ?stmt:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.kernel_function ->
  Frama_c_kernel.Inout_type.t

Returns the inputs/outputs computed for the given function. If stmt is specified and is a possible call to the given function, returns the inputs/outputs for this call specifically.

Sourceval self : Frama_c_kernel.State.t

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-inout.core/Inout/index.html

Module `Inout`Source

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-inout.core/Inout/index.html

Module InoutSource

Module `Inout`Source