From b9129b0d5f00aeea8656533c9ff347dc8edf3b6c Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Thu, 30 Aug 2018 16:15:25 +0200
Subject: [PATCH] [visit] improve test stability
---
.../tests/temporal/oracle/gen_t_global_init.c | 16 ++++++++--------
.../tests/temporal/oracle/gen_t_local_init.c | 14 +++++++-------
src/plugins/e-acsl/visit.ml | 3 ++-
3 files changed, 17 insertions(+), 16 deletions(-)
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c
index 4d486a49cd8..b3b6d35f872 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_global_init.c
@@ -83,14 +83,6 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& extra_lbits));
__e_acsl_store_block((void *)(strings),(size_t)32);
__e_acsl_full_init((void *)(& strings));
- __e_acsl_temporal_store_nblock((void *)(& strings[0][0]),
- (void *)__gen_e_acsl_literal_string_4);
- __e_acsl_temporal_store_nblock((void *)(& strings[0][1]),
- (void *)__gen_e_acsl_literal_string_3);
- __e_acsl_temporal_store_nblock((void *)(& strings[1][0]),
- (void *)__gen_e_acsl_literal_string_2);
- __e_acsl_temporal_store_nblock((void *)(& strings[1][1]),
- (void *)__gen_e_acsl_literal_string);
__e_acsl_temporal_store_nblock((void *)(& descs2[0].desc.extra_bits),
(void *)(extra_lbits));
__e_acsl_temporal_store_nblock((void *)(& descs2[1].desc.extra_bits),
@@ -103,6 +95,14 @@ void __e_acsl_globals_init(void)
(void *)(extra_lbits));
__e_acsl_temporal_store_nblock((void *)(& l_desc.extra_bits),
(void *)(extra_lbits));
+ __e_acsl_temporal_store_nblock((void *)(& strings[0][0]),
+ (void *)__gen_e_acsl_literal_string_4);
+ __e_acsl_temporal_store_nblock((void *)(& strings[0][1]),
+ (void *)__gen_e_acsl_literal_string_3);
+ __e_acsl_temporal_store_nblock((void *)(& strings[1][0]),
+ (void *)__gen_e_acsl_literal_string_2);
+ __e_acsl_temporal_store_nblock((void *)(& strings[1][1]),
+ (void *)__gen_e_acsl_literal_string);
return;
}
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c
index bf1c1935443..274b6b9ec54 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_local_init.c
@@ -84,6 +84,13 @@ void __e_acsl_globals_init(void)
__e_acsl_full_init((void *)(& Str));
__e_acsl_store_block((void *)(Strings),(size_t)32);
__e_acsl_full_init((void *)(& Strings));
+ __e_acsl_temporal_store_nblock((void *)(Str),
+ (void *)__gen_e_acsl_literal_string_5);
+ __e_acsl_temporal_store_nblock((void *)(& Str[1]),
+ (void *)__gen_e_acsl_literal_string_6);
+ __e_acsl_temporal_store_nblock((void *)(& Str[2]),
+ (void *)__gen_e_acsl_literal_string_7);
+ __e_acsl_temporal_store_nblock((void *)(& Str[3]),(void *)0);
__e_acsl_temporal_store_nblock((void *)(& Strings[0][0]),
(void *)__gen_e_acsl_literal_string);
__e_acsl_temporal_store_nblock((void *)(& Strings[0][1]),
@@ -92,13 +99,6 @@ void __e_acsl_globals_init(void)
(void *)__gen_e_acsl_literal_string_3);
__e_acsl_temporal_store_nblock((void *)(& Strings[1][1]),
(void *)__gen_e_acsl_literal_string_4);
- __e_acsl_temporal_store_nblock((void *)(Str),
- (void *)__gen_e_acsl_literal_string_5);
- __e_acsl_temporal_store_nblock((void *)(& Str[1]),
- (void *)__gen_e_acsl_literal_string_6);
- __e_acsl_temporal_store_nblock((void *)(& Str[2]),
- (void *)__gen_e_acsl_literal_string_7);
- __e_acsl_temporal_store_nblock((void *)(& Str[3]),(void *)0);
return;
}
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 0cd4db83923..4152ed586ac 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -393,7 +393,8 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
(* Make a unique mapping for each global variable omitting initializers.
Initializers (used to capture literal strings) are added to
[global_vars] via the [vinit] visitor method (see comments below). *)
- Varinfo.Hashtbl.replace global_vars vi (NoOffset, None)
+ Varinfo.Hashtbl.replace global_vars
+ (Cil.get_original_varinfo self#behavior vi) (NoOffset, None)
| _ -> ());
if generate then Cil.DoChildrenPost(fun g -> List.iter do_it g; g)
else Cil.DoChildren
--
GitLab