[E-ACSL] fixed bug #1473 about removing the default project on a corner case

src/plugins/e-acsl/TODO

@@ -19,6 +19,7 @@
 - loop invariant
 - loop variant
 - grep "not_yet" *.ml
+- logical shift (at least in non GMP mode)
 
 ########
 # CODE #
@@ -84,3 +85,4 @@ function call
 - inclure exemple du E-ACSL Reference Manual
 - inclure exemple du E-ACSL User Manual
 - test arith.i: mettre les exemples du ACSL manual about div and modulo
+- currently, tests require a non-free version of Frama-C

src/plugins/e-acsl/doc/Changelog

@@ -15,6 +15,8 @@
 #   E-ACSL: the Whole E-ACSL plug-in
 ###############################################################################
 
+-* E-ACSL       [2013/09/04] Fix bug when mixing -e-acsl-prepare and
+	        running E-ACSL in another project (bts #!1473).
 -* E-ACSL       [2013/06/26] Fix crash with typedef on pointer types.
 -  E-ACSL       [2013/06/21] Fewer unknown locations.
 -* E-ACSL       [2013/06/18] Fixed bug when generating RTEs on the E-ACSL

src/plugins/e-acsl/main.ml

@@ -43,7 +43,11 @@ let check =
     (Datatype.func Datatype.unit Datatype.bool)
     check
 
-let extended_ast_project: Project.t option ref = ref None
+type extended_project =
+  | To_be_extended
+  | Already_extended of Project.t option (* None = keep the current project *)
+
+let extended_ast_project: extended_project ref = ref To_be_extended
 
 let unmemoized_extend_ast () =
   let extend () =
@@ -89,27 +93,34 @@ E-ACSL is going to work on a copy.";
 	Kernel.Files.set [ tmpfile ];
 	extend ())
       ();
-    prj
+    Some prj
   end else begin
     extend ();
-    Project.current ()
+    None
   end
 
 let extend_ast () = match !extended_ast_project with
-  | None -> 
+  | To_be_extended -> 
     let prj = unmemoized_extend_ast () in
-    extended_ast_project := Some prj;
-    prj
-  | Some prj ->
+    extended_ast_project := Already_extended prj;
+    (match prj with
+    | None -> Project.current ()
+    | Some prj -> prj)
+  | Already_extended None ->
+    Project.current ()
+  | Already_extended(Some prj) ->
     prj
 
 let apply_on_e_acsl_ast f x =
   let tmp_prj = extend_ast () in
   let res = Project.on tmp_prj f x in
-  if not (Project.equal tmp_prj (Project.current ())) then begin
-    extended_ast_project := None;
-    Project.remove ~project:tmp_prj ()
-  end;
+  (match !extended_ast_project with
+  | To_be_extended -> assert false
+  | Already_extended None -> ()
+  | Already_extended (Some prj) ->
+    assert (Project.equal prj tmp_prj);
+    extended_ast_project := To_be_extended;
+    Project.remove ~project:tmp_prj ());
   res
 
 module Resulting_projects =