[e-acsl] second revision

src/plugins/e-acsl/src/analyses/bound_variables.ml

@@ -64,8 +64,9 @@ module Quantified_predicate =
             |lv::_ -> Cil_datatype.Logic_var.hash lv
           end
         | _ -> assert false
-      let compare (p1:predicate) p2 =
-        if p1 == p2 then 0 else 1
+      (* The function compare should never be used since we only use this
+         datatype for hashtables *)
+      let compare _ _ = assert false
       let equal (p1:predicate) p2 = p1 == p2
       let structural_descr = Structural_descr.t_abstract
       let rehash = Datatype.identity
@@ -85,6 +86,7 @@ module Quantifier: sig
       of the variable *)
   val get_guard_for_small_type : logic_var -> predicate option
   val add_guard_for_small_type : logic_var -> predicate option -> unit
+  val clear : unit -> unit
 end = struct
 
   let tbl = Quantified_predicate.Hashtbl.create 97
@@ -112,10 +114,15 @@ end = struct
 
   let add_guard_for_small_type lv p =
     Cil_datatype.Logic_var.Hashtbl.add guard_tbl lv p
+
+  let clear () =
+    Cil_datatype.Logic_var.Hashtbl.clear guard_tbl;
+    Quantified_predicate.Hashtbl.clear tbl
 end
 
 let get_preprocessed_quantifier = Quantifier.get
 let get_guard_for_small_type = Quantifier.get_guard_for_small_type
+let clear_guards = Quantifier.clear
 
 (** Helper module to process the constraints in the quantification and extract
     guards for the quantified variables. *)
@@ -701,16 +708,18 @@ let normalize_guard ~loc (t1, rel1, lv, rel2, t2) =
     | Rle ->
       t1
     | Rgt | Rge | Req | Rneq ->
-      assert false  in
+      assert false
+  in
   let t2 = match rel2 with
     | Rlt ->
       t2
     | Rle ->
       t_plus_one t2
     | Rgt | Rge | Req | Rneq ->
-      assert false in
-  let t1, t2, guard_for_small_type = bounds_for_small_types ~loc (t1, lv, t2) in
-  Quantifier.add_guard_for_small_type lv guard_for_small_type;
+      assert false
+  in
+  let t1, t2, guard_for_small_type = bounds_for_small_types ~loc (t1, lv, t2)
+  in Quantifier.add_guard_for_small_type lv guard_for_small_type;
   t1, lv, t2
 
 let compute_guards loc ~is_forall p bounded_vars hyps =

src/plugins/e-acsl/src/analyses/bound_variables.mli

@@ -25,9 +25,18 @@ open Cil_datatype
 
 
 val compute_guards: location -> is_forall:bool -> predicate -> Logic_var.t list -> predicate -> unit
-(** Takes a predicate starting with a quantifier and store the scope of its variable *)
+(** Take a predicate starting with a quantifier and store the scope of its variable *)
 
 val get_preprocessed_quantifier: predicate -> (term * logic_var * term) list * predicate
-(** Returns the preprocessed form of a quantifier *)
+(** @return the preprocessed of a quantified predicate
+    the [(term * logic_var * term) list] is the list of all the quantified variables
+    along with their syntactic guards, and the [predicate] is the goal: the original
+    predicate with all the quantifiers removed *)
 
 val get_guard_for_small_type : logic_var -> predicate option
+(** @return the optional additional guard for a quantified logic variables. It may
+    happen that the syntactic guard of the variable can be refined with the type
+    of the variable, this additional predicate translates this refinement *)
+
+val clear_guards : unit -> unit
+(** Clear the table of guard conditions for quantified variables *)

src/plugins/e-acsl/src/code_generator/injector.ml

@@ -831,6 +831,7 @@ let reset_all ast =
   Logic_functions.reset ();
   Literal_strings.reset ();
   Global_observer.reset ();
+  Bound_variables.clear_guards ();
   Typing.clear ();
   (* reset some kernel states: *)
   (* reset the CFG that has been heavily modified by the code generation step *)