From 783172b7afb4f8321b547706f941417adac94448 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Tue, 25 Mar 2014 17:38:38 +0100
Subject: [PATCH] fix bug #1716 about annotations in while(1)
---
src/plugins/e-acsl/doc/Changelog | 3 ++-
src/plugins/e-acsl/pre_analysis.ml | 2 +-
2 files changed, 3 insertions(+), 2 deletions(-)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 8336ee75a9c..6a9b2d8ec1a 100644
--- a/src/plugins/e-acsl/doc/Changelog
+++ b/src/plugins/e-acsl/doc/Changelog
@@ -15,7 +15,8 @@
# E-ACSL: the Whole E-ACSL plug-in
###############################################################################
--* E-ACSL [2014/03/17] Fix bug #1715 about -e-acsl-full-mmodel which
+-* E-ACSL [2014/03/25] Fix bug #1716 with annotations in while(1).
+-* E-ACSL [2014/03/25] Fix bug #1715 about -e-acsl-full-mmodel which
generates incorrect code.
-* E-ACSL [2014/03/17] Fix bug #1700 about non-ISO empty struct.
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 637c6f76480..e97eb36f048 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -599,7 +599,7 @@ end = struct
List.iter (fun s -> Stmt.Hashtbl.replace tbl s (Some set)) returns)
init_set
end;
- D.compute returns
+ D.compute stmts
with Kernel_function.No_Definition | Kernel_function.No_Statement ->
());
Options.feedback ~dkey ~level:2 "function %a done."
--
GitLab