diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle index 08feacb630fdf2abef302c28b4c47a1de830036c..cc9d1544cc9598fd1457d711f92627bc1858500f 100644 --- a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle +++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.0.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle index 08feacb630fdf2abef302c28b4c47a1de830036c..cc9d1544cc9598fd1457d711f92627bc1858500f 100644 --- a/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle +++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/addrOf.1.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c b/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c index 722d228580232fc73932d84fcc911560fe4de039..229e759e39255fa63c6ea07db035c9351fff7eb0 100644 --- a/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c +++ b/src/plugins/e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c @@ -31,16 +31,8 @@ void __e_acsl_globals_init(void) { __e_acsl_store_block((void *)(& f),(size_t)1); __e_acsl_full_init((void *)(& f)); - __e_acsl_store_block((void *)(& __fc_wctomb_state),(size_t)4); - __e_acsl_full_init((void *)(& __fc_wctomb_state)); - __e_acsl_store_block((void *)(& __fc_mbtowc_state),(size_t)4); - __e_acsl_full_init((void *)(& __fc_mbtowc_state)); - __e_acsl_store_block((void *)(& __fc_mblen_state),(size_t)4); - __e_acsl_full_init((void *)(& __fc_mblen_state)); __e_acsl_store_block((void *)(& __fc_rand_max),(size_t)8); __e_acsl_full_init((void *)(& __fc_rand_max)); - __e_acsl_store_block((void *)(& __fc_random_counter),(size_t)4); - __e_acsl_full_init((void *)(& __fc_random_counter)); return; } @@ -60,11 +52,7 @@ int main(void) __e_acsl_full_init((void *)(& __retres)); __retres = 0; __e_acsl_delete_block((void *)(& f)); - __e_acsl_delete_block((void *)(& __fc_wctomb_state)); - __e_acsl_delete_block((void *)(& __fc_mbtowc_state)); - __e_acsl_delete_block((void *)(& __fc_mblen_state)); __e_acsl_delete_block((void *)(& __fc_rand_max)); - __e_acsl_delete_block((void *)(& __fc_random_counter)); __e_acsl_delete_block((void *)(& x)); __e_acsl_delete_block((void *)(& __retres)); __e_acsl_memory_clean(); diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle index 7a7fac17de4bda89f62034d0a7b9cb709e89e0c1..ca8cdb6dbb22320274fed0d8401b7a10f334b925 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle index d71a528c82c2df4f1a7159373bf3a7d81835e5b4..17fae168ee445f09a2d44a7a2060f47c118a3499 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle index 5220932a16679d71e6d92c1723ade4c7e601e203..d4a3fccd1d867115e1e9d7d58b70ead56302e3b8 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle index 89d29cade4ed5821497d27243792d1d44dcbdbf7..aa13ba6cb09ab9cb4f636760ee71d52551d4ae97 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle index eb6f872f382f44ed7fc83054a999d126e783b15d..5e56d54261b621a3e05c50019ecfae52e772a12d 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle index 6342f94cbdd429e15dd6309f6146fe219281938b..e912d362dda88d4ac5df1e55a80888c66f7d24da 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle index a54a14a8d905f603467f074c9a0f52b334b157d1..560ddd4e17b9118068f868734e6d6ae93c9d01cd 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.0.res.oracle @@ -6,12 +6,8 @@ tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle index 2787673575ff20e67ed4e9704a2ab92b3ca8b272..23514bf035f716bdbb120e743dfd1e96614cf312 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle @@ -6,12 +6,8 @@ tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle index 34c9ac44d75ab2f77051a22b6f6ab2d5000bcac5..83a041c13b5ca36f8d3b4beb9ecf6fe2ab1cadf0 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/comparison.0.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle index 79c6428f81559e7c8a336de3a4b2d69a8e7d09dc..0e02b9b04f642f5717e683a55be658a1f0253a6c 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/comparison.1.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle index 728aaa6eb8371cc8dbc840fbc756b56eeb6096ee..b80db4bd9d02d0d1f7bb800af038908dcce8a20c 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle index 5378a45bc88035d8eb5c7afb8d8637dfdc1c9347..6624797a92967d977d9701b954141a979ece270e 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle index b686a7f8196e46d86ea33da15c44328366d9b4ce..3c70303a9bfb4c27f19ad45f2a55bae461214810 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.0.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle index 9ee43edefef20d9ea5cdd84c645f6b375bc54bc1..f898b78327d7230006c219ea978e4e024db0bde2 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/longlong.1.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle index 34c9ac44d75ab2f77051a22b6f6ab2d5000bcac5..83a041c13b5ca36f8d3b4beb9ecf6fe2ab1cadf0 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle index 354a68bdcd8a47e1e27c3761959b0638c8b4317d..1f738410a4f1d041bcb75a1e246840765779f98d 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle index dbe7f04a981ae6776d75e0718635c11b7ea55c02..9686892d0e0dfb4aa926f2774cb9a64da8773f92 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.0.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle index 2d7d54f28bf4e15c73a19f933e76bd0ac27cc9d2..f8ba551c18d90c9739197789abc98489ed8340fd 100644 --- a/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle +++ b/src/plugins/e-acsl/tests/gmp/oracle/quantif.1.res.oracle @@ -4,12 +4,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ {0} __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ {0} - __fc_mbtowc_state ∈ {0} - __fc_wctomb_state ∈ {0} __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--] diff --git a/src/plugins/e-acsl/tests/runtime/oracle/local_init.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/local_init.res.oracle index fd269ac1affddae520aa3997f145ab0abc6d09c7..434eada8b3132bfa3a1a5c48f39b2eedeaf67a82 100644 --- a/src/plugins/e-acsl/tests/runtime/oracle/local_init.res.oracle +++ b/src/plugins/e-acsl/tests/runtime/oracle/local_init.res.oracle @@ -5,12 +5,8 @@ [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization - __fc_random_counter ∈ [--..--] __fc_rand_max ∈ {32767} __fc_heap_status ∈ [--..--] - __fc_mblen_state ∈ [--..--] - __fc_mbtowc_state ∈ [--..--] - __fc_wctomb_state ∈ [--..--] __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __e_acsl_heap_allocation_size ∈ [--..--]