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 Dependency

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

Authors

Maintainers

F

frama-ci-bot@frama-c.com

Sources

frama-c-29.0-Copper.tar.gz

sha256=d2fbb3b8d0ff83945872e9e6fa258e934a706360e698dae3b4d5f971addf7493

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

module SpecialPointers : sig ... end

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_monitor_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_monitor_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_monitor_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.