From f7169fb04b589cb12a1bdc73b7d3834cfb1a6feb Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 25 Sep 2013 12:41:11 +0000
Subject: [PATCH] [E-ACSL] some loop invariants were tagged as 'assertions'
---
src/plugins/e-acsl/TODO | 6 +++---
src/plugins/e-acsl/doc/Changelog | 2 ++
src/plugins/e-acsl/loops.ml | 1 +
3 files changed, 6 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/TODO b/src/plugins/e-acsl/TODO
index 07864bf4047..2652369061c 100644
--- a/src/plugins/e-acsl/TODO
+++ b/src/plugins/e-acsl/TODO
@@ -9,6 +9,7 @@
- memory profiling
- [Guillaume] ajouter les annotations de RTE dans la table des annotations
(avec une option)
+- [David Mentré] tset
#####################
# E-ACSL CONSTRUCTS #
@@ -21,6 +22,7 @@
- loop variant
- logical shift (at least in non GMP mode)
- let-in
+- tset
- grep "not_yet" *.ml
########
@@ -69,7 +71,6 @@
(voir aussi result.i et ./at_stmt_contract.i)
- interprétation des tableaux logiques
[Dillon] Windows
-[Guillaume] look like some loop invariants are tagged as "assertion"
[to be check]: no call to full_init or initialize for the assigned result of a
function call
@@ -87,5 +88,4 @@ function call
- inclure exemple du E-ACSL Reference Manual
- inclure exemple du E-ACSL User Manual
- inclure exemple du E-ACSL Tutorial
-- test arith.i: mettre les exemples du ACSL manual about div and modulo
-- currently, tests require a non-free version of Frama-C
+- currently, tests require a non-free version of Frama-C (built-ins Value)
diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog
index 58de08d9fac..a9f8c6c57e0 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/25] Some loop invariants were tagged as "assertions".
+
###################################
Plugin E-ACSL 0.3 Fluorine_20130601
###################################
diff --git a/src/plugins/e-acsl/loops.ml b/src/plugins/e-acsl/loops.ml
index 68fd01bf680..decfc08b779 100644
--- a/src/plugins/e-acsl/loops.ml
+++ b/src/plugins/e-acsl/loops.ml
@@ -68,6 +68,7 @@ let preserve_invariant prj env kf stmt = match stmt.skind with
Misc.mk_block prj last blk :: stmts, env, invariants != []
| s :: tl -> handle_invariants (s :: stmts, env, false) tl
in
+ let env = Env.set_annotation_kind env Misc.Invariant in
let stmts, env, has_loop = handle_invariants ([], env, false) stmts in
let new_blk = { blk with bstmts = List.rev stmts } in
{ stmt with skind = Loop([], new_blk, loc, cont, break) },
--
GitLab