From e71091a9ca0ead57020e46d4cdd789e658c9f1df Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 4 Sep 2017 10:13:53 +0200
Subject: [PATCH] sync with frama-c/frama-c!1450
---
.../tests/full-mmodel/oracle/addrOf.0.res.oracle | 4 ----
.../tests/full-mmodel/oracle/addrOf.1.res.oracle | 4 ----
.../e-acsl/tests/full-mmodel/oracle/gen_addrOf2.c | 12 ------------
.../e-acsl/tests/gmp/oracle/arith.0.res.oracle | 4 ----
.../e-acsl/tests/gmp/oracle/arith.1.res.oracle | 4 ----
.../e-acsl/tests/gmp/oracle/array.0.res.oracle | 4 ----
.../e-acsl/tests/gmp/oracle/array.1.res.oracle | 4 ----
src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle | 4 ----
src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle | 4 ----
.../e-acsl/tests/gmp/oracle/cast.0.res.oracle | 4 ----
.../e-acsl/tests/gmp/oracle/cast.1.res.oracle | 4 ----
.../e-acsl/tests/gmp/oracle/comparison.0.res.oracle | 4 ----
.../e-acsl/tests/gmp/oracle/comparison.1.res.oracle | 4 ----
.../tests/gmp/oracle/integer_constant.0.res.oracle | 4 ----
.../tests/gmp/oracle/integer_constant.1.res.oracle | 4 ----
.../e-acsl/tests/gmp/oracle/longlong.0.res.oracle | 4 ----
.../e-acsl/tests/gmp/oracle/longlong.1.res.oracle | 4 ----
src/plugins/e-acsl/tests/gmp/oracle/not.0.res.oracle | 4 ----
src/plugins/e-acsl/tests/gmp/oracle/not.1.res.oracle | 4 ----
.../e-acsl/tests/gmp/oracle/quantif.0.res.oracle | 4 ----
.../e-acsl/tests/gmp/oracle/quantif.1.res.oracle | 4 ----
.../tests/runtime/oracle/local_init.res.oracle | 4 ----
22 files changed, 96 deletions(-)
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 08feacb630f..cc9d1544cc9 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 08feacb630f..cc9d1544cc9 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 722d2285802..229e759e392 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 7a7fac17de4..ca8cdb6dbb2 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 d71a528c82c..17fae168ee4 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 5220932a166..d4a3fccd1d8 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 89d29cade4e..aa13ba6cb09 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 eb6f872f382..5e56d54261b 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 6342f94cbdd..e912d362dda 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 a54a14a8d90..560ddd4e17b 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 2787673575f..23514bf035f 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 34c9ac44d75..83a041c13b5 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 79c6428f815..0e02b9b04f6 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 728aaa6eb83..b80db4bd9d0 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 5378a45bc88..6624797a929 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 b686a7f8196..3c70303a9bf 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 9ee43edefef..f898b78327d 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 34c9ac44d75..83a041c13b5 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 354a68bdcd8..1f738410a4f 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 dbe7f04a981..9686892d0e0 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 2d7d54f28bf..f8ba551c18d 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 fd269ac1aff..434eada8b31 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 ∈ [--..--]
--
GitLab