diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
index aa55f57b68134ef0a070c2ae4cd0c628ccd2c1b6..8773d06ed290564424e11540514804e9eebfaf49 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
@@ -30,11 +30,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- m ∈ {123}
- u ∈ {{ &m }}
- p ∈ {{ &m }}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- x ∈ {0}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
index aa55f57b68134ef0a070c2ae4cd0c628ccd2c1b6..8773d06ed290564424e11540514804e9eebfaf49 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
@@ -30,11 +30,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- m ∈ {123}
- u ∈ {{ &m }}
- p ∈ {{ &m }}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- x ∈ {0}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
index e826a10252a3a1bdb0909e5c58324cce61475777..569a317907e7f9aab1d46042885b2014b4362df1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
@@ -86,7 +86,3 @@ tests/e-acsl-runtime/arith.i:33:[value] Assertion got status valid.
tests/e-acsl-runtime/arith.i:33:[value] Assertion 'E_ACSL' got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {-3}
- y ∈ {2}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
index a5f2cd71f27149d57400f1777193cf673a8548ac..9d33b17f15c80b5d11a490afe61a39ec975c897c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
@@ -38,7 +38,3 @@ tests/e-acsl-runtime/arith.i:32:[value] Assertion got status valid.
tests/e-acsl-runtime/arith.i:33:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {-3}
- y ∈ {2}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
index 1d3b8f7c04285a7dc6061fc6ef0e560abf3f185a..c4cd42d3ae35fc9d4cfce2c56dce80914ccd9f5a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
@@ -26,9 +26,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
tests/e-acsl-runtime/array.i:16:[value] Assertion got status unknown.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- T1[0] ∈ {0; 2}
- [1..2] ∈ {0; 1; 2}
- T2[0] ∈ {0; 2}
- [1..3] ∈ {0; 2; 4; 6}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
index 3f7c1963f285d06a41ac690fe7974e04d432199b..9c76d866663413b10e9f8f114ecebc8c8ec97b64 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
@@ -35,9 +35,3 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition
tests/e-acsl-runtime/array.i:16:[value] Assertion got status unknown.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- T1[0] ∈ {0; 2}
- [1..2] ∈ {0; 1; 2}
- T2[0] ∈ {0; 2}
- [1..3] ∈ {0; 2; 4; 6}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
index 8a0364192b24c50194edeea6b6a9209abb1de4e3..a05225b59c2b51b21a4b7a4df1d2309f0bb992cc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
@@ -69,23 +69,3 @@ tests/e-acsl-runtime/at.i:34:[value] Assertion got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- A ∈ {3}
-[value] Values at end of function __e_acsl_f:
- A ∈ {3}
-[value] Values at end of function g:
- A ∈ {4}
- x ∈ {1}
- t[0] ∈ {2}
- [1] ∈ {3}
-[value] Values at end of function h:
-
-[value] Values at end of function __e_acsl_h:
- __retres ∈ {0}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- A ∈ {4}
- x ∈ {1}
- t[0] ∈ {2}
- [1] ∈ {3}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
index 4e633188c05c140c99a7f219a8164bab2e20a8e1..8ca19010e11def8602dfc4499bd820c5a8bfd5d6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
@@ -50,23 +50,3 @@ tests/e-acsl-runtime/at.i:34:[value] Assertion got status unknown.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- A ∈ {3}
-[value] Values at end of function __e_acsl_f:
- A ∈ {3}
-[value] Values at end of function g:
- A ∈ {4}
- x ∈ {1}
- t[0] ∈ {2}
- [1] ∈ {3}
-[value] Values at end of function h:
-
-[value] Values at end of function __e_acsl_h:
- __retres ∈ {0}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- A ∈ {4}
- x ∈ {1}
- t[0] ∈ {2}
- [1] ∈ {3}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
index 6640da36b1de2062b307aa4394be39325ec2fc37..1cb0bf21feee957d0b26b19af49cb87774a2d836 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.1.res.oracle
@@ -29,10 +29,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function read_sensor_4:
- buf[0..11] ∈ {0} or UNINITIALIZED
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- buf[0..11] ∈ {0}
- i ∈ {3}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
index 6640da36b1de2062b307aa4394be39325ec2fc37..1cb0bf21feee957d0b26b19af49cb87774a2d836 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1304.res.oracle
@@ -29,10 +29,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function read_sensor_4:
- buf[0..11] ∈ {0} or UNINITIALIZED
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- buf[0..11] ∈ {0}
- i ∈ {3}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
index 313e9f7afd2640fbbefb125363601592b5dd115b..11f4a771e503959f8b6d755970047c6696f39b99 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.1.res.oracle
@@ -7,9 +7,7 @@
tests/e-acsl-runtime/bts1307.i:16:[kernel] warning: Floating-point constant 0.4 is not represented exactly. Will use 0x1.999999999999ap-2. See documentation for option -warn-decimal-float
[e-acsl] beginning translation.
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating type `real' by `long double'
-tests/e-acsl-runtime/bts1307.i:13:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
tests/e-acsl-runtime/bts1307.i:31:[e-acsl] warning: approximating a real number by a float
-tests/e-acsl-runtime/bts1307.i:25:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
[e-acsl] translation done in project "e-acsl".
[value] Analyzing a complete application starting at main
[value] Computing initial state
@@ -78,17 +76,3 @@ tests/e-acsl-runtime/bts1307.i:25:[value] Function __e_acsl_bar, behavior UnderE
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function bar:
- h ∈ 0.850000023842
-[value] Values at end of function __e_acsl_bar:
- h ∈ 0.850000023842
-[value] Values at end of function foo:
- h ∈ 6.
-[value] Values at end of function __e_acsl_foo:
- h ∈ 6.
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- f ∈ 1.
- g ∈ 1.
- h ∈ 0.850000023842
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
index 7fb4f34d14f2996792046ee15a2cdc4e8f82a143..c95f7403f103385006cadb955431868b56e91d4a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1307.res.oracle
@@ -39,9 +39,10 @@ tests/e-acsl-runtime/bts1307.i:13:[value] Function foo, behavior OverEstimate_Mo
FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h:93:[value] Function __valid_read: postcondition got status unknown.
FRAMAC_SHARE/e-acsl/memory_model/e_acsl_mmodel.h:94:[value] Function __valid_read: postcondition got status valid.
[value] user error: type long double not implemented. Using double instead
-tests/e-acsl-runtime/bts1307.i:13:[kernel] warning: non-finite long double value ({5}):
+tests/e-acsl-runtime/bts1307.i:13:[kernel] warning: non-finite float value ([-1.79769313486e+308 .. 1.79769313486e+308]):
assert
- \is_finite((long double)(5-(long double)((long double)((int)(5/80)**__e_acsl_at_3)*0.4)));
+ \is_finite((float)(*__e_acsl_at_2+(int)(5-(long double)((float)((int)
+ (5/80)**__e_acsl_at_3)*0.4))));
tests/e-acsl-runtime/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: postcondition got status valid.
tests/e-acsl-runtime/bts1307.i:19:[value] Function __e_acsl_bar: precondition got status valid.
tests/e-acsl-runtime/bts1307.i:20:[value] Function __e_acsl_bar: precondition got status valid.
@@ -55,17 +56,3 @@ tests/e-acsl-runtime/bts1307.i:25:[value] Function __e_acsl_bar, behavior UnderE
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function bar:
- h ∈ 0.850000023842
-[value] Values at end of function __e_acsl_bar:
- h ∈ 0.850000023842
-[value] Values at end of function foo:
- h ∈ 6.
-[value] Values at end of function __e_acsl_foo:
- h ∈ 6.
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- f ∈ 1.
- g ∈ 1.
- h ∈ 0.850000023842
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
index 026e16c244010f1a71e5db78c0b1ce7d34d2554d..a0f5710bcda77b74c67ac9821ca225f04536b2bc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.1.res.oracle
@@ -56,16 +56,3 @@ tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function sorted:
- b ∈ [7..15]
- __retres ∈ {1}
-[value] Values at end of function __e_acsl_sorted:
- __retres ∈ {1}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- t[0] ∈ {1}
- [1..2] ∈ {4}
- [3..5] ∈ {5}
- [6] ∈ {7}
- n ∈ {1}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
index 613e574254946e4d0b93b43de63833a9a0961b6f..5198e195ed67fc7eda5dea85cba26ba56834c582 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1324.res.oracle
@@ -33,16 +33,3 @@ tests/e-acsl-runtime/bts1324.i:25:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function sorted:
- b ∈ [7..15]
- __retres ∈ {1}
-[value] Values at end of function __e_acsl_sorted:
- __retres ∈ {1}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- t[0] ∈ {1}
- [1..2] ∈ {4}
- [3..5] ∈ {5}
- [6] ∈ {7}
- n ∈ {1}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
index d151fa8905a88fbafefb01860c4fa7fa73aaa87d..94b221716daf90eab26c0e7259816c5521b19358 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.1.res.oracle
@@ -47,16 +47,3 @@ tests/e-acsl-runtime/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAv
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function atp_NORMAL_computeAverageAccel:
- av ∈ {3}
-[value] Values at end of function __e_acsl_atp_NORMAL_computeAverageAccel:
- av ∈ {3}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- Accel[0] ∈ {1}
- [1] ∈ {2}
- [2] ∈ {3}
- [3] ∈ {4}
- [4] ∈ {5}
- av ∈ {3}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.res.oracle
index 9ed71ba6232aaff0f960a2a8afe3e5b5531718c1..8b2fe09a5f901796791e0841111f940111880a5d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1326.res.oracle
@@ -30,16 +30,3 @@ tests/e-acsl-runtime/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAv
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function atp_NORMAL_computeAverageAccel:
- av ∈ {3}
-[value] Values at end of function __e_acsl_atp_NORMAL_computeAverageAccel:
- av ∈ {3}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- Accel[0] ∈ {1}
- [1] ∈ {2}
- [2] ∈ {3}
- [3] ∈ {4}
- [4] ∈ {5}
- av ∈ {3}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
index 028cb57255608543f6bc8184f1d686c8129249db..dc531550cdff23b075f2d377071f2700715ac96f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.1.res.oracle
@@ -43,12 +43,3 @@ tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function memchr:
- i ∈ {0; 1; 2; 3; 4}
- s ∈ {{ "toto" + {0; 1} ; "tata" + [0..--] }}
- __retres ∈ {{ NULL ; "toto" + {1} }}
-[value] Values at end of function __e_acsl_memchr:
- __retres ∈ {{ NULL ; "toto" + {1} }}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
index 0b0259f7ab258eb7b2d027e2afefcbe2a4232e2e..46aa73f9818f096f0bf51a498d50f13b74652f56 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1390.res.oracle
@@ -68,12 +68,3 @@ tests/e-acsl-runtime/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function memchr:
- i ∈ {0; 1; 2; 3; 4}
- s ∈ {{ "toto" + {0; 1} ; "tata" + [0..--] }}
- __retres ∈ {{ NULL ; "toto" + {1} }}
-[value] Values at end of function __e_acsl_memchr:
- __retres ∈ {{ NULL ; "toto" + {1} }}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
index cadee1883c3509fe1e61ec9a0546730c30f77fba..9fabd606e3d99a7d88e5530f4031c4767f4eed31 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.1.res.oracle
@@ -56,16 +56,3 @@
[value] using specification for function printf
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- t[0] ∈ {1}
- [1] ∈ {2}
- i ∈ {1}
- __retres ∈ {0}
- S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
- [--..--]
- [0].__fc_inode ∈
- {{ NULL + [--..--] ; &S___fc_inode_0_S___fc_stdout }}
- [1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
- [--..--]
- [1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
index cadee1883c3509fe1e61ec9a0546730c30f77fba..9fabd606e3d99a7d88e5530f4031c4767f4eed31 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1398.res.oracle
@@ -56,16 +56,3 @@
[value] using specification for function printf
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- t[0] ∈ {1}
- [1] ∈ {2}
- i ∈ {1}
- __retres ∈ {0}
- S___fc_stdout[0]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
- [--..--]
- [0].__fc_inode ∈
- {{ NULL + [--..--] ; &S___fc_inode_0_S___fc_stdout }}
- [1]{.__fc_stdio_id; .__fc_maxsz; .__fc_writepos; .__fc_readpos; .__fc_is_a_socket; .mode} ∈
- [--..--]
- [1].__fc_inode ∈ {{ NULL ; &S___fc_inode_1_S___fc_stdout }}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
index 4c1213eb840d30863063e4c66ba5fb61baf931a9..f7a92f10fe02cd370707b466427d43aad3bff7f8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.1.res.oracle
@@ -49,14 +49,3 @@ FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior dealloca
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- state ∈ ESCAPINGADDR
- __retres ∈ {0}
- Frama_C_alloc[0..447] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
index 0622734bb26295a8c7ace30649e88d49a7250f2e..e40384a482a3450a6851c2d7c812b61ed5f5e022 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1399.res.oracle
@@ -68,14 +68,3 @@ FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior dealloca
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- state ∈ ESCAPINGADDR
- __retres ∈ {0}
- Frama_C_alloc[0..447] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
index 825a55c515611b4f4f42e8c530fdfb19e473edae..88faa36b80d7f2a69c4c19bdb84e3051c989ddd5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.1.res.oracle
@@ -45,12 +45,3 @@ tests/e-acsl-runtime/bts1478.c:12:[value] Function loop: precondition got status
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_memory_init:
-
-[value] Values at end of function loop:
-
-[value] Values at end of function __e_acsl_loop:
-
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
index c65806558f44ebe0dde2d95c1207390c7e0eb547..a4cfba3e7c9abdf1656fd04df066ccd813ffec48 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/bts1478.res.oracle
@@ -36,12 +36,3 @@ tests/e-acsl-runtime/bts1478.c:12:[value] Function loop: precondition got status
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_memory_init:
-
-[value] Values at end of function loop:
-
-[value] Values at end of function __e_acsl_loop:
-
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
index 368529f6a90fa6c348385ddd4c1659e58bd7525b..0da47a198a90721a75da06ca0b05437ce1359b48 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle
@@ -40,23 +40,3 @@ tests/e-acsl-runtime/call.c:12:[value] Function __e_acsl_f: postcondition got st
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc ; &Frama_C_alloc_0 }}
-[value] Values at end of function f:
- Frama_C_alloc[bits 0 to 31] ∈ {1}
- Frama_C_alloc_0[bits 0 to 31] ∈ {1} or UNINITIALIZED
-[value] Values at end of function __e_acsl_f:
- __retres ∈ {{ &x }}
- Frama_C_alloc[bits 0 to 31] ∈ {1}
- Frama_C_alloc_0[bits 0 to 31] ∈ {1} or UNINITIALIZED
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- x ∈ {0}
- p ∈ {{ &x }}
- q ∈ {{ &x }}
- r ∈ {{ &Frama_C_alloc_0 }}
- __retres ∈ {0}
- Frama_C_alloc[bits 0 to 31] ∈ {1}
- Frama_C_alloc_0[bits 0 to 31] ∈ {1}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
index 368529f6a90fa6c348385ddd4c1659e58bd7525b..0da47a198a90721a75da06ca0b05437ce1359b48 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.res.oracle
@@ -40,23 +40,3 @@ tests/e-acsl-runtime/call.c:12:[value] Function __e_acsl_f: postcondition got st
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc ; &Frama_C_alloc_0 }}
-[value] Values at end of function f:
- Frama_C_alloc[bits 0 to 31] ∈ {1}
- Frama_C_alloc_0[bits 0 to 31] ∈ {1} or UNINITIALIZED
-[value] Values at end of function __e_acsl_f:
- __retres ∈ {{ &x }}
- Frama_C_alloc[bits 0 to 31] ∈ {1}
- Frama_C_alloc_0[bits 0 to 31] ∈ {1} or UNINITIALIZED
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- x ∈ {0}
- p ∈ {{ &x }}
- q ∈ {{ &x }}
- r ∈ {{ &Frama_C_alloc_0 }}
- __retres ∈ {0}
- Frama_C_alloc[bits 0 to 31] ∈ {1}
- Frama_C_alloc_0[bits 0 to 31] ∈ {1}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
index 9f16f96e5d0e3e31fce3d091759f52d27423da7c..20ae38c9e7f26eb512d3e58d83ffcd8842fb3095 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
@@ -26,7 +26,3 @@ tests/e-acsl-runtime/cast.i:19:[value] Assertion got status valid.
tests/e-acsl-runtime/cast.i:20:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- y ∈ {0}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
index 6fb627ae899251df39f9bdff5a944861c4f1154e..6ed92f56e1f8572e477205c81b15a3e01f009494 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
@@ -45,7 +45,3 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: preconditio
tests/e-acsl-runtime/cast.i:20:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- y ∈ {0}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
index dc04ecac55278e05bb05a0c0ec5bc98c9b752965..6961112718f047f7c4f06bf3b3611642364f17df 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
@@ -56,8 +56,3 @@ tests/e-acsl-runtime/comparison.i:28:[value] Assertion got status valid.
tests/e-acsl-runtime/comparison.i:29:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- y ∈ {1}
- s ∈ {{ "toto" }}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
index 8cb4feb818d9c33df51178277ffa31907d93f63a..e77b42acb2e36d03b62fdca99f3e90a29a6bf80f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -40,8 +40,3 @@ tests/e-acsl-runtime/comparison.i:28:[value] Assertion got status valid.
tests/e-acsl-runtime/comparison.i:29:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- y ∈ {1}
- s ∈ {{ "toto" }}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle
index b5ed2908c38ea90f28021259436997e106a8eade..dbb2932fc8d63a050db25d1a57fa1f68a9df7a5c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle
@@ -18,6 +18,3 @@
__memory_size ∈ [--..--]
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
index b5ed2908c38ea90f28021259436997e106a8eade..dbb2932fc8d63a050db25d1a57fa1f68a9df7a5c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
@@ -18,6 +18,3 @@
__memory_size ∈ [--..--]
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
index dbe3866dbb7200d2b1550ff5668533c3f3070210..8889978e5cf55a0e35b998731cb92970b26b0bc0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
@@ -83,42 +83,3 @@ tests/e-acsl-runtime/function_contract.i:71:[value] Function __e_acsl_n, behavio
tests/e-acsl-runtime/function_contract.i:74:[value] Function __e_acsl_n, behavior b2: assumes got status invalid; postcondition not evaluated.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- X ∈ {1}
-[value] Values at end of function __e_acsl_f:
- X ∈ {1}
-[value] Values at end of function g:
- X ∈ {2}
-[value] Values at end of function __e_acsl_g:
- X ∈ {2}
-[value] Values at end of function h:
- X ∈ {3}
-[value] Values at end of function __e_acsl_h:
- X ∈ {3}
-[value] Values at end of function i:
- X ∈ {5}
-[value] Values at end of function __e_acsl_i:
- X ∈ {5}
-[value] Values at end of function j:
- X ∈ {3}
-[value] Values at end of function __e_acsl_j:
- X ∈ {3}
-[value] Values at end of function k:
- X ∈ {5}
-[value] Values at end of function __e_acsl_k:
- X ∈ {5}
-[value] Values at end of function l:
-
-[value] Values at end of function __e_acsl_l:
- __retres ∈ {5}
-[value] Values at end of function m:
- X ∈ {7}
-[value] Values at end of function __e_acsl_m:
- X ∈ {7}
-[value] Values at end of function n:
- X ∈ {8}
-[value] Values at end of function __e_acsl_n:
- X ∈ {8}
-[value] Values at end of function main:
- X ∈ {8}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
index d11a5d9f76c5c430a01dd75bcfd219cf82fcada1..874df546bf09e6439d1a878e1ac445b14f860cd8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
@@ -67,42 +67,3 @@ tests/e-acsl-runtime/function_contract.i:71:[value] Function __e_acsl_n, behavio
tests/e-acsl-runtime/function_contract.i:74:[value] Function __e_acsl_n, behavior b2: assumes got status invalid; postcondition not evaluated.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- X ∈ {1}
-[value] Values at end of function __e_acsl_f:
- X ∈ {1}
-[value] Values at end of function g:
- X ∈ {2}
-[value] Values at end of function __e_acsl_g:
- X ∈ {2}
-[value] Values at end of function h:
- X ∈ {3}
-[value] Values at end of function __e_acsl_h:
- X ∈ {3}
-[value] Values at end of function i:
- X ∈ {5}
-[value] Values at end of function __e_acsl_i:
- X ∈ {5}
-[value] Values at end of function j:
- X ∈ {3}
-[value] Values at end of function __e_acsl_j:
- X ∈ {3}
-[value] Values at end of function k:
- X ∈ {5}
-[value] Values at end of function __e_acsl_k:
- X ∈ {5}
-[value] Values at end of function l:
-
-[value] Values at end of function __e_acsl_l:
- __retres ∈ {5}
-[value] Values at end of function m:
- X ∈ {7}
-[value] Values at end of function __e_acsl_m:
- X ∈ {7}
-[value] Values at end of function n:
- X ∈ {8}
-[value] Values at end of function __e_acsl_n:
- X ∈ {8}
-[value] Values at end of function main:
- X ∈ {8}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
index 9a7d2dab63c5b174de72e989abf336da85639fef..dcd294fb4afc5e0ece3954c58c818dc80825c067 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle
@@ -38,11 +38,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_memory_init:
-
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- G ∈ {1}
- P ∈ {{ &G }}
- q ∈ {{ &G }}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.res.oracle
index 4880c72a7e85e14749a60ffd6a7e289c54aac5b3..6fd50ebee3cbf760801670709de3fc6cc76d3fdf 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.res.oracle
@@ -43,11 +43,3 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_memory_init:
-
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- G ∈ {1}
- P ∈ {{ &G }}
- q ∈ {{ &G }}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
index 9e19e37529c422f1c62465b995b15146fdc5819c..698e138073401db126311f61f0b91be02bf4e76a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
@@ -37,6 +37,3 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:76:[value] Function __gmpz_init_set_str: postco
tests/e-acsl-runtime/integer_constant.i:13:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {1}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
index a4857abe6f9d81197f0b43d57e32889bb252e6d1..060220d92e7b06ed6d268df33d92130b95aff051 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
@@ -34,6 +34,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {1}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
index 04ff90046466b51a92c84423fab6c1d953e5ddb3..1533e5e39e3616739f067690e0abc2459195902a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
@@ -31,6 +31,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
tests/e-acsl-runtime/invariant.i:10:[kernel] warning: signed overflow. assert x+i ≤ 2147483647;
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ [0..2147483647]
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
index 1a6d4d66bdc89fd5800e6cc305f661e01c378e08..248c8af9cc25e4e62f67acc9d499ca1fa27da417 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
@@ -23,6 +23,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
tests/e-acsl-runtime/invariant.i:10:[kernel] warning: signed overflow. assert x+i ≤ 2147483647;
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ [0..2147483647]
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
index 8a1f7d4ba04332505ebdfc1e155a9397b7091605..28f904648cbd8ebec2f76e80f46c6025d6152140 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
@@ -33,9 +33,3 @@ tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function __e_acsl_main: postcondit
tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function main: postcondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_main:
- X ∈ {3}
- __retres ∈ {0}
-[value] Values at end of function main:
- X ∈ {3}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
index 6bcf7ea63af06949a9ef6e2bb4f925fdf87827ff..2d59ce2eeda28b2688a5c477da19e00cd86beccc 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
@@ -24,9 +24,3 @@ tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function __e_acsl_main: postcondit
tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function main: postcondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_main:
- X ∈ {3}
- __retres ∈ {0}
-[value] Values at end of function main:
- X ∈ {3}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
index 074e28f29a4cd3a56e26e6aafc170cb13bd04185..f47b81bc824892d36499954cdbb33399819cb3d0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
@@ -56,7 +56,3 @@ tests/e-acsl-runtime/lazy.i:29:[value] Assertion got status valid.
tests/e-acsl-runtime/lazy.i:30:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- y ∈ {1}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
index 849cb66ea603dcfd402f75f0cc03102c97b0d652..c1ab49ed8ffb0793fa524787176f4d5bf15b5fad 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
@@ -39,7 +39,3 @@ tests/e-acsl-runtime/lazy.i:29:[value] Assertion got status valid.
tests/e-acsl-runtime/lazy.i:30:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- y ∈ {1}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
index f35104b955ade462f613e6c69b2194b398aea37c..27fbd7dfebdfa62fb94f156c427a4ec91c9f5e7a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
@@ -64,12 +64,3 @@ tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
tests/e-acsl-runtime/linear_search.i:36:[value] Assertion got status unknown.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function search:
- k ∈ [0..10]
- __retres ∈ {0; 1}
-[value] Values at end of function __e_acsl_search:
- __retres ∈ {0; 1}
-[value] Values at end of function main:
- A[0..9] ∈ [0..81]
- found ∈ {0}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
index 9a6166c3bcbfae6aa4fce4336e59bd949a980048..4fe509716ad4246e86b14c301e30660601419e0e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
@@ -39,12 +39,3 @@ tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
tests/e-acsl-runtime/linear_search.i:36:[value] Assertion got status unknown.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function search:
- k ∈ [0..10]
- __retres ∈ {0; 1}
-[value] Values at end of function __e_acsl_search:
- __retres ∈ {0; 1}
-[value] Values at end of function main:
- A[0..9] ∈ [0..81]
- found ∈ {0}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
index 605f709024776b1701ddf404df91ba2fc280b192..097753bfe5500cd18bdaf7dbcec91fe5ae701ab6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle
@@ -55,17 +55,3 @@ tests/e-acsl-runtime/literal_string.i:13:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_memory_init:
- T ∈ {{ "bar" }}
- S ∈ {{ "foo" }}
- S2 ∈ {{ "foo2" }}
-[value] Values at end of function f:
- G ∈ {1}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- T ∈ {{ "bar" }}
- G ∈ {1}
- S ∈ {{ "foo" }}
- S2 ∈ {{ "foo2" }}
- SS ∈ {{ "ss" }}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
index b259157367697919dbc17350ceb615e70c29f079..57c1ac1c53f48c07ba6d321893b880ef6c529417 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.res.oracle
@@ -47,17 +47,3 @@ tests/e-acsl-runtime/literal_string.i:13:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_memory_init:
- T ∈ {{ "bar" }}
- S ∈ {{ "foo" }}
- S2 ∈ {{ "foo2" }}
-[value] Values at end of function f:
- G ∈ {1}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- T ∈ {{ "bar" }}
- G ∈ {1}
- S ∈ {{ "foo" }}
- S2 ∈ {{ "foo2" }}
- SS ∈ {{ "ss" }}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
index be56602ae89929964b4dea5f8b1fbeab2cf695f1..523c06b2b3d7d263798a5ee397dacb8a9b925183 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle
@@ -42,22 +42,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc ; &Frama_C_alloc_0 }}
-[value] Values at end of function add:
- __fc_heap_status ∈ [--..--]
- new ∈ {{ &Frama_C_alloc ; &Frama_C_alloc_0 }}
- Frama_C_alloc[bits 0 to 31] ∈ {4}
- [4..7] ∈ {0}
- Frama_C_alloc_0[bits 0 to 31] ∈ {7}
- [bits 32 to 63] ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- l ∈ {{ &Frama_C_alloc_0 }}
- __retres ∈ {0}
- Frama_C_alloc[bits 0 to 31] ∈ {4}
- [4..7] ∈ {0}
- Frama_C_alloc_0[bits 0 to 31] ∈ {7}
- [bits 32 to 63] ∈ {{ &Frama_C_alloc }}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
index be56602ae89929964b4dea5f8b1fbeab2cf695f1..523c06b2b3d7d263798a5ee397dacb8a9b925183 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.res.oracle
@@ -42,22 +42,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc ; &Frama_C_alloc_0 }}
-[value] Values at end of function add:
- __fc_heap_status ∈ [--..--]
- new ∈ {{ &Frama_C_alloc ; &Frama_C_alloc_0 }}
- Frama_C_alloc[bits 0 to 31] ∈ {4}
- [4..7] ∈ {0}
- Frama_C_alloc_0[bits 0 to 31] ∈ {7}
- [bits 32 to 63] ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- l ∈ {{ &Frama_C_alloc_0 }}
- __retres ∈ {0}
- Frama_C_alloc[bits 0 to 31] ∈ {4}
- [4..7] ∈ {0}
- Frama_C_alloc_0[bits 0 to 31] ∈ {7}
- [bits 32 to 63] ∈ {{ &Frama_C_alloc }}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
index 06ca9a7373d9cc22614c82b4de86d89daed6ec9f..b4be92d36aab7d7a5cf2f56c6745ecb4d3a90277 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle
@@ -65,11 +65,3 @@ tests/e-acsl-runtime/longlong.i:19:[kernel] warning: pointer comparison:
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-tests/e-acsl-runtime/longlong.i:11:[inout] warning: During inout context analysis of my_pow:
- ignoring probable recursive call.
-[value] Values at end of function my_pow:
- tmp ∈ [--..--]
- __retres ∈ [0..4294967294],0%2
-[value] Values at end of function main:
- x ∈ [0..4294967294],0%2
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle
index daeec6d3f8586b0a39ee858c678d2bc5e8f94de5..bf00755202cf96dd00f6b71313c7465e349051df 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.res.oracle
@@ -63,11 +63,3 @@ tests/e-acsl-runtime/longlong.i:19:[kernel] warning: pointer comparison: assert
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-tests/e-acsl-runtime/longlong.i:11:[inout] warning: During inout context analysis of my_pow:
- ignoring probable recursive call.
-[value] Values at end of function my_pow:
- tmp ∈ [--..--]
- __retres ∈ [0..4294967294],0%2
-[value] Values at end of function main:
- x ∈ [0..4294967294],0%2
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
index 2034d9ebfe3153245905a0bc0bf1b8a3dd755868..67423ac21da34824d10536b7f32fe2e0792cdcfb 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle
@@ -30,43 +30,3 @@ tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing uninitialized left-va
tests/e-acsl-runtime/loop.i:28:[value] Loop invariant got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function nested_loops:
- t{[0][0..14]; [1][0]} ∈ {0}
- [1][1] ∈ {1}
- [1][2] ∈ {2}
- [1][3] ∈ {3}
- [1][4] ∈ {4}
- [1][5] ∈ {5}
- [1][6] ∈ {6}
- [1][7] ∈ {7}
- [1][8] ∈ {8}
- [1][9] ∈ {9}
- [1][10] ∈ {10}
- [1][11] ∈ {11}
- [1][12] ∈ {12}
- [1][13] ∈ {13}
- [1][14] ∈ {14}
- [2][0] ∈ {0}
- [2][1..3] ∈ [2..127]
- [2][4..14] ∈ [2..127] or UNINITIALIZED
- [3][0] ∈ [0..127] or UNINITIALIZED
- [3][1..14] ∈ [2..127] or UNINITIALIZED
- [4][0] ∈ [0..127] or UNINITIALIZED
- [4][1..14] ∈ [2..127] or UNINITIALIZED
- [5][0] ∈ [0..126] or UNINITIALIZED
- [5][1..14] ∈ [2..126] or UNINITIALIZED
- [6][0] ∈ [0..126] or UNINITIALIZED
- [6][1..14] ∈ [2..126] or UNINITIALIZED
- [7][0] ∈ [0..126] or UNINITIALIZED
- [7][1..14] ∈ [2..126] or UNINITIALIZED
- [8][0] ∈ [0..126] or UNINITIALIZED
- [8][1..14] ∈ [2..126] or UNINITIALIZED
- [9][0] ∈ [0..126] or UNINITIALIZED
- [9][1..14] ∈ [2..126] or UNINITIALIZED
- i ∈ {10}
-[value] Values at end of function simple_loop:
- sum ∈ {45}
-[value] Values at end of function unnatural_loop:
- x ∈ {5}
-[value] Values at end of function main:
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle
index a2b4b995e79e77713bf667e5e2949498e0cd0353..fe99e93ad604a53a1dc253d87d71877cdb508b34 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.res.oracle
@@ -65,82 +65,3 @@ tests/e-acsl-runtime/loop.i:21:[value] entering loop for the first time
tests/e-acsl-runtime/loop.i:28:[value] Loop invariant got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function nested_loops:
- t{[0][0..14]; [1][0]} ∈ {0}
- [1][1] ∈ {1}
- [1][2] ∈ {2}
- [1][3] ∈ {3}
- [1][4] ∈ {4}
- [1][5] ∈ {5}
- [1][6] ∈ {6}
- [1][7] ∈ {7}
- [1][8] ∈ {8}
- [1][9] ∈ {9}
- [1][10] ∈ {10}
- [1][11] ∈ {11}
- [1][12] ∈ {12}
- [1][13] ∈ {13}
- [1][14] ∈ {14}
- [2][0] ∈ {0}
- [2][1] ∈ {2}
- [2][2] ∈ {4}
- [2][3] ∈ {6}
- [2][4] ∈ {8}
- [2][5] ∈ {10}
- [2][6] ∈ {12}
- [2][7] ∈ {14}
- [2][8] ∈ {16}
- [2][9] ∈ {18}
- [2][10] ∈ {20}
- [2][11] ∈ {22}
- [2][12] ∈ {24}
- [2][13] ∈ {26}
- [2][14] ∈ {28}
- [3][0] ∈ {0}
- [3][1] ∈ {3}
- [3][2] ∈ {6}
- [3][3] ∈ {9}
- [3][4] ∈ {12}
- [3][5] ∈ {15}
- [3][6] ∈ {18}
- [3][7] ∈ {21}
- [3][8] ∈ {24}
- [3][9] ∈ {27}
- [3][10] ∈ {30}
- [3][11] ∈ {33}
- [3][12] ∈ {36}
- [3][13] ∈ {39}
- [3][14] ∈ {42}
- [4][0] ∈ {0}
- [4][1] ∈ {4}
- [4][2] ∈ {8}
- [4][3] ∈ {12}
- [4][4] ∈ {16}
- [4][5] ∈ {20}
- [4][6] ∈ {24}
- [4][7] ∈ {28}
- [4][8] ∈ {32}
- [4][9] ∈ {36}
- [4][10] ∈ {40}
- [4][11] ∈ {44}
- [4][12] ∈ {48}
- [4][13] ∈ {52}
- [4][14] ∈ {56}
- [5][0] ∈ {0}
- [5][1..5] ∈ [5..126]
- [5][6..14] ∈ [5..126] or UNINITIALIZED
- [6][0] ∈ [0..126] or UNINITIALIZED
- [6][1..14] ∈ [5..126] or UNINITIALIZED
- [7][0] ∈ [0..126] or UNINITIALIZED
- [7][1..14] ∈ [5..126] or UNINITIALIZED
- [8][0] ∈ [0..126] or UNINITIALIZED
- [8][1..14] ∈ [5..126] or UNINITIALIZED
- [9][0] ∈ [0..126] or UNINITIALIZED
- [9][1..14] ∈ [5..126] or UNINITIALIZED
- i ∈ {10}
-[value] Values at end of function simple_loop:
- sum ∈ {45}
-[value] Values at end of function unnatural_loop:
- x ∈ {5}
-[value] Values at end of function main:
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
index 278ee4bc1b8bff116481bf9683739d99b964368c..534c38767c1cd8645362e746833169ff68f58ef0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
@@ -30,7 +30,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {2}
- y ∈ {1}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
index 6557b0c429ac7391c9f0c5c56d5c64f822b1ea58..e5c231612712bc11898fb226864c4ad6769989f8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
@@ -21,7 +21,3 @@ tests/e-acsl-runtime/nested_code_annot.i:9:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {2}
- y ∈ {1}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
index b6da35609000892d9da69e1918660fe1dab97c77..c4f9ff2db62799b7b9159f7dac2d262040452bf6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
@@ -30,6 +30,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
index 92fcf287fb2ea40b466c74b7aa337a98a1a7520d..40316cdce210326a7e449a7cff78d172479c8bb1 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
@@ -21,6 +21,3 @@ tests/e-acsl-runtime/not.i:8:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
index 60f6bc168734ed245047f8c4853723bc95647ace..f166bba7846f0c090951a4f278f7b03169aa5ac7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
@@ -21,5 +21,3 @@ tests/e-acsl-runtime/null.i:8:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
index 60f6bc168734ed245047f8c4853723bc95647ace..f166bba7846f0c090951a4f278f7b03169aa5ac7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
@@ -21,5 +21,3 @@ tests/e-acsl-runtime/null.i:8:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
index a968f385f31415ce3072d64f99276dc66479b254..9693e41b97b45f946156c4528c24f62c9c2389a6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
@@ -31,5 +31,3 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition
tests/e-acsl-runtime/other_constants.i:13:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
index 15fc52ccb20f0e85eca755bc23002eb76aa19de8..2042277c0a8f2050732e392876722383565c2091 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
@@ -22,5 +22,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
tests/e-acsl-runtime/other_constants.i:13:[value] Assertion got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
index 81b8356afcf0064ed153a97db9cd5d72cfbc0c3c..73e6d73c9e85747655ac69adc60c859baf43fe3a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
@@ -70,11 +70,3 @@ tests/e-acsl-runtime/ptr.i:27:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- x ∈ {1}
- t[0] ∈ {2}
- [1] ∈ {3}
- [2] ∈ {5}
- p ∈ {{ &t + {8} }}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
index f8a7c968bfd753e3bc5f90eceb44804a4bdd5526..05ae42c747a2f119d9c47b9222799c82d34cfc0e 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
@@ -44,11 +44,3 @@ tests/e-acsl-runtime/ptr.i:27:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- x ∈ {1}
- t[0] ∈ {2}
- [1] ∈ {3}
- [2] ∈ {5}
- p ∈ {{ &t + {8} }}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
index 8750728362c06c34d6f9cbfb2065d67f2befdd53..a3038ab5ba0f1efa09b21bdfd2736bac1a78a284 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle
@@ -46,21 +46,3 @@ tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈
- {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
-[value] Values at end of function __e_acsl_memory_init:
-
-[value] Values at end of function f:
- A ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
-[value] Values at end of function g:
-
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- A ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
- B ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
- x ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
- y ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
index 8750728362c06c34d6f9cbfb2065d67f2befdd53..a3038ab5ba0f1efa09b21bdfd2736bac1a78a284 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.res.oracle
@@ -46,21 +46,3 @@ tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈
- {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
-[value] Values at end of function __e_acsl_memory_init:
-
-[value] Values at end of function f:
- A ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
-[value] Values at end of function g:
-
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- A ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
- B ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
- x ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
- y ∈ {{ NULL + [--..--] ; &alloced_return___malloc + [0..2147483647] }}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
index 6169ca8a5d392616ae1aa66b11f07fab94807949..850eee44a2a7d338f98010460b42bd9a52799e1b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
@@ -68,5 +68,3 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition g
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle
index 6186b7fcbc749f20eb5b9aacfe12bc52b6aeba7f..330bd859fb7f8cf3ce923f84646cfa6fc1efbfd5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle
@@ -36,5 +36,3 @@ tests/e-acsl-runtime/quantif.i:27:[value] entering loop for the first time
tests/e-acsl-runtime/quantif.i:28:[value] entering loop for the first time
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
index 7b7d8af08d89dba75658de97991c03df55a9d66b..0c5e00fef6d5968b29758e7038ed6876a9828a61 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
@@ -45,17 +45,3 @@ tests/e-acsl-runtime/result.i:23:[value] Function h: postcondition got status va
tests/e-acsl-runtime/result.i:23:[value] Function __e_acsl_h: postcondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- x ∈ {0}
-[value] Values at end of function __e_acsl_f:
- __retres ∈ {0}
-[value] Values at end of function g:
-
-[value] Values at end of function __e_acsl_g:
- __retres ∈ {1}
-[value] Values at end of function h:
- __retres ∈ {0}
-[value] Values at end of function __e_acsl_h:
- __retres ∈ {0}
-[value] Values at end of function main:
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
index 77fe429d401d7cad3df3dfd13a546529f0f1bb30..013d4c42c5cef6285f71387f469fa20d3f1875ce 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
@@ -27,17 +27,3 @@ tests/e-acsl-runtime/result.i:23:[value] Function h: postcondition got status va
tests/e-acsl-runtime/result.i:23:[value] Function __e_acsl_h: postcondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- x ∈ {0}
-[value] Values at end of function __e_acsl_f:
- __retres ∈ {0}
-[value] Values at end of function g:
-
-[value] Values at end of function __e_acsl_g:
- __retres ∈ {1}
-[value] Values at end of function h:
- __retres ∈ {0}
-[value] Values at end of function __e_acsl_h:
- __retres ∈ {0}
-[value] Values at end of function main:
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
index eb2ed0a97e1a678ec59cd34ba8e3b9d87fb1e6b0..46bfad9226fe20123d60264a28a512dbe349e311 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
@@ -30,6 +30,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {1}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
index 32c0062cd3d76555f805bef89617da6a72828153..f4b58164d5ef75c5651ee8ea7ceb7309d514f8c2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
@@ -21,6 +21,3 @@ tests/e-acsl-runtime/sizeof.i:10:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {1}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
index 6bd184dc25a94b636bae340669662d71f327efc8..4b5936cb9766ad46121cc2bbb62367dd1716b352 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
@@ -36,7 +36,3 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition g
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {7}
- y ∈ {2}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
index a3f17f4363580997009e87db169dac99e5c545c9..525695a8f824d26a67473e76d81e0b438f9c0454 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
@@ -20,7 +20,3 @@
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {7}
- y ∈ {2}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
index 58bbc088820e403921a75b4b7611c1578290a9e3..27bf58526758d8c8854d9eae97a5493e17af681b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
@@ -21,6 +21,3 @@ tests/e-acsl-runtime/true.i:10:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {1}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
index 58bbc088820e403921a75b4b7611c1578290a9e3..27bf58526758d8c8854d9eae97a5493e17af681b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
@@ -21,6 +21,3 @@ tests/e-acsl-runtime/true.i:10:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {1}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
index 920a2b42daff94cf0e40489a7473fd86e94d04b9..b4764b2c9632de2d531758da1914df595614883d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
@@ -34,6 +34,3 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got
FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle
index e45df4dc9cb72e545316f9fc8e477b5e847a0cfd..7d4f021a945a485ac35581c92638f1117cc43513 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle
@@ -21,6 +21,3 @@ tests/e-acsl-runtime/typedef.i:11:[value] Assertion got status valid.
FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid.
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function main:
- x ∈ {0}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
index 36eaf36d15a0633fa21c248b638e469be6692f8b..0f5e3407939aad8f0009d807943a5452eb0940e4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
@@ -94,28 +94,3 @@ tests/e-acsl-runtime/valid.c:30:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function __e_acsl_memory_init:
-
-[value] Values at end of function f:
- y ∈ {{ &n }}
-[value] Values at end of function __e_acsl_f:
- __retres ∈ {{ &n }}
-[value] Values at end of function g:
- m ∈ {123}
- u ∈ {{ &m }}
- p ∈ {{ &u }}
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- X ∈ {{ &n }}
- a ∈ ESCAPINGADDR
- b ∈ {{ &n }}
- c ∈ {{ &a }}
- d ∈ {{ &c }}
- n ∈ {0}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
index 36eaf36d15a0633fa21c248b638e469be6692f8b..0f5e3407939aad8f0009d807943a5452eb0940e4 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
@@ -94,28 +94,3 @@ tests/e-acsl-runtime/valid.c:30:[value] Assertion got status valid.
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function __e_acsl_memory_init:
-
-[value] Values at end of function f:
- y ∈ {{ &n }}
-[value] Values at end of function __e_acsl_f:
- __retres ∈ {{ &n }}
-[value] Values at end of function g:
- m ∈ {123}
- u ∈ {{ &m }}
- p ∈ {{ &u }}
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- X ∈ {{ &n }}
- a ∈ ESCAPINGADDR
- b ∈ {{ &n }}
- c ∈ {{ &a }}
- d ∈ {{ &c }}
- n ∈ {0}
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
index be90ffa809a0f04f66b9317e01435a846760eee4..44c5a9f2d391485f70dbb897e01a42c5878c9c0d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
@@ -72,16 +72,3 @@ tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for fu
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- a ∈ ESCAPINGADDR
- b ∈ ESCAPINGADDR
- n ∈ {0}
- __retres ∈ {0}
- Frama_C_alloc[0..3] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
index 32ad3893090be36211cf4aee8e05f3ccad9d1d1d..bda631e4dd693991efcefae28196a5b174711ae8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
@@ -78,16 +78,3 @@ tests/e-acsl-runtime/valid_alias.c:19:[value] all evaluations are invalid for fu
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- a ∈ ESCAPINGADDR
- b ∈ ESCAPINGADDR
- n ∈ {0}
- __retres ∈ {0}
- Frama_C_alloc[0..3] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
index 3a199ccfcaabe75e423bf22b617cc4ca515c8fd8..389e3dfbfb230c53dc7a403d78361a21cd8a30ef 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle
@@ -41,10 +41,3 @@ tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavio
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- __retres ∈ {0}
-[value] Values at end of function __e_acsl_f:
- __retres ∈ {0}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
index 3a199ccfcaabe75e423bf22b617cc4ca515c8fd8..389e3dfbfb230c53dc7a403d78361a21cd8a30ef 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.res.oracle
@@ -41,10 +41,3 @@ tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavio
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function f:
- __retres ∈ {0}
-[value] Values at end of function __e_acsl_f:
- __retres ∈ {0}
-[value] Values at end of function main:
- __e_acsl_internal_heap ∈ [--..--]
- __retres ∈ {0}
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
index 7d060f6ba8af68cbeccca1e9b2b88dcc5affbaf1..89273f9658726e0618c2cbfbf95600c47f5dc901 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle
@@ -50,24 +50,3 @@ FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior dealloca
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function new_inversed:
- __fc_heap_status ∈ [--..--]
- i ∈ {3}
- p ∈ {{ &Frama_C_alloc }}
- Frama_C_alloc[bits 0 to 95]# ∈ {1; 2; 3} or UNINITIALIZED repeated %32
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- LAST ∈ {1; 2; 3} or UNINITIALIZED
- x ∈ {3}
- v1[0] ∈ {1}
- [1] ∈ {2}
- [2] ∈ {3}
- v2 ∈ ESCAPINGADDR
- __retres ∈ {0}
- Frama_C_alloc[0..11] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
index bf837c6ed6de48ef378928b2eb178829388aa68f..11a76f188546b277e2d87996a7d238ac4c7690b0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.res.oracle
@@ -59,24 +59,3 @@ FRAMAC_SHARE/libc/stdlib.h:144:[value] Function __e_acsl_free, behavior dealloca
[value] using specification for function __e_acsl_memory_clean
[value] done for function main
[value] ====== VALUES COMPUTED ======
-[value] Values at end of function __e_acsl_free:
- __fc_heap_status ∈ [--..--]
-[value] Values at end of function __e_acsl_malloc:
- __fc_heap_status ∈ [--..--]
- __retres ∈ {{ &Frama_C_alloc }}
-[value] Values at end of function new_inversed:
- __fc_heap_status ∈ [--..--]
- i ∈ {3}
- p ∈ {{ &Frama_C_alloc }}
- Frama_C_alloc[bits 0 to 95]# ∈ {1; 2; 3} or UNINITIALIZED repeated %32
-[value] Values at end of function main:
- __fc_heap_status ∈ [--..--]
- __e_acsl_internal_heap ∈ [--..--]
- LAST ∈ {1; 2; 3} or UNINITIALIZED
- x ∈ {3}
- v1[0] ∈ {1}
- [1] ∈ {2}
- [2] ∈ {3}
- v2 ∈ ESCAPINGADDR
- __retres ∈ {0}
- Frama_C_alloc[0..11] ∈ UNINITIALIZED
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
index a0452c1b8dd8fd2db7e55506372ab3267ff32f5d..bcf70a16ce721877a1395b4bba98fa674a28f50c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/test_config
@@ -1,2 +1,2 @@
-OPT: -check -e-acsl -then-on e-acsl -val -no-val-show-progress
-OPT: -check -e-acsl -e-acsl-gmp-only -then-on e-acsl -val -no-val-show-progress
+OPT: -check -e-acsl -then-on e-acsl -val -no-val-show-progress -no-results
+OPT: -check -e-acsl -e-acsl-gmp-only -then-on e-acsl -val -no-val-show-progress -no-results
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 0c1167636959610cf3bbd8131fa4fcfd204909ab..30e38e317385c4690fcede84848d73d65ea5cbd1 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -131,9 +131,10 @@ let join ty1 ty2 = match ty1, ty2 with
| No_integral t1, No_integral t2 when Logic_type.equal t1 t2 -> ty1
| No_integral t, ty | ty, No_integral t when Cil.isLogicRealType t -> ty
| No_integral t, _ when Cil.isLogicFloatType t -> ty1
- | No_integral _, No_integral _
- | (Z | Interv _), No_integral _
- | No_integral _, (Interv _ | Z) ->
+ | (Z | Interv _), (No_integral _ as ty)
+ | (No_integral _ as ty), (Interv _ | Z) ->
+ ty
+ | No_integral _, No_integral _ ->
Options.fatal "cannot join %a and %a"
pretty_eacsl_typ ty1
pretty_eacsl_typ ty2