Merge branch 'fix/andre/libc-extern-ghost' into 'master'

sync with frama-c/frama-c!1450

See merge request !160

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 ∈ [--..--]

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 ∈ [--..--]

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();

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 ∈ [--..--]

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 ∈ [--..--]

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 ∈ [--..--]

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 ∈ [--..--]

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 ∈ [--..--]

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 ∈ [--..--]

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 ∈ [--..--]

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 ∈ [--..--]

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 ∈ [--..--]

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 ∈ [--..--]

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 ∈ [--..--]

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 ∈ [--..--]

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 ∈ [--..--]

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 ∈ [--..--]

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 ∈ [--..--]

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 ∈ [--..--]

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 ∈ [--..--]