From 8d4a45fad4bc7fcf42d4febaa3f1644a59acb54b Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 4 Sep 2013 09:41:17 +0000
Subject: [PATCH] [E-ACSL] fixed bug #1473 about removing the default project
on a corner case
---
src/plugins/e-acsl/TODO | 2 ++
src/plugins/e-acsl/doc/Changelog | 2 ++
src/plugins/e-acsl/main.ml | 33 +++++++++++++++++++++-----------
3 files changed, 26 insertions(+), 11 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 02a9b6fff51..9f341167868 100644
--- a/src/plugins/e-acsl/TODO
+++ b/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
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 1b49d78daec..0851d76b828 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/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
diff --git a/src/plugins/e-acsl/main.ml b/src/plugins/e-acsl/main.ml
index 0250febfdbe..31c81c15d53 100644
--- a/src/plugins/e-acsl/main.ml
+++ b/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 =
--
GitLab