[E-ACSL] order of some generated instructions does not depend anymore on hash implementation

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c

@@ -104,31 +104,31 @@ void e_acsl_global_init(void)
   char *__e_acsl_literal_string_3;
   char *__e_acsl_literal_string_2;
   char *__e_acsl_literal_string;
-  __store_block((void *)(& S),4U);
-  __e_acsl_literal_string = "foo2";
-  __store_block((void *)__e_acsl_literal_string,sizeof("foo2"));
+  __store_block((void *)(& G2),4U);
+  __e_acsl_literal_string = "bar";
+  __store_block((void *)__e_acsl_literal_string,sizeof("bar"));
   __full_init((void *)__e_acsl_literal_string);
   __literal_string((void *)__e_acsl_literal_string);
-  __e_acsl_literal_string_2 = "bar";
-  __store_block((void *)__e_acsl_literal_string_2,sizeof("bar"));
+  __e_acsl_literal_string_2 = "foo";
+  __store_block((void *)__e_acsl_literal_string_2,sizeof("foo"));
   __full_init((void *)__e_acsl_literal_string_2);
   __literal_string((void *)__e_acsl_literal_string_2);
-  __e_acsl_literal_string_3 = "foo";
-  __store_block((void *)__e_acsl_literal_string_3,sizeof("foo"));
+  __e_acsl_literal_string_3 = "foo2";
+  __store_block((void *)__e_acsl_literal_string_3,sizeof("foo2"));
   __full_init((void *)__e_acsl_literal_string_3);
   __literal_string((void *)__e_acsl_literal_string_3);
+  __full_init((void *)(& G2));
+  __store_block((void *)(& S2),4U);
+  __full_init((void *)(& S2));
+  S2 = (char *)__e_acsl_literal_string_3;
+  __store_block((void *)(& S),4U);
   __full_init((void *)(& S));
-  S = (char *)__e_acsl_literal_string_3;
+  S = (char *)__e_acsl_literal_string_2;
   __store_block((void *)(& G),4U);
   __full_init((void *)(& G));
   __store_block((void *)(& T),4U);
   __full_init((void *)(& T));
-  T = (char *)__e_acsl_literal_string_2;
-  __store_block((void *)(& G2),4U);
-  __full_init((void *)(& G2));
-  __store_block((void *)(& S2),4U);
-  __full_init((void *)(& S2));
-  S2 = (char *)__e_acsl_literal_string;
+  T = (char *)__e_acsl_literal_string;
   return;
 }
 

src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c

@@ -129,31 +129,31 @@ void e_acsl_global_init(void)
   char *__e_acsl_literal_string_3;
   char *__e_acsl_literal_string_2;
   char *__e_acsl_literal_string;
-  __store_block((void *)(& S),4U);
-  __e_acsl_literal_string = "foo2";
-  __store_block((void *)__e_acsl_literal_string,sizeof("foo2"));
+  __store_block((void *)(& G2),4U);
+  __e_acsl_literal_string = "bar";
+  __store_block((void *)__e_acsl_literal_string,sizeof("bar"));
   __full_init((void *)__e_acsl_literal_string);
   __literal_string((void *)__e_acsl_literal_string);
-  __e_acsl_literal_string_2 = "bar";
-  __store_block((void *)__e_acsl_literal_string_2,sizeof("bar"));
+  __e_acsl_literal_string_2 = "foo";
+  __store_block((void *)__e_acsl_literal_string_2,sizeof("foo"));
   __full_init((void *)__e_acsl_literal_string_2);
   __literal_string((void *)__e_acsl_literal_string_2);
-  __e_acsl_literal_string_3 = "foo";
-  __store_block((void *)__e_acsl_literal_string_3,sizeof("foo"));
+  __e_acsl_literal_string_3 = "foo2";
+  __store_block((void *)__e_acsl_literal_string_3,sizeof("foo2"));
   __full_init((void *)__e_acsl_literal_string_3);
   __literal_string((void *)__e_acsl_literal_string_3);
+  __full_init((void *)(& G2));
+  __store_block((void *)(& S2),4U);
+  __full_init((void *)(& S2));
+  S2 = (char *)__e_acsl_literal_string_3;
+  __store_block((void *)(& S),4U);
   __full_init((void *)(& S));
-  S = (char *)__e_acsl_literal_string_3;
+  S = (char *)__e_acsl_literal_string_2;
   __store_block((void *)(& G),4U);
   __full_init((void *)(& G));
   __store_block((void *)(& T),4U);
   __full_init((void *)(& T));
-  T = (char *)__e_acsl_literal_string_2;
-  __store_block((void *)(& G2),4U);
-  __full_init((void *)(& G2));
-  __store_block((void *)(& S2),4U);
-  __full_init((void *)(& S2));
-  S2 = (char *)__e_acsl_literal_string;
+  T = (char *)__e_acsl_literal_string;
   return;
 }
 

src/plugins/e-acsl/visit.ml

@@ -150,7 +150,7 @@ class e_acsl_visitor prj generate = object (self)
 	      in
 	      let env = Env.push !function_env in
 	      let stmts, env = 
-		Varinfo.Hashtbl.fold
+		Varinfo.Hashtbl.fold_sorted
 		  (fun old_vi i (stmts, env) -> 
 		    let new_vi = Cil.get_varinfo self#behavior old_vi in
 		    let model blk =