Module Exit_points

module Exit_points: sig .. end

E-ACSL tracks a local variable by injecting:


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