diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle index 9f073f5d7095bc8b2c505b23058942df66c7a815..077c0847b439ca7600c915855d19bbb51961a4d7 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.res.oracle @@ -3,4 +3,4 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. tests/bts/bts1390.c:13:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) 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:[kernel] warning: out of bounds read. assert \valid_read(s); +tests/bts/bts1390.c:18:[value] warning: out of bounds read. assert \valid_read(s); diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle index b151b39e10cf77d06f108e19998a6c830cfb0fb5..405331f98680e027a0576313cda743797c89e2b9 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.res.oracle @@ -1,4 +1,4 @@ [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. -tests/bts/bts1837.i:18:[kernel] warning: signed overflow. assert -2147483648 ≤ i-1; +tests/bts/bts1837.i:18:[value] warning: signed overflow. assert -2147483648 ≤ i-1; diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle index 90fbfd1130c2b5e048471e38a4bce05c37bc5e0a..92a368f6c4c61e29f65c159d4b5d98303b582fda 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.res.oracle @@ -20,4 +20,4 @@ FRAMAC_SHARE/libc/stdlib.h:166:[e-acsl] warning: E-ACSL construct `logic functio Ignoring annotation. [e-acsl] translation done in project "e-acsl". tests/e-acsl-runtime/freeable.c:15:[value] warning: assertion got status unknown. -tests/e-acsl-runtime/freeable.c:15:[kernel] warning: accessing uninitialized left-value. assert \initialized(&p); +tests/e-acsl-runtime/freeable.c:15:[value] warning: accessing uninitialized left-value. assert \initialized(&p); diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle index 8a6001896bd90475ee5d2d619ff1b4c66f8b1e07..5887eacd77314809fefcb034bc02189a4190bd9e 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/initialized.res.oracle @@ -55,11 +55,11 @@ tests/e-acsl-runtime/initialized.c:74:[value] warning: assertion got status unkn tests/e-acsl-runtime/initialized.c:76:[value] warning: assertion got status unknown. FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:181:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:179:[kernel] warning: pointer comparison. assert \pointer_comparable(p, (void *)0); -FRAMAC_SHARE/libc/stdlib.h:178:[kernel] warning: pointer comparison. assert \pointer_comparable(p, (void *)0); +FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: pointer comparison. assert \pointer_comparable(p, (void *)0); +FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: pointer comparison. assert \pointer_comparable(p, (void *)0); tests/e-acsl-runtime/initialized.c:84:[value] warning: assertion got status unknown. tests/e-acsl-runtime/initialized.c:85:[value] warning: assertion got status unknown. tests/e-acsl-runtime/initialized.c:93:[value] warning: assertion got status unknown. tests/e-acsl-runtime/initialized.c:96:[value] warning: assertion got status unknown. -tests/e-acsl-runtime/initialized.c:107:[kernel] warning: out of bounds write. assert \valid(partsi+i); -tests/e-acsl-runtime/initialized.c:105:[kernel] warning: out of bounds write. assert \valid(partsc+i); +tests/e-acsl-runtime/initialized.c:107:[value] warning: out of bounds write. assert \valid(partsi+i); +tests/e-acsl-runtime/initialized.c:105:[value] warning: out of bounds write. assert \valid(partsc+i); 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 3880f6950b8127776107a1d4671b61e68c2f6697..5994e51e92e1fa1c126abf3a651a4cb3525b1021 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 @@ -2,5 +2,5 @@ [e-acsl] translation done in project "e-acsl". tests/e-acsl-runtime/loop.i:19:[value] warning: loop invariant got status unknown. FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status invalid. -tests/e-acsl-runtime/loop.i:19:[kernel] warning: accessing uninitialized left-value. - assert \initialized(&t[__gen_e_acsl_k_2][__gen_e_acsl_l_2]); +tests/e-acsl-runtime/loop.i:19:[value] warning: accessing uninitialized left-value. + assert \initialized(&t[__gen_e_acsl_k_2][__gen_e_acsl_l_2]); diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle index c9394915eb1300cf3c0211a66782edc9e8d3a811..b07a36e39225cf9eb1e0267e1460cab0d17160d4 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.res.oracle @@ -13,9 +13,9 @@ FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: preco tests/e-acsl-runtime/mainargs.c:12:[value] warning: assertion got status unknown. tests/e-acsl-runtime/mainargs.c:13:[value] warning: assertion got status unknown. tests/e-acsl-runtime/mainargs.c:15:[value] warning: assertion got status unknown. -tests/e-acsl-runtime/mainargs.c:15:[kernel] warning: out of bounds read. assert \valid_read(argv+argc); +tests/e-acsl-runtime/mainargs.c:15:[value] warning: out of bounds read. assert \valid_read(argv+argc); tests/e-acsl-runtime/mainargs.c:16:[value] warning: assertion got status unknown. -tests/e-acsl-runtime/mainargs.c:16:[kernel] warning: out of bounds read. assert \valid_read(argv+argc); +tests/e-acsl-runtime/mainargs.c:16:[value] warning: out of bounds read. assert \valid_read(argv+argc); FRAMAC_SHARE/libc/string.h:91:[value] warning: function __gen_e_acsl_strlen: precondition 'valid_string_src' got status unknown. FRAMAC_SHARE/libc/string.h:91:[value] warning: function strlen: precondition 'valid_string_src' got status unknown. FRAMAC_SHARE/libc/string.h:93:[value] warning: function __gen_e_acsl_strlen: postcondition got status unknown. 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 006ce91f496a1b9116396f5cd1587c07f0de0c2a..58ac8f9ec263aedb884fab195d28b86043c3b8ee 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 @@ -24,5 +24,5 @@ FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, be FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. FRAMAC_SHARE/libc/stdlib.h:181:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown. -tests/e-acsl-runtime/valid.c:47:[kernel] warning: accessing left-value that contains escaping addresses. - assert ¬\dangling(&a); +tests/e-acsl-runtime/valid.c:47:[value] warning: accessing left-value that contains escaping addresses. + assert ¬\dangling(&a); 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 22951efd584ac785e47d460a5ddbd3430db4f264..ddcd452f35a42c71a7be228433dd1d13fbf454a9 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 @@ -24,7 +24,7 @@ FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, be FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. FRAMAC_SHARE/libc/stdlib.h:181:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown. -tests/e-acsl-runtime/valid_alias.c:17:[kernel] warning: accessing left-value that contains escaping addresses. - assert ¬\dangling(&a); -tests/e-acsl-runtime/valid_alias.c:17:[kernel] warning: accessing left-value that contains escaping addresses. - assert ¬\dangling(&b); +tests/e-acsl-runtime/valid_alias.c:17:[value] warning: accessing left-value that contains escaping addresses. + assert ¬\dangling(&a); +tests/e-acsl-runtime/valid_alias.c:17:[value] warning: accessing left-value that contains escaping addresses. + assert ¬\dangling(&b); 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 70d2c3e40bc0e027a217ba3436c65548f631ee24..2a5c2bd025e734b8bf6f3b0b8aaef30f1081a84c 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 @@ -1,4 +1,4 @@ [e-acsl] beginning translation. [e-acsl] translation done in project "e-acsl". FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/valid_in_contract.c:19:[kernel] warning: out of bounds read. assert \valid_read(&l->next); +tests/e-acsl-runtime/valid_in_contract.c:19:[value] warning: out of bounds read. assert \valid_read(&l->next); 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 c27dbd9bb0282333fd49e5ee52cc39dc4e0152ca..c8caafe3a835c5698624fbf343efc71cffb06193 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 @@ -24,6 +24,6 @@ FRAMAC_SHARE/libc/stdlib.h:164:[value] warning: function __gen_e_acsl_malloc, be FRAMAC_SHARE/libc/stdlib.h:169:[value] warning: function __gen_e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/vector.c:27:[value] warning: assertion got status unknown. tests/e-acsl-runtime/vector.c:28:[value] warning: assertion got status unknown. -tests/e-acsl-runtime/vector.c:28:[kernel] warning: accessing uninitialized left-value. assert \initialized(&LAST); +tests/e-acsl-runtime/vector.c:28:[value] warning: accessing uninitialized left-value. assert \initialized(&LAST); FRAMAC_SHARE/libc/stdlib.h:179:[value] warning: function __gen_e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. FRAMAC_SHARE/libc/stdlib.h:181:[value] warning: function __gen_e_acsl_free, behavior deallocation: postcondition got status unknown. 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 55900b4ce3381bb9cc84ce48b2dfe54971182987..2aa07b37357093db836cc8fd0bba2338c8cbac00 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 @@ -16,8 +16,8 @@ tests/gmp/longlong.i:9:[value] warning: recursive call during value analysis [value] user error: Recursive call on an unspecified function. Using potentially invalid inferred assigns 'assigns \result \from x, n;' [value] using specification for function my_pow -tests/gmp/longlong.i:10:[kernel] warning: signed overflow. assert -2147483648 ≤ tmp*tmp; -tests/gmp/longlong.i:10:[kernel] warning: signed overflow. assert tmp*tmp ≤ 2147483647; +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; [value] using specification for function __gmpz_init_set_si [value] using specification for function __gmpz_init [value] using specification for function __gmpz_import @@ -29,7 +29,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:88:[value] warning: function __gmpz_import: pre FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_tdiv_r [value] using specification for function __gmpz_get_ui -tests/gmp/longlong.i:17:[kernel] warning: pointer comparison. - assert \pointer_comparable((void *)__gen_e_acsl__4, (void *)1); +tests/gmp/longlong.i:17:[value] warning: pointer comparison. + 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 4950add02acdad3a3fd33cc3b7f810819e5e874c..cb8aca989bc7fc910a4eb1769f247bbca1069822 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 @@ -16,8 +16,8 @@ tests/gmp/longlong.i:9:[value] warning: recursive call during value analysis [value] user error: Recursive call on an unspecified function. Using potentially invalid inferred assigns 'assigns \result \from x, n;' [value] using specification for function my_pow -tests/gmp/longlong.i:10:[kernel] warning: signed overflow. assert -2147483648 ≤ tmp*tmp; -tests/gmp/longlong.i:10:[kernel] warning: signed overflow. assert tmp*tmp ≤ 2147483647; +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; [value] using specification for function __gmpz_init_set_si [value] using specification for function __gmpz_init [value] using specification for function __gmpz_import @@ -28,7 +28,7 @@ FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:88:[value] warning: function __gmpz_import: pre [value] using specification for function __e_acsl_assert FRAMAC_SHARE/e-acsl/e_acsl.h:43:[value] warning: function __e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_tdiv_r -tests/gmp/longlong.i:17:[kernel] warning: pointer comparison. - assert \pointer_comparable((void *)__gen_e_acsl_eq, (void *)0); +tests/gmp/longlong.i:17:[value] warning: pointer comparison. + assert \pointer_comparable((void *)__gen_e_acsl_eq, (void *)0); [value] using specification for function __gmpz_clear [value] done for function main