Frama-C:
Plug-ins:
Libraries:

Frama-C API - 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)?

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.

Same as must_monitor_vi, for left-values

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.