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 3d159d5b0bfd4b80ef3727c801b6b93a83a6967e..02532f4105b3e7af15d2cf0478812fa649f17e56 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 dca4b1cccc1ce3ed18b08bfe9ea2b879f3a27bcf..3d8a44702c8220836dfdb5bd084f263d035137d2 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 8424e6b55ae6555303c3143f404e8c9094fe5d5c..d4f061d60e78b008613560053feaee2a296d11e7 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 =