package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Platform dedicated to the analysis of source code written in C

Install

dune-project

Dependency

frama-c.com Readme Edit opam file Versions (25)

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-27.0-beta-Cobalt.tar.gz

sha256=9c1b14a689ac8ccda9e827c2eede13bb8d781fb8e4e33c1b5360408e312127d2

doc/frama-c-e-acsl.core/E_ACSL/Memory_tracking/index.html

Module `E_ACSL.Memory_tracking`

Compute a sound over-approximation of what left-values must be tracked by the memory model library

val reset : unit -> unit

Must be called to redo the analysis

val use_monitoring : unit -> bool

Is one variable monitored (at least)?

val must_monitor_vi : 
  ?kf:Frama_c_kernel.Cil_types.kernel_function ->
  ?stmt:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.varinfo ->
  bool

must_model_vi ?kf ?stmt vi returns true if the varinfo vi at the given stmt in the given function kf must be tracked by the memory model library.

val must_monitor_lval : 
  ?kf:Frama_c_kernel.Cil_types.kernel_function ->
  ?stmt:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.lval ->
  bool

Same as must_model_vi, for left-values

val must_monitor_exp : 
  ?kf:Frama_c_kernel.Cil_types.kernel_function ->
  ?stmt:Frama_c_kernel.Cil_types.stmt ->
  Frama_c_kernel.Cil_types.exp ->
  bool

Same as must_model_vi, for expressions

val found_concurrent_function : 
  loc:Frama_c_kernel.Cil_types.location ->
  Frama_c_kernel.Cil_types.varinfo ->
  unit

found_concurrent_function ~loc fvi signals to the memory tracking sub-system that a concurrent function fvi has been found at loc while parsing the sources. This function needs only to be called if the concurrency support of E-ACSL is deactivated.

If the memory monitoring is in use when a concurrent function is found, abort the parsing: the user needs to activate the concurrency support.

Otherwise store the information of the first concurrent function found. Later if the memory monitoring is used because of memory properties to verify, then abort the parsing: the user needs to activate the concurrency support.

In summary, an analyzed source code can be concurrent with the concurrency support of E-ACSL deactivated only if no memory properties are to be verified.