Frama-C:
Plug-ins:
Libraries:

Frama-C API - Locals_scoping

Auxiliary functions to mark invalid (more precisely 'escaping') the references to a variable whose scope ends.

type clobbered_set = {
  1. mutable clob : Frama_c_kernel.Base.SetLattice.t;
}

Set of bases that might contain a reference to a local or formal variable. Those references must be marked as dangling once we leave the scope of those local or formals.

val bottom : unit -> clobbered_set
val top : unit -> clobbered_set
val remember_bases_with_locals : clobbered_set -> Frama_c_kernel.Base.SetLattice.t -> unit

Add the given set of bases to an existing clobbered set

val remember_if_locals_in_value : clobbered_set -> Frama_c_kernel.Locations.location -> Frama_c_kernel.Cvalue.V.t -> unit

remember_locals_in_value clob loc v adds all bases pointed to by loc to clob if v contains the address of a local or formal

val offsetmap_contains_local : Frama_c_kernel.Cvalue.V_Offsetmap.t -> bool

make_escaping ~exact ~escaping ~on_escaping ~within state changes all references to the variables in escaping to "escaping address". All such references must be in the offsetmaps bound to within. on_escaping b itv v is called when a reference is found: v is the value that refers to escaping, b is the base in which v appears (included in within) and itv is the offset at which v appears. If exact holds, a strong update is performed. Otherwise, only a week update is executed.

make_escaping_fundec fdec clob l state changes all references to the local or formal variables in l to "escaping". All pointers to l should be in the offsetmap bound to the variables contained in clob. fdec is used to detect whether we are deallocating the outer scope of a function, in which case a different warning is emitted.

substitute substitution clob state applies substitution to all pointer values in the offsetmaps bound to variables in clob in state.