diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
index a904b504644e2050f2ed6de2844b0b3c2bcb3a4f..6ba8601ad60881832d2940b1fac9459522071a9e 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.res.oracle
@@ -6,4 +6,4 @@ tests/bts/bts1307.i:11:[e-acsl] warning: approximating a real number by a float
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] user error: type long double wider than 64 bits not supported.
- Using double instead for the remainder of the analysis.
+ Using double instead for the remainder of the analysis.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle
index 028bc0d2c2db0310d0f97cc889f03820f8046dbe..8ecce2ff208f3a57061487b3ce946e6c1ee14ee5 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle
@@ -1,10 +1,10 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
tests/bts/bts1395.i:8:[value] warning: detected recursive call
- (__gen_e_acsl_fact <- fact :: tests/bts/bts1395.i:6 <-
- __gen_e_acsl_fact :: tests/bts/bts1395.i:12 <-
- main)
- Use -val-ignore-recursive-calls to ignore (beware this will make the analysis
- unsound)
+ (__gen_e_acsl_fact <- fact :: tests/bts/bts1395.i:6 <-
+ __gen_e_acsl_fact :: tests/bts/bts1395.i:12 <-
+ main)
+ Use -val-ignore-recursive-calls to ignore (beware this will make the analysis
+ unsound)
[value] user error: Degeneration occurred:
- results are not correct for lines of code that can be reached from the degeneration point.
+ results are not correct for lines of code that can be reached from the degeneration point.
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle
index 46b779f7c6ab6bc1a73df2e015cd2e5afeeb5fa6..d9f6e43c01cd9702f50b14eefc81fa89f676be39 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts1740.res.oracle
@@ -3,4 +3,4 @@
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/bts/bts1740.i:12:[value] warning: locals {a} escaping the scope of a block of main through p
tests/bts/bts1740.i:16:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&p);
+ assert ¬\dangling(&p);
diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
index 133c3ba4e2253b9187c16942b0d96cc44289d8d3..fd4f79bbeeddfce2d1453e31edd9e45174ec8964 100644
--- a/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle
@@ -1,6 +1,6 @@
[e-acsl] beginning translation.
[e-acsl] warning: annotating undefined function `atoi':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
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 560ddd4e17b9118068f868734e6d6ae93c9d01cd..b7c475fe776d9f35bc9d91ee32e5bf88a091e63c 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
@@ -17,5 +17,5 @@ tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float
[value] using specification for function __e_acsl_memory_init
[value] using specification for function __e_acsl_assert
[value] user error: type long double wider than 64 bits not supported.
- Using double instead for the remainder of the analysis.
+ Using double instead for the remainder of the analysis.
[value] done for function main
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 23514bf035f716bdbb120e743dfd1e96614cf312..778f507241c801c74cbd4656363dedc8f0dd6f48 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
@@ -24,7 +24,7 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: preco
[value] using specification for function __gmpz_get_ui
[value] using specification for function __gmpz_init_set_ui
[value] user error: type long double wider than 64 bits not supported.
- Using double instead for the remainder of the analysis.
+ Using double instead for the remainder of the analysis.
tests/gmp/cast.i:23:[value] warning: accessing out of bounds index. assert 0 ≤ __gen_e_acsl_cast_9;
tests/gmp/cast.i:23:[value] warning: accessing out of bounds index. assert __gen_e_acsl_cast_9 < 2;
[value] done for function main
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 3c70303a9bfb4c27f19ad45f2a55bae461214810..b4467de16fb2b2b57c53897f1da85d0cb32a215b 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
@@ -14,8 +14,8 @@
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
[value] using specification for function __e_acsl_memory_init
tests/gmp/longlong.i:9:[value] user error: recursive call during value analysis
- of my_pow (my_pow <- my_pow :: tests/gmp/longlong.i:16 <- main). Assuming
- the call has no effect. The analysis will be unsound.]
+ of my_pow (my_pow <- my_pow :: tests/gmp/longlong.i:16 <- main). Assuming
+ the call has no effect. The analysis will be unsound.]
[value] using specification for function my_pow
tests/gmp/longlong.i:10:[value] warning: signed overflow. assert -2147483648 ≤ tmp * tmp;
tests/gmp/longlong.i:10:[value] warning: signed overflow. assert tmp * tmp ≤ 2147483647;
@@ -31,8 +31,8 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: preco
[value] using specification for function __gmpz_tdiv_r
[value] using specification for function __gmpz_get_si
tests/gmp/longlong.i:17:[value] Assigning imprecise value to __gen_e_acsl__4.
- The imprecision originates from Library function
+ The imprecision originates from Library function
tests/gmp/longlong.i:17:[value] warning: pointer comparison.
- assert \pointer_comparable((void *)__gen_e_acsl__4, (void *)1);
+ assert \pointer_comparable((void *)__gen_e_acsl__4, (void *)1);
[value] using specification for function __gmpz_clear
[value] done for function main
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 f898b78327d7230006c219ea978e4e024db0bde2..7770261972fae1b2eff21a15ce5f145ea9150cbd 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
@@ -14,8 +14,8 @@
__e_acsl_math_INFINITY ∈ [-1.79769313486e+308 .. 1.79769313486e+308]
[value] using specification for function __e_acsl_memory_init
tests/gmp/longlong.i:9:[value] user error: recursive call during value analysis
- of my_pow (my_pow <- my_pow :: tests/gmp/longlong.i:16 <- main). Assuming
- the call has no effect. The analysis will be unsound.]
+ of my_pow (my_pow <- my_pow :: tests/gmp/longlong.i:16 <- main). Assuming
+ the call has no effect. The analysis will be unsound.]
[value] using specification for function my_pow
tests/gmp/longlong.i:10:[value] warning: signed overflow. assert -2147483648 ≤ tmp * tmp;
tests/gmp/longlong.i:10:[value] warning: signed overflow. assert tmp * tmp ≤ 2147483647;
@@ -30,8 +30,8 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp_api.h:100:[value] warning: function __gmpz_import
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
[value] using specification for function __gmpz_tdiv_r
tests/gmp/longlong.i:17:[value] Assigning imprecise value to __gen_e_acsl_eq.
- The imprecision originates from Library function
+ The imprecision originates from Library function
tests/gmp/longlong.i:17:[value] warning: pointer comparison.
- assert \pointer_comparable((void *)__gen_e_acsl_eq, (void *)0);
+ assert \pointer_comparable((void *)__gen_e_acsl_eq, (void *)0);
[value] using specification for function __gmpz_clear
[value] done for function main
diff --git a/src/plugins/e-acsl/tests/no-main/oracle/empty.res.oracle b/src/plugins/e-acsl/tests/no-main/oracle/empty.res.oracle
index 80488f4bb315531cbdf54bcf412367700688d8d4..352c228e7c566ad78fb1526dda5f7b015197ce53 100644
--- a/src/plugins/e-acsl/tests/no-main/oracle/empty.res.oracle
+++ b/src/plugins/e-acsl/tests/no-main/oracle/empty.res.oracle
@@ -3,7 +3,7 @@
[kernel] Parsing tests/no-main/empty.i (no preprocessing)
[e-acsl] beginning translation.
[e-acsl] warning: cannot find entry point `main'.
- Please use option `-main' for specifying a valid entry point.
- The generated program may miss memory instrumentation
- if there are memory-related annotations.
+ Please use option `-main' for specifying a valid entry point.
+ The generated program may miss memory instrumentation
+ if there are memory-related annotations.
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
index eb06d443b20bdb58bed9cacd44fa8e9402f2bb49..c9a941f7a21d5877116ba7de20bd22041f2bb2dc 100644
--- a/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/reject/oracle/quantif.res.oracle
@@ -2,37 +2,37 @@
[kernel] Parsing FRAMAC_SHARE/e-acsl/e_acsl.h (with preprocessing)
[kernel] Parsing tests/reject/quantif.i (no preprocessing)
tests/reject/quantif.i:6:[e-acsl] warning: E-ACSL construct `unguarded \forall quantification' is not yet supported.
- Ignoring annotation.
+ Ignoring annotation.
tests/reject/quantif.i:7:[e-acsl] warning: invalid E-ACSL construct
- `invalid guard x ≡ 1 in quantification ∀ ℤ x; x ≡ 1 ⇒ x ≥ 0'.
- Ignoring annotation.
+ `invalid guard x ≡ 1 in quantification ∀ ℤ x; x ≡ 1 ⇒ x ≥ 0'.
+ Ignoring annotation.
tests/reject/quantif.i:8:[e-acsl] warning: invalid E-ACSL construct
- `missing upper-bound for variable x in quantification ∀ int x; 0 ≤ x ⇒ x ≥ 0'.
- Ignoring annotation.
+ `missing upper-bound for variable x in quantification ∀ int x; 0 ≤ x ⇒ x ≥ 0'.
+ Ignoring annotation.
tests/reject/quantif.i:9:[e-acsl] warning: invalid E-ACSL construct
- `non integer variable x in quantification ∀ float x; 0 ≤ x ≤ 3 ⇒ x ≥ 0'.
- Ignoring annotation.
+ `non integer variable x in quantification ∀ float x; 0 ≤ x ≤ 3 ⇒ x ≥ 0'.
+ Ignoring annotation.
tests/reject/quantif.i:10:[e-acsl] warning: invalid E-ACSL construct
- `unguarded variable y in quantification
- ∀ ℤ x, ℤ y; 0 ≤ x ≤ 3 ⇒ x ≥ 0'.
- Ignoring annotation.
+ `unguarded variable y in quantification
+ ∀ ℤ x, ℤ y; 0 ≤ x ≤ 3 ⇒ x ≥ 0'.
+ Ignoring annotation.
tests/reject/quantif.i:11:[e-acsl] warning: invalid E-ACSL construct
- `too much constraint(s) in quantification ∀ ℤ x; 0 ≤ x ≤ 3 ∧ 0 ≤ z ≤ 3 ⇒ x ≥ 0'.
- Ignoring annotation.
+ `too much constraint(s) in quantification ∀ ℤ x; 0 ≤ x ≤ 3 ∧ 0 ≤ z ≤ 3 ⇒ x ≥ 0'.
+ Ignoring annotation.
tests/reject/quantif.i:12:[e-acsl] warning: invalid E-ACSL construct
- `invalid guard (0 ≤ x ≤ 3) ∨ (0 ≤ y ≤ 3) in quantification
- ∀ ℤ x, ℤ y; (0 ≤ x ≤ 3) ∨ (0 ≤ y ≤ 3) ⇒ x ≥ 0'.
- Ignoring annotation.
+ `invalid guard (0 ≤ x ≤ 3) ∨ (0 ≤ y ≤ 3) in quantification
+ ∀ ℤ x, ℤ y; (0 ≤ x ≤ 3) ∨ (0 ≤ y ≤ 3) ⇒ x ≥ 0'.
+ Ignoring annotation.
tests/reject/quantif.i:13:[e-acsl] warning: invalid E-ACSL construct
- `invalid binder x + 1 in quantification ∀ int x; 0 ≤ x + 1 ≤ 3 ⇒ x ≥ 0'.
- Ignoring annotation.
+ `invalid binder x + 1 in quantification ∀ int x; 0 ≤ x + 1 ≤ 3 ⇒ x ≥ 0'.
+ Ignoring annotation.
tests/reject/quantif.i:14:[e-acsl] warning: invalid E-ACSL construct
- `too much constraint(s) in quantification ∀ ℤ x; 0 ≤ x < 10 ∧ 9 ≤ x < 20 ⇒ x > z'.
- Ignoring annotation.
+ `too much constraint(s) in quantification ∀ ℤ x; 0 ≤ x < 10 ∧ 9 ≤ x < 20 ⇒ x > z'.
+ Ignoring annotation.
tests/reject/quantif.i:15:[e-acsl] warning: invalid E-ACSL construct
- `invalid binder y in quantification
- ∀ ℤ x, ℤ z, ℤ y;
- 0 ≤ x < 2 ∧ 0 ≤ y < 5 ∧ 0 ≤ z ≤ y ⇒ x + z ≤ y + 1'.
- Ignoring annotation.
+ `invalid binder y in quantification
+ ∀ ℤ x, ℤ z, ℤ y;
+ 0 ≤ x < 2 ∧ 0 ≤ y < 5 ∧ 0 ≤ z ≤ y ⇒ x + z ≤ y + 1'.
+ Ignoring annotation.
[e-acsl] 9 annotations were ignored, being untypable.
[e-acsl] 1 annotation was ignored, being unsupported.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
index 729d83e4e818868e3e973e48b2c2a788cbd49737..fb79cdc60f5e835b8ddd42b063bdef8dcdc1db7c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle
@@ -1,9 +1,9 @@
[e-acsl] beginning translation.
[e-acsl] warning: annotating undefined function `isupper':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
tests/runtime/ctype_macros.c:39:[e-acsl] warning: E-ACSL construct `disjoint behaviors' is not yet supported.
- Ignoring annotation.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/libc/ctype.h:164:[value] warning: function __gen_e_acsl_isupper: precondition got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle
index b37801b0973650db7f7135c7051681e9b39cbba9..3f4c2a5e8fdf5b8cac214435f90233ed6ded203c 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/early_exit.res.oracle
@@ -3,33 +3,33 @@
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/early_exit.c:14:[value] warning: locals {a} escaping the scope of a block of goto_bts through p
tests/runtime/early_exit.c:18:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&p);
+ assert ¬\dangling(&p);
tests/runtime/early_exit.c:37:[value] warning: locals {a2} escaping the scope of a block of goto_valid through q
tests/runtime/early_exit.c:37:[value] warning: locals {a3} escaping the scope of a block of goto_valid through r
tests/runtime/early_exit.c:47:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&q);
+ assert ¬\dangling(&q);
tests/runtime/early_exit.c:48:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&r);
+ assert ¬\dangling(&r);
tests/runtime/early_exit.c:50:[value] warning: locals {a1} escaping the scope of a block of goto_valid through p
tests/runtime/early_exit.c:56:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&p);
+ assert ¬\dangling(&p);
tests/runtime/early_exit.c:57:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&q);
+ assert ¬\dangling(&q);
tests/runtime/early_exit.c:58:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&r);
+ assert ¬\dangling(&r);
tests/runtime/early_exit.c:79:[value] warning: locals {a1} escaping the scope of a block of switch_valid through p
tests/runtime/early_exit.c:79:[value] warning: locals {a2} escaping the scope of a block of switch_valid through q
tests/runtime/early_exit.c:87:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&q);
+ assert ¬\dangling(&q);
tests/runtime/early_exit.c:88:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&p);
+ assert ¬\dangling(&p);
tests/runtime/early_exit.c:103:[value] warning: locals {a1} escaping the scope of a block of while_valid through p
tests/runtime/early_exit.c:103:[value] warning: locals {a2} escaping the scope of a block of while_valid through q
tests/runtime/early_exit.c:116:[value] warning: accessing uninitialized left-value. assert \initialized(&p);
tests/runtime/early_exit.c:116:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&p);
+ assert ¬\dangling(&p);
tests/runtime/early_exit.c:117:[value] warning: accessing uninitialized left-value. assert \initialized(&q);
tests/runtime/early_exit.c:117:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&q);
+ assert ¬\dangling(&q);
tests/runtime/early_exit.c:99:[value] warning: locals {a0} escaping the scope of a block of while_valid through r
[scope:rm_asserts] removing 5 assertion(s)
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.res.oracle
index 537cc4f4abfd448619f4698b21c6de8791f80b19..88f409e29672882f8e8dad43bed8720a5061ecfc 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/hidden_malloc.res.oracle
@@ -3,4 +3,4 @@ tests/runtime/hidden_malloc.c:11:[kernel] warning: Calling undeclared function r
tests/runtime/hidden_malloc.c:11:[kernel] warning: Neither code nor specification for function realpath, generating default assigns from the prototype
[e-acsl] translation done in project "e-acsl".
tests/runtime/hidden_malloc.c:11:[value] warning: Completely invalid destination for assigns clause *((char *)x_1 + (0 ..)).
- Ignoring.
+ Ignoring.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
index d7a840a8dc17f28ee570606415d6837d0ecc6f06..dee7ed535006155a87063f244e8b989a5985ef8e 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle
@@ -1,18 +1,18 @@
[e-acsl] beginning translation.
[e-acsl] warning: annotating undefined function `printf_va_1':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
[e-acsl] warning: annotating undefined function `printf_va_2':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
[e-acsl] warning: annotating undefined function `printf_va_3':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
tests/runtime/local_goto.c:37:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
+ Ignoring annotation.
tests/runtime/local_goto.c:28:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
+ Ignoring annotation.
tests/runtime/local_goto.c:16:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle
index 6797f7632014916d58fc3ef8b124c4bb9f246c86..d62a15cccbd332be7664cc7022ac90c0dca29d80 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/loop.res.oracle
@@ -3,4 +3,4 @@
tests/runtime/loop.i:19:[value] warning: loop invariant got status unknown.
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status invalid.
tests/runtime/loop.i:19:[value] warning: accessing uninitialized left-value.
- assert \initialized(&t[__gen_e_acsl_k_2][__gen_e_acsl_l_2]);
+ assert \initialized(&t[__gen_e_acsl_k_2][__gen_e_acsl_l_2]);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
index 3454430c79cbe2d6c29ffa49ffd0447dc45c1673..409d36f4d6a5e126f4feeeb21667ec8a380da18a 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle
@@ -1,13 +1,13 @@
[e-acsl] beginning translation.
[e-acsl] warning: annotating undefined function `strlen':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
+ Ignoring annotation.
FRAMAC_SHARE/libc/string.h:92:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
+ Ignoring annotation.
FRAMAC_SHARE/libc/string.h:94:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/mainargs.c:12:[value] warning: assertion got status unknown.
@@ -18,7 +18,7 @@ tests/runtime/mainargs.c:16:[value] warning: assertion got status unknown.
tests/runtime/mainargs.c:16:[value] warning: out of bounds read. assert \valid_read(argv + argc);
FRAMAC_SHARE/libc/string.h:92:[value] warning: function __gen_e_acsl_strlen: precondition 'valid_string_src' got status unknown.
FRAMAC_SHARE/libc/string.h:92:[value] warning: builtin Frama_C_strlen: possibly reading indeterminate data
- invalid base: NULL
+ invalid base: NULL
FRAMAC_SHARE/libc/string.h:94:[value] warning: function __gen_e_acsl_strlen: postcondition got status unknown.
tests/runtime/mainargs.c:19:[value] warning: assertion got status unknown.
tests/runtime/mainargs.c:20:[value] warning: assertion got status unknown.
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle
index 3489e4d7c7ee2c023b29fad9f063e7034f548369..a759f44c4bf541540813b22346c0ea8d534a2fd6 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/valid.res.oracle
@@ -2,4 +2,4 @@
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/valid.c:47:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&a);
+ assert ¬\dangling(&a);
diff --git a/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle
index 5855c1110d6124665566981e912dab0597f6136f..99b074f02e9afe58d0ab70f3045b050f26eabb40 100644
--- a/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/runtime/oracle/valid_alias.res.oracle
@@ -2,6 +2,6 @@
[e-acsl] translation done in project "e-acsl".
FRAMAC_SHARE/e-acsl/e_acsl.h:94:[value] warning: function __e_acsl_assert: precondition got status unknown.
tests/runtime/valid_alias.c:17:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&a);
+ assert ¬\dangling(&a);
tests/runtime/valid_alias.c:17:[value] warning: accessing left-value that contains escaping addresses.
- assert ¬\dangling(&b);
+ assert ¬\dangling(&b);
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
index 729b206a280d975fbd74c1c5aac3fab77aa9acb3..b2a10e6e5e22e0944edea1b94a9d91aa895df397 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle
@@ -1,7 +1,7 @@
[e-acsl] beginning translation.
[e-acsl] warning: annotating undefined function `getenv':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
FRAMAC_SHARE/libc/stdlib.h:407:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
index ba226e9e6d64d59137ba1b53851efda350850aa8..1adfbf4c3325a5ac415b0ba674c6c4237c8c2c29 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle
@@ -1,7 +1,7 @@
[e-acsl] beginning translation.
[e-acsl] warning: annotating undefined function `printf_va_1':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
tests/temporal/t_malloc-asan.c:31:[e-acsl] warning: E-ACSL construct `logic function application' is not yet supported.
- Ignoring annotation.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
index 1004081d7dd9d5733a7ceab69a2dd5b760f4baae..caf187356b86b329a85cb8fec3cf23af87b9f4c0 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_memcpy.res.oracle
@@ -1,25 +1,25 @@
[e-acsl] beginning translation.
[e-acsl] warning: annotating undefined function `memcpy':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
[e-acsl] warning: annotating undefined function `memset':
- the generated program may miss memory instrumentation
- if there are memory-related annotations.
+ the generated program may miss memory instrumentation
+ if there are memory-related annotations.
FRAMAC_SHARE/libc/string.h:60:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/string.h:82:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/string.h:82:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
+ Ignoring annotation.
FRAMAC_SHARE/libc/string.h:85:[e-acsl] warning: E-ACSL construct `user-defined logic type' is not yet supported.
- Ignoring annotation.
+ Ignoring annotation.
FRAMAC_SHARE/libc/string.h:85:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
+ Ignoring annotation.
FRAMAC_SHARE/libc/string.h:60:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/string.h:61:[e-acsl] warning: E-ACSL construct `trange' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/string.h:62:[e-acsl] warning: E-ACSL construct `\separated' is not yet supported. Ignoring annotation.
FRAMAC_SHARE/libc/string.h:62:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
+ Ignoring annotation.
FRAMAC_SHARE/libc/string.h:65:[e-acsl] warning: E-ACSL construct `logic function returning an integer' is not yet supported.
- Ignoring annotation.
+ Ignoring annotation.
FRAMAC_SHARE/libc/string.h:65:[e-acsl] warning: E-ACSL construct `assigns clause in behavior' is not yet supported.
- Ignoring annotation.
+ Ignoring annotation.
[e-acsl] translation done in project "e-acsl".