Merge branch 'feature/andre/log-fixed-prefix-length' into 'stable/sulfur'

synchronize with frama-c!1539

See merge request frama-c/e-acsl!170

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.

src/plugins/e-acsl/tests/bts/oracle/bts1395.res.oracle

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

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

src/plugins/e-acsl/tests/bts/oracle/bts2192.res.oracle

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

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

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

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

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

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".

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.

src/plugins/e-acsl/tests/runtime/oracle/ctype_macros.res.oracle

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

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)

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.

src/plugins/e-acsl/tests/runtime/oracle/local_goto.res.oracle

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

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

src/plugins/e-acsl/tests/runtime/oracle/mainargs.res.oracle

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

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

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

src/plugins/e-acsl/tests/temporal/oracle/t_getenv.res.oracle

 [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".

src/plugins/e-acsl/tests/temporal/oracle/t_malloc-asan.res.oracle

 [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".