Merge branch 'bugfix/basile/eacsl-124-gen-globals-order' into 'master'

[eacsl] Fix order of generated globals

Closes e-acsl#124

See merge request frama-c/frama-c!2761

src/plugins/e-acsl/doc/Changelog

@@ -25,9 +25,11 @@
 Plugin E-ACSL <next-release>
 ############################
 
+-* E-ACSL       [2020-07-20] Fix unstable order of generated globals.
+                (frama-c/e-acsl#124)
 -* E-ACSL       [2020-07-10] Fix translation of trange (incorrect length).
 -* E-ACSL       [2020-07-09] Decrease the number of allocated blocks when one
-	        block is freed.
+                block is freed.
 -  E-ACSL       [2020-06-19] Add support of bitwise operators for C integers.
                 (frama-c/e-acsl#33)
 -  E-ACSL       [2020-06-19] Add support to create GMP rational from GMP

src/plugins/e-acsl/src/code_generator/logic_functions.ml

@@ -260,7 +260,7 @@ let add_generated_functions globals =
            GFunDecl(Cil.empty_funspec (), Kernel_function.get_vi kf, loc)
            :: acc
          in
-         aux (Params_ty.Hashtbl.fold (fun _ -> add_fundecl) params acc) l
+         aux (Params_ty.Hashtbl.fold_sorted (fun _ -> add_fundecl) params acc) l
        with Not_found ->
          aux acc l)
     | g :: l ->
@@ -276,8 +276,8 @@ let add_generated_functions globals =
     GFun(fundec, Location.unknown) :: globals
   in
   let rev_globals =
-    Logic_info.Hashtbl.fold
-      (fun _ -> Params_ty.Hashtbl.fold (fun _ -> add_fundec))
+    Logic_info.Hashtbl.fold_sorted
+      (fun _ -> Params_ty.Hashtbl.fold_sorted (fun _ -> add_fundec))
       memo_tbl
       rev_globals
   in

src/plugins/e-acsl/tests/arith/oracle_ci/gen_functions.c

@@ -17,10 +17,10 @@ int __gen_e_acsl_p1(int x, int y);
 */
 int __gen_e_acsl_p2(int x, int y);
 
-int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y);
-
 int __gen_e_acsl_p2_5(int x, long y);
 
+int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y);
+
 /*@ logic ℤ f1(ℤ x, ℤ y) = x + y;
 
 */
@@ -232,56 +232,18 @@ void __gen_e_acsl_k(int x)
   return;
 }
 
-int __gen_e_acsl_g(int x)
-{
-  int __gen_e_acsl_g_hidden_2;
-  __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
-  return __gen_e_acsl_g_hidden_2;
-}
-
-mystruct __gen_e_acsl_t1(mystruct m)
-{
-  return m;
-}
-
 int __gen_e_acsl_p1(int x, int y)
 {
   int __retres = x + (long)y > 0L;
   return __retres;
 }
 
-long __gen_e_acsl_t2(mystruct m)
-{
-  long __retres = m.k + (long)m.l;
-  return __retres;
-}
-
 int __gen_e_acsl_p2(int x, int y)
 {
   int __retres = x + (long)y > 0L;
   return __retres;
 }
 
-int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
-{
-  __e_acsl_mpz_t __gen_e_acsl_x;
-  __e_acsl_mpz_t __gen_e_acsl_add;
-  __e_acsl_mpz_t __gen_e_acsl__2;
-  int __gen_e_acsl_gt;
-  __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
-  __gmpz_init(__gen_e_acsl_add);
-  __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
-             (__e_acsl_mpz_struct const *)(y));
-  __gmpz_init_set_si(__gen_e_acsl__2,0L);
-  __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
-                               (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
-  int __retres = __gen_e_acsl_gt > 0;
-  __gmpz_clear(__gen_e_acsl_x);
-  __gmpz_clear(__gen_e_acsl_add);
-  __gmpz_clear(__gen_e_acsl__2);
-  return __retres;
-}
-
 int __gen_e_acsl_p2_5(int x, long y)
 {
   __e_acsl_mpz_t __gen_e_acsl_x_2;
@@ -306,9 +268,23 @@ int __gen_e_acsl_p2_5(int x, long y)
   return __retres;
 }
 
-int __gen_e_acsl_k_pred(int x)
+int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
 {
-  int __retres = x > 0;
+  __e_acsl_mpz_t __gen_e_acsl_x;
+  __e_acsl_mpz_t __gen_e_acsl_add;
+  __e_acsl_mpz_t __gen_e_acsl__2;
+  int __gen_e_acsl_gt;
+  __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
+  __gmpz_init(__gen_e_acsl_add);
+  __gmpz_add(__gen_e_acsl_add,(__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+             (__e_acsl_mpz_struct const *)(y));
+  __gmpz_init_set_si(__gen_e_acsl__2,0L);
+  __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_add),
+                               (__e_acsl_mpz_struct const *)(__gen_e_acsl__2));
+  int __retres = __gen_e_acsl_gt > 0;
+  __gmpz_clear(__gen_e_acsl_x);
+  __gmpz_clear(__gen_e_acsl_add);
+  __gmpz_clear(__gen_e_acsl__2);
   return __retres;
 }
 
@@ -363,6 +339,30 @@ int __gen_e_acsl_g_hidden(int x)
   return x;
 }
 
+int __gen_e_acsl_g(int x)
+{
+  int __gen_e_acsl_g_hidden_2;
+  __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
+  return __gen_e_acsl_g_hidden_2;
+}
+
+mystruct __gen_e_acsl_t1(mystruct m)
+{
+  return m;
+}
+
+long __gen_e_acsl_t2(mystruct m)
+{
+  long __retres = m.k + (long)m.l;
+  return __retres;
+}
+
+int __gen_e_acsl_k_pred(int x)
+{
+  int __retres = x > 0;
+  return __retres;
+}
+
 double __gen_e_acsl_f2(double x)
 {
   __e_acsl_mpq_t __gen_e_acsl__8;

src/plugins/e-acsl/tests/gmp-only/oracle_ci/gen_functions.c

@@ -288,18 +288,6 @@ void __gen_e_acsl_k(int x)
   return;
 }
 
-int __gen_e_acsl_g(int x)
-{
-  int __gen_e_acsl_g_hidden_2;
-  __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
-  return __gen_e_acsl_g_hidden_2;
-}
-
-mystruct __gen_e_acsl_t1(mystruct m)
-{
-  return m;
-}
-
 int __gen_e_acsl_p1(int x, int y)
 {
   __e_acsl_mpz_t __gen_e_acsl_x;
@@ -323,25 +311,6 @@ int __gen_e_acsl_p1(int x, int y)
   return __retres;
 }
 
-void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m)
-{
-  __e_acsl_mpz_t __gen_e_acsl__10;
-  __e_acsl_mpz_t __gen_e_acsl__11;
-  __e_acsl_mpz_t __gen_e_acsl_add_7;
-  __gmpz_init_set_si(__gen_e_acsl__10,(long)m.k);
-  __gmpz_init_set_si(__gen_e_acsl__11,(long)m.l);
-  __gmpz_init(__gen_e_acsl_add_7);
-  __gmpz_add(__gen_e_acsl_add_7,
-             (__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
-             (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
-  __gmpz_init_set(*__retres_arg,
-                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
-  __gmpz_clear(__gen_e_acsl__10);
-  __gmpz_clear(__gen_e_acsl__11);
-  __gmpz_clear(__gen_e_acsl_add_7);
-  return;
-}
-
 int __gen_e_acsl_p2(int x, int y)
 {
   __e_acsl_mpz_t __gen_e_acsl_x_2;
@@ -387,21 +356,6 @@ int __gen_e_acsl_p2_3(int x, __e_acsl_mpz_struct * y)
   return __retres;
 }
 
-int __gen_e_acsl_k_pred(int x)
-{
-  __e_acsl_mpz_t __gen_e_acsl_x;
-  __e_acsl_mpz_t __gen_e_acsl_;
-  int __gen_e_acsl_gt;
-  __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
-  __gmpz_init_set_si(__gen_e_acsl_,0L);
-  __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
-                               (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
-  int __retres = __gen_e_acsl_gt > 0;
-  __gmpz_clear(__gen_e_acsl_x);
-  __gmpz_clear(__gen_e_acsl_);
-  return __retres;
-}
-
 void __gen_e_acsl_f1(__e_acsl_mpz_t *__retres_arg, int x, int y)
 {
   __e_acsl_mpz_t __gen_e_acsl_x_4;
@@ -466,6 +420,52 @@ int __gen_e_acsl_g_hidden(int x)
   return x;
 }
 
+int __gen_e_acsl_g(int x)
+{
+  int __gen_e_acsl_g_hidden_2;
+  __gen_e_acsl_g_hidden_2 = __gen_e_acsl_g_hidden(x);
+  return __gen_e_acsl_g_hidden_2;
+}
+
+mystruct __gen_e_acsl_t1(mystruct m)
+{
+  return m;
+}
+
+void __gen_e_acsl_t2(__e_acsl_mpz_t *__retres_arg, mystruct m)
+{
+  __e_acsl_mpz_t __gen_e_acsl__10;
+  __e_acsl_mpz_t __gen_e_acsl__11;
+  __e_acsl_mpz_t __gen_e_acsl_add_7;
+  __gmpz_init_set_si(__gen_e_acsl__10,(long)m.k);
+  __gmpz_init_set_si(__gen_e_acsl__11,(long)m.l);
+  __gmpz_init(__gen_e_acsl_add_7);
+  __gmpz_add(__gen_e_acsl_add_7,
+             (__e_acsl_mpz_struct const *)(__gen_e_acsl__10),
+             (__e_acsl_mpz_struct const *)(__gen_e_acsl__11));
+  __gmpz_init_set(*__retres_arg,
+                  (__e_acsl_mpz_struct const *)(__gen_e_acsl_add_7));
+  __gmpz_clear(__gen_e_acsl__10);
+  __gmpz_clear(__gen_e_acsl__11);
+  __gmpz_clear(__gen_e_acsl_add_7);
+  return;
+}
+
+int __gen_e_acsl_k_pred(int x)
+{
+  __e_acsl_mpz_t __gen_e_acsl_x;
+  __e_acsl_mpz_t __gen_e_acsl_;
+  int __gen_e_acsl_gt;
+  __gmpz_init_set_si(__gen_e_acsl_x,(long)x);
+  __gmpz_init_set_si(__gen_e_acsl_,0L);
+  __gen_e_acsl_gt = __gmpz_cmp((__e_acsl_mpz_struct const *)(__gen_e_acsl_x),
+                               (__e_acsl_mpz_struct const *)(__gen_e_acsl_));
+  int __retres = __gen_e_acsl_gt > 0;
+  __gmpz_clear(__gen_e_acsl_x);
+  __gmpz_clear(__gen_e_acsl_);
+  return __retres;
+}
+
 double __gen_e_acsl_f2(double x)
 {
   __e_acsl_mpq_t __gen_e_acsl__13;