[E-ACSL] fix previous commit in case of multiple initializers (requires an...

[E-ACSL] fix previous commit in case of multiple initializers (requires an up-to-date Frama-C kernel)

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
 ###############

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