From 39064bd00ae63fffbc93d198df8a345a3b23cde8 Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Fri, 30 Nov 2012 08:03:44 +0000
Subject: [PATCH] [E-ACSL] order of some generated instructions does not depend
anymore on hash implementation
---
.../oracle/gen_literal_string.c | 28 +++++++++----------
.../oracle/gen_literal_string2.c | 28 +++++++++----------
src/plugins/e-acsl/visit.ml | 2 +-
3 files changed, 29 insertions(+), 29 deletions(-)
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
index 3d159d5b0bf..02532f4105b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
index dca4b1cccc1..3d8a44702c8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/gen_literal_string2.c
+++ b/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;
}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 8424e6b55ae..d4f061d60e7 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/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 =
--
GitLab