module Exit_points:sig
..end
E-ACSL tracks a local variable by injecting:
__e_acsl_store_block
at the beginning of its scope, and__e_acsl_delete_block
at the end of the scope.
This is not always sufficient to track variables because execution
may exit a scope early (for instance via a goto or a break statement).
This module computes program points at which extra `delete_block` statements
need to be added to handle such early scope exits.val generate : Cil_types.fundec -> unit
Visit a function and populate data structures used to compute exit points
val clear : unit -> unit
Clear all gathered data
val delete_vars : Cil_types.stmt -> Cil_datatype.Varinfo.Set.t
Given a statement which potentially leads to an early scope exit (such as
goto, break or continue) return the list of local variables which
need to be removed from tracking before that statement is executed.
Before calling this function generate
need to be executed.
val store_vars : Cil_types.stmt -> Cil_datatype.Varinfo.Set.t
Compute variables that should be re-recorded before a labelled statement to which some goto jumps