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 4d486a49cd8eb0c3b09bb3f5258e2f836da613ef..b3b6d35f87250dcc5d580196ddee27980b40a344 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 bf1c19354434a4585a2954a6ac1ed4b174e500a7..274b6b9ec54b0231de237cd4c1061542ce9353fa 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 0cd4db839235c22e8903b96f60dff58b5a1b560b..4152ed586ac940c1681f9742677887ded54225f9 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