From bc0f175b367541771310cd5ab7794175183cd5c4 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 21 Jan 2013 13:06:50 +0000
Subject: [PATCH] [E-ACSL] better handling of already-proven properties
---
src/plugins/e-acsl/pre_visit.ml | 16 ++++++++--------
.../e-acsl/tests/e-acsl-runtime/linear_search.i | 2 +-
2 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/src/plugins/e-acsl/pre_visit.ml b/src/plugins/e-acsl/pre_visit.ml
index 1fa4b0951a6..9fe4fd77ac3 100644
--- a/src/plugins/e-acsl/pre_visit.ml
+++ b/src/plugins/e-acsl/pre_visit.ml
@@ -53,6 +53,11 @@ let reset () =
(* Duplicating property statuses *)
(* ********************************************************************** *)
+let reemit = function
+ | Property.IPBehavior _ | Property.IPAxiom _ | Property.IPAxiomatic _
+ | Property.IPPredicate (Property.PKAssumes _, _, _, _) -> false
+ | _ -> true
+
let copy_ppt old_prj new_prj old_ppt new_ppt =
let module P = Property_status in
let selection = State_selection.of_list [ P.self; Emitter.self ] in
@@ -60,13 +65,8 @@ let copy_ppt old_prj new_prj old_ppt new_ppt =
Project.on ~selection new_prj
(fun s ->
let e = match l with [] -> assert false | e :: _ -> e in
-(* Options.feedback "HERE %a --> %a (%a)" Property.pretty new_ppt
- P.Emitted_status.pretty s Project.pretty new_prj;*)
- if not e.P.logical_consequence then
- let emitter = Emitter.Usable_emitter.get e.P.emitter in
-(* Options.feedback "EMIT %a --> %a (%a)" Property.pretty new_ppt
- P.Emitted_status.pretty s Project.pretty new_prj;*)
- P.emit emitter ~hyps:e.P.properties new_ppt s)
+ let emitter = Emitter.Usable_emitter.get e.P.emitter in
+ P.emit emitter ~hyps:e.P.properties new_ppt s)
s
in
let copy () =
@@ -77,7 +77,7 @@ let copy_ppt old_prj new_prj old_ppt new_ppt =
emit P.True i.P.valid;
emit P.False_and_reachable i.P.invalid
in
- if not (Options.Valid.get ()) then Queue.add copy actions
+ if reemit old_ppt && not (Options.Valid.get ()) then Queue.add copy actions
(* ********************************************************************** *)
(* Duplicating functions *)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i b/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i
index 05c2da44bba..00899cadc06 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/linear_search.i
@@ -1,5 +1,5 @@
/* run.config
- COMMENT: linear search (example of the TAP'12 article)
+ COMMENT: linear search (example of the SAC'13 article)
EXECNOW: LOG gen_linear_search.c BIN gen_linear_search.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/linear_search.i -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_linear_search.c > /dev/null && ./gcc_test.sh linear_search
EXECNOW: LOG gen_linear_search2.c BIN gen_linear_search2.out @frama-c@ -e-acsl-share ./share/e-acsl ./tests/e-acsl-runtime/linear_search.i -e-acsl-gmp-only -e-acsl -then-on e-acsl -print -ocode ./tests/e-acsl-runtime/result/gen_linear_search2.c > /dev/null && ./gcc_test.sh linear_search2
*/
--
GitLab