Merge branch 'feature/virgile/warning-categories' into 'master'

Auxiliary MR for warning categories

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

src/plugins/e-acsl/options.mli

@@ -38,10 +38,10 @@ val parameter_states: State.t list
 
 val must_visit: unit -> bool
 
-val dkey_analysis: Log.category
-val dkey_dup: Log.category
-val dkey_translation: Log.category
-val dkey_typing: Log.category
+val dkey_analysis: category
+val dkey_dup: category
+val dkey_translation: category
+val dkey_typing: category
 
 (*
 Local Variables:

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

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-tests/bts/bts1304.i:23:[value] warning: assertion got status unknown.
+tests/bts/bts1304.i:23:[value:alarm] warning: assertion got status unknown.

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

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-tests/bts/bts1324.i:6:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/bts/bts1324.i:6:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.

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

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-tests/bts/bts1390.c:12:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/bts/bts1390.c:9:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/bts/bts1390.c:13:[value] warning: function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
-tests/bts/bts1390.c:18:[value] warning: out of bounds read. assert \valid_read(s);
+tests/bts/bts1390.c:12:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/bts/bts1390.c:9:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/bts/bts1390.c:13:[value:alarm] warning: function __gen_e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.)
+tests/bts/bts1390.c:18:[value:alarm] warning: out of bounds read. assert \valid_read(s);

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

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
 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.
+tests/bts/bts1740.i:16:[value:alarm] warning: accessing left-value that contains escaping addresses.
     assert ¬\dangling(&p);

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

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-tests/bts/bts1837.i:18:[value] warning: signed overflow. assert -2147483648 ≤ i - 1;
+tests/bts/bts1837.i:18:[value:alarm] warning: signed overflow. assert -2147483648 ≤ i - 1;

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

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-tests/bts/bts2231.i:8:[value] warning: signed overflow. assert -9223372036854775808 ≤ __gen_e_acsl__2 - 1;
-tests/bts/bts2231.i:8:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/bts/bts2231.i:8:[value:alarm] warning: signed overflow. assert -9223372036854775808 ≤ __gen_e_acsl__2 - 1;
+tests/bts/bts2231.i:8:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.

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

@@ -2,4 +2,4 @@ tests/bts/bts2252.c:22:[kernel] warning: Calling undeclared function strncpy. Ol
 [e-acsl] beginning translation.
 tests/bts/bts2252.c:22:[kernel] warning: Neither code nor specification for function strncpy, generating default assigns from the prototype
 [e-acsl] translation done in project "e-acsl".
-tests/bts/bts2252.c:17:[value] warning: out of bounds read. assert \valid_read(srcbuf + i);
+tests/bts/bts2252.c:17:[value:alarm] warning: out of bounds read. assert \valid_read(srcbuf + i);

src/plugins/e-acsl/tests/format/oracle/fprintf.res.oracle

 tests/format/fprintf.c:12:[kernel] warning: Calling undeclared function strcpy. Old style K&R code?
 tests/format/fprintf.c:13:[kernel] warning: Calling undeclared function mktemp. Old style K&R code?
 tests/format/fprintf.c:17:[kernel] warning: Calling undeclared function fork. Old style K&R code?
+tests/format/fprintf.c:24:[kernel:typing:incompatible-types-call] warning: expected 'FILE *' but got argument of type 'int *': & argc
 [e-acsl] beginning translation.
 [e-acsl] warning: annotating undefined function `exit':
     the generated program may miss memory instrumentation
@@ -93,46 +94,46 @@ tests/format/fprintf.c:17:[kernel] warning: Neither code nor specification for f
 [value] using specification for function __e_acsl_builtin_fprintf
 [value] using specification for function exit
 [value] using specification for function waitpid
-tests/format/fprintf.c:17:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status);
+tests/format/fprintf.c:17:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status);
 tests/format/signalled.h:12:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_printf, generating default assigns from the prototype
 [value] using specification for function __e_acsl_builtin_printf
 [value] using specification for function __e_acsl_delete_block
 tests/format/fprintf.c:18:[value] warning: Completely invalid destination for assigns clause *stream. Ignoring.
-tests/format/fprintf.c:18:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_0);
+tests/format/fprintf.c:18:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_0);
 [value] using specification for function fopen
-tests/format/fprintf.c:21:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_1);
+tests/format/fprintf.c:21:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_1);
 [value] using specification for function __e_acsl_valid
 [value] using specification for function __e_acsl_assert
-FRAMAC_SHARE/libc/stdio.h:87:[value] warning: function __e_acsl_assert: precondition got status unknown.
+FRAMAC_SHARE/libc/stdio.h:87:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function fclose
-tests/format/fprintf.c:23:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_2);
+tests/format/fprintf.c:23:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_2);
 tests/format/fprintf.c:24:[value] warning: Completely invalid destination for assigns clause *stream. Ignoring.
-tests/format/fprintf.c:24:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_3);
+tests/format/fprintf.c:24:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_3);
 [value] using specification for function remove
 FRAMAC_SHARE/libc/stdio.h:70:[value] warning: no 'assigns \result \from ...' clause specified for function remove
 tests/format/fprintf.c:31:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_dprintf, generating default assigns from the prototype
 [value] using specification for function __e_acsl_builtin_dprintf
-tests/format/fprintf.c:31:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_4);
-tests/format/fprintf.c:32:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_5);
+tests/format/fprintf.c:31:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_4);
+tests/format/fprintf.c:32:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_5);
 tests/format/fprintf.c:38:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_sprintf, generating default assigns from the prototype
 [value] using specification for function __e_acsl_builtin_sprintf
-tests/format/fprintf.c:38:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_6);
-tests/format/fprintf.c:39:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_7);
-tests/format/fprintf.c:40:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_8);
+tests/format/fprintf.c:38:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_6);
+tests/format/fprintf.c:39:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_7);
+tests/format/fprintf.c:40:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_8);
 tests/format/fprintf.c:41:[value] warning: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
-tests/format/fprintf.c:41:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_9);
+tests/format/fprintf.c:41:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_9);
 tests/format/fprintf.c:42:[value] warning: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
-tests/format/fprintf.c:42:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_10);
+tests/format/fprintf.c:42:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_10);
 tests/format/fprintf.c:45:[kernel] warning: Neither code nor specification for function __e_acsl_builtin_snprintf, generating default assigns from the prototype
 [value] using specification for function __e_acsl_builtin_snprintf
-tests/format/fprintf.c:45:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_11);
-tests/format/fprintf.c:46:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_12);
+tests/format/fprintf.c:45:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_11);
+tests/format/fprintf.c:46:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_12);
 tests/format/fprintf.c:47:[value] warning: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
-tests/format/fprintf.c:47:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_13);
-tests/format/fprintf.c:48:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_14);
+tests/format/fprintf.c:47:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_13);
+tests/format/fprintf.c:48:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_14);
 tests/format/fprintf.c:49:[value] warning: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
-tests/format/fprintf.c:49:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_15);
+tests/format/fprintf.c:49:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_15);
 tests/format/fprintf.c:50:[value] warning: Completely invalid destination for assigns clause *(str + (0 ..)). Ignoring.
-tests/format/fprintf.c:50:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_16);
+tests/format/fprintf.c:50:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_16);
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main

src/plugins/e-acsl/tests/format/oracle/printf.res.oracle

@@ -417,24 +417,24 @@ tests/format/printf.c:179:[kernel] warning: Neither code nor specification for f
 [value] using specification for function __e_acsl_builtin_printf
 [value] using specification for function exit
 [value] using specification for function waitpid
-tests/format/printf.c:179:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status);
+tests/format/printf.c:179:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status);
 [value] using specification for function __e_acsl_delete_block
-tests/format/printf.c:182:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_0);
-tests/format/printf.c:185:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_1);
-tests/format/printf.c:188:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_2);
+tests/format/printf.c:182:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_0);
+tests/format/printf.c:185:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_1);
+tests/format/printf.c:188:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_2);
 [value] using specification for function __e_acsl_initialize
-tests/format/printf.c:193:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_3);
-tests/format/printf.c:196:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_4);
-tests/format/printf.c:198:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_5);
-tests/format/printf.c:200:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_6);
-tests/format/printf.c:203:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_7);
-tests/format/printf.c:205:[value] warning: accessing uninitialized left-value. assert \initialized(&process_status_8);
+tests/format/printf.c:193:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_3);
+tests/format/printf.c:196:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_4);
+tests/format/printf.c:198:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_5);
+tests/format/printf.c:200:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_6);
+tests/format/printf.c:203:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_7);
+tests/format/printf.c:205:[value:alarm] warning: accessing uninitialized left-value. assert \initialized(&process_status_8);
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_init_set_ui
 [value] using specification for function __gmpz_cmp
 [value] using specification for function __gmpz_clear
 [value] using specification for function __e_acsl_assert
-tests/format/printf.c:50:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/format/printf.c:50:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __builtin_alloca
-tests/format/printf.c:51:[value] warning: function __gen_e_acsl_strcpy: precondition 'room_string' got status invalid.
+tests/format/printf.c:51:[value:alarm] warning: function __gen_e_acsl_strcpy: precondition 'room_string' got status invalid.
 [value] done for function main

src/plugins/e-acsl/tests/gmp/oracle/arith.0.res.oracle

@@ -19,13 +19,13 @@
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_cmp
 [value] using specification for function __gmpz_init
-tests/gmp/arith.i:18:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:18:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_tdiv_q
 [value] using specification for function __gmpz_get_si
 [value] using specification for function __gmpz_clear
 [value] using specification for function __gmpz_add
-tests/gmp/arith.i:34:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/arith.i:34:[value] warning: signed overflow. assert -2147483648 ≤ 1 + __gen_e_acsl__7;
-tests/gmp/arith.i:34:[value] warning: signed overflow. assert 1 + __gen_e_acsl__7 ≤ 2147483647;
-tests/gmp/arith.i:34:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:34:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:34:[value:alarm] warning: signed overflow. assert -2147483648 ≤ 1 + __gen_e_acsl__7;
+tests/gmp/arith.i:34:[value:alarm] warning: signed overflow. assert 1 + __gen_e_acsl__7 ≤ 2147483647;
+tests/gmp/arith.i:34:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] done for function main

src/plugins/e-acsl/tests/gmp/oracle/arith.1.res.oracle

@@ -19,34 +19,34 @@
 [value] using specification for function __gmpz_neg
 [value] using specification for function __gmpz_cmp
 [value] using specification for function __e_acsl_assert
-tests/gmp/arith.i:10:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:10:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_clear
-tests/gmp/arith.i:11:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:11:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_com
-tests/gmp/arith.i:12:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:12:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_add
-tests/gmp/arith.i:14:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:14:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_sub
-tests/gmp/arith.i:15:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:15:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_mul
-tests/gmp/arith.i:16:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/arith.i:17:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:16:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:17:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_tdiv_q
 [value] using specification for function __gmpz_init_set_str
-tests/gmp/arith.i:18:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/arith.i:19:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:18:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:19:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_tdiv_r
-tests/gmp/arith.i:20:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/arith.i:21:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/arith.i:23:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/arith.i:25:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/arith.i:26:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/arith.i:27:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/arith.i:28:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/arith.i:30:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/arith.i:31:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:20:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:21:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:23:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:25:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:26:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:27:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:28:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:30:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:31:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_init_set_ui
-tests/gmp/arith.i:34:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/arith.i:34:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/arith.i:36:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:34:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:34:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/arith.i:36:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] done for function main

src/plugins/e-acsl/tests/gmp/oracle/array.0.res.oracle

@@ -18,9 +18,9 @@
 [value] using specification for function __e_acsl_memory_init
 tests/gmp/array.i:10:[value] entering loop for the first time
 tests/gmp/array.i:11:[value] entering loop for the first time
-tests/gmp/array.i:13:[value] warning: assertion got status unknown.
+tests/gmp/array.i:13:[value:alarm] warning: assertion got status unknown.
 [value] using specification for function __e_acsl_assert
-tests/gmp/array.i:13:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/array.i:14:[value] warning: assertion got status unknown.
-tests/gmp/array.i:14:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/array.i:13:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/array.i:14:[value:alarm] warning: assertion got status unknown.
+tests/gmp/array.i:14:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] done for function main

src/plugins/e-acsl/tests/gmp/oracle/array.1.res.oracle

@@ -18,12 +18,12 @@
 [value] using specification for function __e_acsl_memory_init
 tests/gmp/array.i:10:[value] entering loop for the first time
 tests/gmp/array.i:11:[value] entering loop for the first time
-tests/gmp/array.i:13:[value] warning: assertion got status unknown.
+tests/gmp/array.i:13:[value:alarm] warning: assertion got status unknown.
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_cmp
 [value] using specification for function __e_acsl_assert
-tests/gmp/array.i:13:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/array.i:13:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_clear
-tests/gmp/array.i:14:[value] warning: assertion got status unknown.
-tests/gmp/array.i:14:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/array.i:14:[value:alarm] warning: assertion got status unknown.
+tests/gmp/array.i:14:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] done for function main

src/plugins/e-acsl/tests/gmp/oracle/at.0.res.oracle

@@ -20,20 +20,20 @@
 [value] using specification for function __e_acsl_delete_block
 [value] using specification for function __e_acsl_assert
 tests/gmp/at.i:12:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/gmp/at.i:12:[value] warning: assertion got status unknown.
+tests/gmp/at.i:12:[value:alarm] warning: assertion got status unknown.
 tests/gmp/at.i:14:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/gmp/at.i:14:[value] warning: assertion got status unknown.
+tests/gmp/at.i:14:[value:alarm] warning: assertion got status unknown.
 tests/gmp/at.i:48:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/gmp/at.i:48:[value] warning: assertion got status unknown.
+tests/gmp/at.i:48:[value:alarm] warning: assertion got status unknown.
 tests/gmp/at.i:49:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/gmp/at.i:49:[value] warning: assertion got status unknown.
+tests/gmp/at.i:49:[value:alarm] warning: assertion got status unknown.
 tests/gmp/at.i:50:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/gmp/at.i:50:[value] warning: assertion got status unknown.
+tests/gmp/at.i:50:[value:alarm] warning: assertion got status unknown.
 [value] using specification for function __e_acsl_initialize
 [value] using specification for function __e_acsl_valid_read
 tests/gmp/at.i:26:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/gmp/at.i:26:[value] warning: assertion got status unknown.
+tests/gmp/at.i:26:[value:alarm] warning: assertion got status unknown.
 tests/gmp/at.i:28:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/gmp/at.i:28:[value] warning: assertion got status unknown.
+tests/gmp/at.i:28:[value:alarm] warning: assertion got status unknown.
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main

src/plugins/e-acsl/tests/gmp/oracle/at.1.res.oracle

@@ -23,37 +23,37 @@
 [value] using specification for function __e_acsl_delete_block
 [value] using specification for function __gmpz_cmp
 [value] using specification for function __e_acsl_assert
-tests/gmp/at.i:35:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/at.i:35:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_init
 [value] using specification for function __gmpz_add
-tests/gmp/at.i:43:[value] warning: function __gmpz_init_set: precondition ¬\initialized(z) got status unknown.
-tests/gmp/at.i:43:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/at.i:9:[value] warning: function __gmpz_init_set: precondition ¬\initialized(z) got status unknown.
-tests/gmp/at.i:11:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/at.i:43:[value:alarm] warning: function __gmpz_init_set: precondition ¬\initialized(z) got status unknown.
+tests/gmp/at.i:43:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/at.i:9:[value:alarm] warning: function __gmpz_init_set: precondition ¬\initialized(z) got status unknown.
+tests/gmp/at.i:11:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 tests/gmp/at.i:12:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/gmp/at.i:12:[value] warning: assertion got status unknown.
-tests/gmp/at.i:12:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/at.i:13:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/at.i:12:[value:alarm] warning: assertion got status unknown.
+tests/gmp/at.i:12:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/at.i:13:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 tests/gmp/at.i:14:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/gmp/at.i:14:[value] warning: assertion got status unknown.
-tests/gmp/at.i:14:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/at.i:7:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/at.i:14:[value:alarm] warning: assertion got status unknown.
+tests/gmp/at.i:14:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/at.i:7:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 tests/gmp/at.i:48:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/gmp/at.i:48:[value] warning: assertion got status unknown.
-tests/gmp/at.i:48:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/at.i:48:[value:alarm] warning: assertion got status unknown.
+tests/gmp/at.i:48:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 tests/gmp/at.i:49:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/gmp/at.i:49:[value] warning: assertion got status unknown.
-tests/gmp/at.i:49:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/at.i:49:[value:alarm] warning: assertion got status unknown.
+tests/gmp/at.i:49:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 tests/gmp/at.i:50:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/gmp/at.i:50:[value] warning: assertion got status unknown.
-tests/gmp/at.i:50:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/at.i:50:[value:alarm] warning: assertion got status unknown.
+tests/gmp/at.i:50:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __e_acsl_initialize
 [value] using specification for function __e_acsl_valid_read
 tests/gmp/at.i:26:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/gmp/at.i:26:[value] warning: assertion got status unknown.
-tests/gmp/at.i:26:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/at.i:26:[value:alarm] warning: assertion got status unknown.
+tests/gmp/at.i:26:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 tests/gmp/at.i:28:[value] cannot evaluate ACSL term, \at() on a C label is unsupported
-tests/gmp/at.i:28:[value] warning: assertion got status unknown.
-tests/gmp/at.i:28:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/at.i:28:[value:alarm] warning: assertion got status unknown.
+tests/gmp/at.i:28:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __e_acsl_memory_clean
 [value] done for function main

src/plugins/e-acsl/tests/gmp/oracle/cast.1.res.oracle

@@ -20,16 +20,16 @@ tests/gmp/cast.i:23:[e-acsl] warning: approximating a real number by a float
 [value] using specification for function __gmpz_get_si
 [value] using specification for function __gmpz_cmp
 [value] using specification for function __e_acsl_assert
-tests/gmp/cast.i:10:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/cast.i:10:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_clear
-tests/gmp/cast.i:11:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/cast.i:13:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/cast.i:11:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/cast.i:13:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_get_ui
 [value] using specification for function __gmpz_init_set_ui
-tests/gmp/cast.i:14:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/cast.i:17:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/cast.i:18:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/cast.i:23:[value] warning: function __e_acsl_assert: precondition got status unknown.
-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;
+tests/gmp/cast.i:14:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/cast.i:17:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/cast.i:18:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/cast.i:23:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/cast.i:23:[value:alarm] warning: accessing out of bounds index. assert 0 ≤ __gen_e_acsl_cast_9;
+tests/gmp/cast.i:23:[value:alarm] 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/comparison.1.res.oracle

@@ -17,23 +17,23 @@
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_cmp
 [value] using specification for function __e_acsl_assert
-tests/gmp/comparison.i:7:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/comparison.i:7:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_clear
-tests/gmp/comparison.i:8:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/comparison.i:9:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/comparison.i:10:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/comparison.i:15:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/comparison.i:16:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/comparison.i:17:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/comparison.i:18:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/comparison.i:19:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/comparison.i:20:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/comparison.i:8:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/comparison.i:9:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/comparison.i:10:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/comparison.i:15:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/comparison.i:16:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/comparison.i:17:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/comparison.i:18:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/comparison.i:19:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/comparison.i:20:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_init
 [value] using specification for function __gmpz_neg
-tests/gmp/comparison.i:22:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/comparison.i:23:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/comparison.i:24:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/comparison.i:25:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/comparison.i:26:[value] warning: function __e_acsl_assert: precondition got status unknown.
-tests/gmp/comparison.i:27:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/comparison.i:22:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/comparison.i:23:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/comparison.i:24:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/comparison.i:25:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/comparison.i:26:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/comparison.i:27:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] done for function main

src/plugins/e-acsl/tests/gmp/oracle/integer_constant.0.res.oracle

@@ -17,6 +17,6 @@
 [value] using specification for function __e_acsl_assert
 [value] using specification for function __gmpz_init_set_str
 [value] using specification for function __gmpz_cmp
-tests/gmp/integer_constant.i:11:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/integer_constant.i:11:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_clear
 [value] done for function main

src/plugins/e-acsl/tests/gmp/oracle/integer_constant.1.res.oracle

@@ -17,11 +17,11 @@
 [value] using specification for function __gmpz_init_set_si
 [value] using specification for function __gmpz_cmp
 [value] using specification for function __e_acsl_assert
-tests/gmp/integer_constant.i:6:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/integer_constant.i:6:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_clear
-tests/gmp/integer_constant.i:8:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/integer_constant.i:8:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_init_set_ui
-tests/gmp/integer_constant.i:9:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/integer_constant.i:9:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] using specification for function __gmpz_init_set_str
-tests/gmp/integer_constant.i:11:[value] warning: function __e_acsl_assert: precondition got status unknown.
+tests/gmp/integer_constant.i:11:[value:alarm] warning: function __e_acsl_assert: precondition got status unknown.
 [value] done for function main