From 48d16df930c160c23c5034315b7ec811f6ced255 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Wed, 4 Sep 2013 15:04:06 +0000
Subject: [PATCH] [E-ACSL] fix previous commit in case of multiple initializers
(requires an up-to-date Frama-C kernel)
---
src/plugins/e-acsl/configure.ac | 17 +++++++----------
src/plugins/e-acsl/pre_analysis.ml | 2 +-
2 files changed, 8 insertions(+), 11 deletions(-)
diff --git a/src/plugins/e-acsl/configure.ac b/src/plugins/e-acsl/configure.ac
index ec1d280c702..cb00b0fc14c 100644
--- a/src/plugins/e-acsl/configure.ac
+++ b/src/plugins/e-acsl/configure.ac
@@ -56,20 +56,17 @@ AC_MSG_CHECKING(for Frama-C version)
DEV_VERSION_NUMBER=`echo $FRAMAC_VERSION | sed -e 's/.*-\(.*\)/\1/' `
VERSION_NUMBER=`echo $DEV_VERSION_NUMBER | sed -e 's/\(.*\)+dev/\1/' `
-if test $VERSION_NUMBER -lt 20130401; then
- AC_MSG_ERROR(Frama-C version must be at least Fluorine-20130401.)
-else if test $VERSION_NUMBER -gt 20130501; then
- AC_MSG_WARN(Frama-C version higher than Fluorine-20130501 not tested: use it at your own risk.)
-fi
+if test $VERSION_NUMBER -lt 20130601; then
+ AC_MSG_ERROR(Frama-C version must be at least Fluorine-20130601.)
fi
# at the time being, must use the Frama-C development version
-# DEV=`echo $DEV_VERSION_NUMBER | sed -e 's/.*\(+dev\)/\1/' `
-# if test "$DEV" != "+dev"; then
-# AC_MSG_ERROR(Frama-C version must be the current SVN version.);
-# else
+DEV=`echo $DEV_VERSION_NUMBER | sed -e 's/.*\(+dev\)/\1/' `
+if test "$DEV" != "+dev"; then
+ AC_MSG_ERROR(Frama-C version must be the current SVN version.);
+else
AC_MSG_RESULT($FRAMAC_VERSION)
-# fi
+fi
# OCaml version
###############
diff --git a/src/plugins/e-acsl/pre_analysis.ml b/src/plugins/e-acsl/pre_analysis.ml
index 7d5b9ba80e6..9f46401e2f5 100644
--- a/src/plugins/e-acsl/pre_analysis.ml
+++ b/src/plugins/e-acsl/pre_analysis.ml
@@ -380,7 +380,7 @@ module rec Transfer
| None -> state
| Some init -> do_init vi init state
in
- Globals.Vars.fold_in_file_order do_one state
+ Globals.Vars.fold_in_file_rev_order do_one state
(** The (backwards) transfer function for a branch. The [(Cil.CurrentLoc.get
())] is set before calling this. If it returns None, then we have some
--
GitLab