diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle index 6c989f972cd533e02fe7e0e4334f946cfc0a5988..c9fe27e8b98a7c222f15b81a2d62ba8922e56cac 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.0.res.oracle @@ -14,9 +14,9 @@ tests/bts/bts1304.i:23:[value] entering loop for the first time [value] using specification for function __initialize [value] using specification for function __delete_block -tests/bts/bts1304.i:25:[value] Assertion got status unknown. +tests/bts/bts1304.i:25:[value] warning: assertion got status unknown. [value] using specification for function __initialized [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle index 6c989f972cd533e02fe7e0e4334f946cfc0a5988..c9fe27e8b98a7c222f15b81a2d62ba8922e56cac 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1304.1.res.oracle @@ -14,9 +14,9 @@ tests/bts/bts1304.i:23:[value] entering loop for the first time [value] using specification for function __initialize [value] using specification for function __delete_block -tests/bts/bts1304.i:25:[value] Assertion got status unknown. +tests/bts/bts1304.i:25:[value] warning: assertion got status unknown. [value] using specification for function __initialized [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle index ec68e5b94427a8453af3ec577bbf1d2523f73114..c7d6f581b9c68ae6cb484e6d6026f243808731a3 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.0.res.oracle @@ -16,20 +16,12 @@ tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float __memory_size ∈ [--..--] [value] using specification for function __store_block [value] using specification for function __full_init -tests/bts/bts1307.i:7:[value] Function __e_acsl_foo: precondition got status valid. -tests/bts/bts1307.i:8:[value] Function __e_acsl_foo: precondition got status valid. -tests/bts/bts1307.i:9:[value] Function __e_acsl_foo: precondition got status valid. [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/bts/bts1307.i:7:[value] Function foo: precondition got status valid. -tests/bts/bts1307.i:8:[value] Function foo: precondition got status valid. -tests/bts/bts1307.i:9:[value] Function foo: precondition got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __initialize [value] using specification for function __delete_block -tests/bts/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid. [value] using specification for function __valid_read [value] user error: type long double not implemented. Using double instead -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid. -tests/bts/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: no state left in which to evaluate postcondition, status not computed. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status invalid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle index 6291429ab43848435ab895b87db17f8fd383b214..3f9e8609612695c9f97ee3f4649c80771c98ff81 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1307.1.res.oracle @@ -16,45 +16,20 @@ tests/bts/bts1307.i:25:[e-acsl] warning: approximating a real number by a float __memory_size ∈ [--..--] [value] using specification for function __store_block [value] using specification for function __full_init -tests/bts/bts1307.i:7:[value] Function __e_acsl_foo: precondition got status valid. -tests/bts/bts1307.i:8:[value] Function __e_acsl_foo: precondition got status valid. -tests/bts/bts1307.i:9:[value] Function __e_acsl_foo: precondition got status valid. [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/bts/bts1307.i:7:[value] Function foo: precondition got status valid. -tests/bts/bts1307.i:8:[value] Function foo: precondition got status valid. -tests/bts/bts1307.i:9:[value] Function foo: precondition got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __initialize [value] using specification for function __delete_block -tests/bts/bts1307.i:13:[value] Function foo, behavior OverEstimate_Motoring: postcondition got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. -tests/bts/bts1307.i:13:[value] Assertion 'E_ACSL' got status valid. [value] using specification for function __gmpz_tdiv_q -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:164:[value] Function __gmpz_tdiv_q: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:166:[value] Function __gmpz_tdiv_q: precondition got status valid. [value] using specification for function __gmpz_get_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid. [value] using specification for function __valid_read [value] user error: type long double not implemented. Using double instead [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/bts/bts1307.i:13:[value] Function __e_acsl_foo, behavior OverEstimate_Motoring: postcondition got status valid. -tests/bts/bts1307.i:19:[value] Function __e_acsl_bar: precondition got status valid. -tests/bts/bts1307.i:20:[value] Function __e_acsl_bar: precondition got status valid. -tests/bts/bts1307.i:21:[value] Function __e_acsl_bar: precondition got status valid. -tests/bts/bts1307.i:19:[value] Function bar: precondition got status valid. -tests/bts/bts1307.i:20:[value] Function bar: precondition got status valid. -tests/bts/bts1307.i:21:[value] Function bar: precondition got status valid. -tests/bts/bts1307.i:25:[value] Function bar, behavior UnderEstimate_Motoring: postcondition got status unknown. -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/bts/bts1307.i:25:[value] Function __e_acsl_bar, behavior UnderEstimate_Motoring: postcondition got status unknown. +tests/bts/bts1307.i:25:[value] warning: function bar, behavior UnderEstimate_Motoring: postcondition got status unknown. +tests/bts/bts1307.i:25:[value] warning: function __e_acsl_bar, behavior UnderEstimate_Motoring: postcondition got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle index 77eafde3d46c7f39fded2b11bc8d66fb33437c99..aab4aebb68a166f0d5653a87a6cffcc5db1e3781 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.0.res.oracle @@ -15,12 +15,8 @@ tests/bts/bts1324.i:8:[value] entering loop for the first time [value] using specification for function __valid_read [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. tests/bts/bts1324.i:15:[value] entering loop for the first time -tests/bts/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] using specification for function __delete_block -tests/bts/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.) -tests/bts/bts1324.i:25:[value] Assertion got status valid. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle index 9d10a4d5f852636ce9beafcdaf0c3449ed604ec7..1b06bc092ff68a5c3c237049c724b31c6f648fbe 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1324.1.res.oracle @@ -13,36 +13,19 @@ [value] using specification for function __store_block [value] using specification for function __initialize [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_add -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid. [value] using specification for function __gmpz_set -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. tests/bts/bts1324.i:8:[value] entering loop for the first time [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function __gmpz_sub -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:150:[value] Function __gmpz_sub: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:151:[value] Function __gmpz_sub: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:152:[value] Function __gmpz_sub: precondition got status valid. [value] using specification for function __gmpz_get_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid. tests/bts/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_2); tests/bts/bts1324.i:8:[kernel] warning: out of bounds read. assert \valid_read(t+__e_acsl_i_2); tests/bts/bts1324.i:15:[value] entering loop for the first time -tests/bts/bts1324.i:9:[value] Function sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.) [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __delete_block -tests/bts/bts1324.i:9:[value] Function __e_acsl_sorted, behavior yes: postcondition got status valid. (Behavior may be inactive, no reduction performed.) -tests/bts/bts1324.i:25:[value] Assertion got status valid. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle index ec79b9e70c9f6b090b0ef42b676bb35eb3bc6414..dd5cc416639f4522e7a52ad7566bc86188debba2 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.0.res.oracle @@ -13,11 +13,8 @@ [value] using specification for function __store_block [value] using specification for function __initialize [value] using specification for function __delete_block -tests/bts/bts1326.i:10:[value] Function atp_NORMAL_computeAverageAccel: postcondition got status valid. [value] using specification for function __valid_read [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/bts/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAverageAccel: postcondition got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle index 7b216576b832623406d9095114d1fb4affb822b6..3920964dc2c217df243cf3f0df2727c81c72409c 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1326.1.res.oracle @@ -13,27 +13,13 @@ [value] using specification for function __store_block [value] using specification for function __initialize [value] using specification for function __delete_block -tests/bts/bts1326.i:10:[value] Function atp_NORMAL_computeAverageAccel: postcondition got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. [value] using specification for function __gmpz_add -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. -tests/bts/bts1326.i:11:[value] Assertion 'E_ACSL' got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_tdiv_q -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:164:[value] Function __gmpz_tdiv_q: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:166:[value] Function __gmpz_tdiv_q: precondition got status valid. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/bts/bts1326.i:10:[value] Function __e_acsl_atp_NORMAL_computeAverageAccel: postcondition got status valid. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle index c24855a7c940c62569801100e17d416737c70547..07aa4ab20e4edd8fba195c589237e0ce9c53a6b4 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.0.res.oracle @@ -18,19 +18,14 @@ tests/bts/bts1390.c:15:[value] entering loop for the first time [value] using specification for function __valid_read [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. tests/bts/bts1390.c:11:[value] entering loop for the first time tests/bts/bts1390.c:20:[value] entering loop for the first time [value] using specification for function __delete_block -tests/bts/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) -tests/bts/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +tests/bts/bts1390.c:16:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) tests/bts/bts1390.c:13:[value] entering loop for the first time [value] using specification for function __offset -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/bts/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) -tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +tests/bts/bts1390.c:16:[value] warning: function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) tests/bts/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s); -tests/bts/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) -tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle index 0dc7fb06cc0ec368a1e4b5025989f6d3029f2429..4167be2b1419df4c68742b3372e83f7be7c67621 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1390.1.res.oracle @@ -16,43 +16,26 @@ [value] using specification for function __full_init [value] using specification for function __literal_string [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_set -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. tests/bts/bts1390.c:15:[value] entering loop for the first time [value] using specification for function __gmpz_init_set_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function __gmpz_get_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid. tests/bts/bts1390.c:15:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_k_2); [value] using specification for function __gmpz_add -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid. tests/bts/bts1390.c:11:[value] entering loop for the first time tests/bts/bts1390.c:11:[kernel] warning: out of bounds read. assert \valid_read((char *)buf+__e_acsl_i_2); tests/bts/bts1390.c:20:[value] entering loop for the first time [value] using specification for function __delete_block -tests/bts/bts1390.c:13:[value] Function memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) -tests/bts/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +tests/bts/bts1390.c:16:[value] warning: function memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) tests/bts/bts1390.c:13:[value] entering loop for the first time [value] using specification for function __offset tests/bts/bts1390.c:13:[kernel] warning: out of bounds read. assert \valid_read((char *)__e_acsl_at_2+__e_acsl_j_2); [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/bts/bts1390.c:13:[value] Function __e_acsl_memchr, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) -tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. +tests/bts/bts1390.c:16:[value] warning: function __e_acsl_memchr, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) tests/bts/bts1390.c:21:[kernel] warning: out of bounds read. assert \valid_read(s); -tests/bts/bts1390.c:16:[value] Function memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/bts/bts1390.c:16:[value] Function __e_acsl_memchr, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle index 4773e0b0310047318f83d07d7bdfeb0b2539356c..815257536b6869d15a0cc23c434ff298b61f6333 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.0.res.oracle @@ -35,22 +35,20 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is [value] using specification for function __full_init FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156 [value] using specification for function __delete_block -FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) [value] using specification for function __initialize -tests/bts/bts1399.c:24:[value] Assertion got status valid. [value] using specification for function __valid_read [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __initialized -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. +FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. [value] using specification for function __freeable :0:[value] Assigning imprecise value to __e_acsl_implies. The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178} FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies. It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}. -FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown. +FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle index ff529ac753db6af667533dbc84bc336486e806ee..0e90a522d2cdd7d222c3cbc010fa94ba0406f388 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1399.1.res.oracle @@ -27,38 +27,26 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is [value] using specification for function __full_init FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156 [value] using specification for function __delete_block -FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) [value] using specification for function __initialize -tests/bts/bts1399.c:24:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. -tests/bts/bts1399.c:24:[value] Assertion 'E_ACSL' got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_tdiv_q -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:164:[value] Function __gmpz_tdiv_q: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:166:[value] Function __gmpz_tdiv_q: precondition got status valid. [value] using specification for function __gmpz_get_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid. [value] using specification for function __initialized [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. +FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. [value] using specification for function __freeable :0:[value] Assigning imprecise value to __e_acsl_implies. The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178} FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies. It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}. -FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown. +FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle index 615a1182b1808b5ab22594d8869d317a555ec50c..45f26ef331a318f4a22e30b839db366f298becf4 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.0.res.oracle @@ -14,16 +14,9 @@ global_i_ptr ∈ {{ &global_i }} [value] using specification for function __store_block [value] using specification for function __full_init -tests/bts/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid. -tests/bts/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid. -tests/bts/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] using specification for function __valid -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/bts/bts1478.c:11:[value] Function loop: precondition got status valid. -tests/bts/bts1478.c:12:[value] Function loop: precondition got status valid. -tests/bts/bts1478.c:13:[value] Function loop: precondition got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle index ca69d07a0e98b05b362eda09c8298067a242d337..3be1a2aeb0d5f81cf38e0978f683f15f28c3b0eb 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1478.1.res.oracle @@ -14,23 +14,12 @@ global_i_ptr ∈ {{ &global_i }} [value] using specification for function __store_block [value] using specification for function __full_init -tests/bts/bts1478.c:11:[value] Function __e_acsl_loop: precondition got status valid. -tests/bts/bts1478.c:12:[value] Function __e_acsl_loop: precondition got status valid. -tests/bts/bts1478.c:13:[value] Function __e_acsl_loop: precondition got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __valid -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/bts/bts1478.c:11:[value] Function loop: precondition got status valid. -tests/bts/bts1478.c:12:[value] Function loop: precondition got status valid. -tests/bts/bts1478.c:13:[value] Function loop: precondition got status valid. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle index 983b2ddb8e8ff5693361e16e4c59b8684deaabb5..b323b8576182f6f3b8d636b5e8dcf035d262943d 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.0.res.oracle @@ -11,12 +11,10 @@ __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] [value] using specification for function __store_block -tests/bts/bts1700.i:10:[value] Assertion got status valid. [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __full_init -tests/bts/bts1700.i:13:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle index 983b2ddb8e8ff5693361e16e4c59b8684deaabb5..b323b8576182f6f3b8d636b5e8dcf035d262943d 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1700.1.res.oracle @@ -11,12 +11,10 @@ __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] [value] using specification for function __store_block -tests/bts/bts1700.i:10:[value] Assertion got status valid. [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __full_init -tests/bts/bts1700.i:13:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle index eb2f883c0869d46c4a4b83af223996c299bf1249..2c04f4eb44ed2c35b7ae1ae22a95ca2ee8fc2e9b 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.0.res.oracle @@ -12,11 +12,10 @@ __memory_size ∈ [--..--] [value] using specification for function __store_block [value] using specification for function __full_init -tests/bts/bts1717.i:13:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle index eb2f883c0869d46c4a4b83af223996c299bf1249..2c04f4eb44ed2c35b7ae1ae22a95ca2ee8fc2e9b 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1717.1.res.oracle @@ -12,11 +12,10 @@ __memory_size ∈ [--..--] [value] using specification for function __store_block [value] using specification for function __full_init -tests/bts/bts1717.i:13:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle index a4617af6a665293e6d96627c8dac6997f06fa11a..2c04f4eb44ed2c35b7ae1ae22a95ca2ee8fc2e9b 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1718.0.res.oracle @@ -12,11 +12,10 @@ __memory_size ∈ [--..--] [value] using specification for function __store_block [value] using specification for function __full_init -tests/bts/bts1718.i:13:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle index a4617af6a665293e6d96627c8dac6997f06fa11a..2c04f4eb44ed2c35b7ae1ae22a95ca2ee8fc2e9b 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1718.1.res.oracle @@ -12,11 +12,10 @@ __memory_size ∈ [--..--] [value] using specification for function __store_block [value] using specification for function __full_init -tests/bts/bts1718.i:13:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle index cefeb276e61b9907bda3ef2e074dc0f0f3f7085d..82924e5df2db14afa891c2a10fecf511d9a179c1 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.0.res.oracle @@ -18,17 +18,12 @@ [value] using specification for function __full_init [value] using specification for function __literal_string tests/bts/bts1837.i:19:[value] entering loop for the first time -tests/bts/bts1837.i:21:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function __valid_read [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/bts/bts1837.i:22:[value] Assertion got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __valid [value] using specification for function __delete_block tests/bts/bts1837.i:19:[kernel] warning: signed overflow. assert -2147483648 ≤ i-1; -tests/bts/bts1837.i:11:[value] Assertion got status valid. -tests/bts/bts1837.i:12:[value] Assertion got status valid. -tests/bts/bts1837.i:13:[value] Assertion got status valid. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle b/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle index cefeb276e61b9907bda3ef2e074dc0f0f3f7085d..82924e5df2db14afa891c2a10fecf511d9a179c1 100644 --- a/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle +++ b/src/plugins/e-acsl/tests/bts/oracle/bts1837.1.res.oracle @@ -18,17 +18,12 @@ [value] using specification for function __full_init [value] using specification for function __literal_string tests/bts/bts1837.i:19:[value] entering loop for the first time -tests/bts/bts1837.i:21:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function __valid_read [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/bts/bts1837.i:22:[value] Assertion got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __valid [value] using specification for function __delete_block tests/bts/bts1837.i:19:[kernel] warning: signed overflow. assert -2147483648 ≤ i-1; -tests/bts/bts1837.i:11:[value] Assertion got status valid. -tests/bts/bts1837.i:12:[value] Assertion got status valid. -tests/bts/bts1837.i:13:[value] Assertion got status valid. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.0.res.oracle index 4bcd25d2c380870a245aad302ba475907b30314c..49684ab11266e7ec9733e2a32224b9e87322254a 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.0.res.oracle @@ -12,12 +12,9 @@ __memory_size ∈ [--..--] [value] using specification for function __store_block [value] using specification for function __full_init -tests/e-acsl-runtime/addrOf.i:12:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __delete_block -tests/e-acsl-runtime/addrOf.i:18:[value] Assertion got status valid. -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle index 4bcd25d2c380870a245aad302ba475907b30314c..49684ab11266e7ec9733e2a32224b9e87322254a 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle @@ -12,12 +12,9 @@ __memory_size ∈ [--..--] [value] using specification for function __store_block [value] using specification for function __full_init -tests/e-acsl-runtime/addrOf.i:12:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __delete_block -tests/e-acsl-runtime/addrOf.i:18:[value] Assertion got status valid. -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.0.res.oracle index e16771bba8f47172248978e9528949591c473921..0c77241ff78f009ed001537fff98034ca770b4ce 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.0.res.oracle @@ -14,9 +14,8 @@ [value] using specification for function __full_init [value] using specification for function __initialize [value] using specification for function __delete_block -tests/e-acsl-runtime/alias.i:16:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.1.res.oracle index e16771bba8f47172248978e9528949591c473921..0c77241ff78f009ed001537fff98034ca770b4ce 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/alias.1.res.oracle @@ -14,9 +14,8 @@ [value] using specification for function __full_init [value] using specification for function __initialize [value] using specification for function __delete_block -tests/e-acsl-runtime/alias.i:16:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.0.res.oracle index 9e13e05e51dd2fa26998055d289d6af06e884bdf..f0d9dbf6c715c6fb6e5314a8a737295cb93f35a9 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.0.res.oracle @@ -10,24 +10,5 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/arith.i:12:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/arith.i:13:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:14:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:16:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:17:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:18:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:19:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:20:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:21:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:22:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:23:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:25:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:27:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:28:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:29:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:30:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:32:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:33:[value] Assertion got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle index 1f09cb63b6eb0eb44fdf71cc73742301516be8ed..ffd0bd8013cddf9bfbfe2a18c373720bf1089834 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle @@ -10,67 +10,18 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/arith.i:12:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. [value] using specification for function __gmpz_neg -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:137:[value] Function __gmpz_neg: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:138:[value] Function __gmpz_neg: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/e-acsl-runtime/arith.i:13:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:14:[value] Assertion got status valid. [value] using specification for function __gmpz_com -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:182:[value] Function __gmpz_com: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:183:[value] Function __gmpz_com: precondition got status valid. -tests/e-acsl-runtime/arith.i:16:[value] Assertion got status valid. [value] using specification for function __gmpz_add -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid. -tests/e-acsl-runtime/arith.i:17:[value] Assertion got status valid. [value] using specification for function __gmpz_sub -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:150:[value] Function __gmpz_sub: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:151:[value] Function __gmpz_sub: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:152:[value] Function __gmpz_sub: precondition got status valid. -tests/e-acsl-runtime/arith.i:18:[value] Assertion got status valid. [value] using specification for function __gmpz_mul -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:157:[value] Function __gmpz_mul: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid. -tests/e-acsl-runtime/arith.i:19:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:19:[value] Assertion 'E_ACSL' got status valid. [value] using specification for function __gmpz_tdiv_q -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:164:[value] Function __gmpz_tdiv_q: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:166:[value] Function __gmpz_tdiv_q: precondition got status valid. -tests/e-acsl-runtime/arith.i:20:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_str -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:73:[value] Function __gmpz_init_set_str: precondition got status valid. -tests/e-acsl-runtime/arith.i:20:[value] Assertion 'E_ACSL' got status valid. -tests/e-acsl-runtime/arith.i:21:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:21:[value] Assertion 'E_ACSL' got status valid. [value] using specification for function __gmpz_tdiv_r -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:171:[value] Function __gmpz_tdiv_r: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:172:[value] Function __gmpz_tdiv_r: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:173:[value] Function __gmpz_tdiv_r: precondition got status valid. -tests/e-acsl-runtime/arith.i:22:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:22:[value] Assertion 'E_ACSL' got status valid. -tests/e-acsl-runtime/arith.i:23:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:23:[value] Assertion 'E_ACSL' got status valid. -tests/e-acsl-runtime/arith.i:25:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:27:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:28:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:29:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:30:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:32:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:33:[value] Assertion got status valid. -tests/e-acsl-runtime/arith.i:33:[value] Assertion 'E_ACSL' got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.0.res.oracle index ee1253b86e554319d71a05658c1c4858f926e07c..8f4a3d3b726e4de70a64a83ff6d2a86ac9758b36 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.0.res.oracle @@ -14,8 +14,8 @@ T2[0..3] ∈ {0} tests/e-acsl-runtime/array.i:12:[value] entering loop for the first time tests/e-acsl-runtime/array.i:13:[value] entering loop for the first time -tests/e-acsl-runtime/array.i:15:[value] Assertion got status unknown. +tests/e-acsl-runtime/array.i:15:[value] warning: assertion got status unknown. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/array.i:16:[value] Assertion got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. +tests/e-acsl-runtime/array.i:16:[value] warning: assertion got status unknown. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle index f776ff5e9498ffaaf3c60e9a53355c6f61bea139..eb2477f723cb8c2dc008e03316844225964c80e3 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle @@ -14,15 +14,11 @@ T2[0..3] ∈ {0} tests/e-acsl-runtime/array.i:12:[value] entering loop for the first time tests/e-acsl-runtime/array.i:13:[value] entering loop for the first time -tests/e-acsl-runtime/array.i:15:[value] Assertion got status unknown. +tests/e-acsl-runtime/array.i:15:[value] warning: assertion got status unknown. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/e-acsl-runtime/array.i:16:[value] Assertion got status unknown. +tests/e-acsl-runtime/array.i:16:[value] warning: assertion got status unknown. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.0.res.oracle index 96720f05fdbbdbb8623457e4ca5767f54f99ab5f..2f339588463bc8f05aa1bf2ebac8874f03c071ed 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.0.res.oracle @@ -14,30 +14,21 @@ [value] using specification for function __store_block [value] using specification for function __full_init [value] using specification for function __delete_block -tests/e-acsl-runtime/at.i:40:[value] Function h: postcondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/at.i:40:[value] Function __e_acsl_h: postcondition got status valid. -tests/e-acsl-runtime/at.i:48:[value] Assertion got status valid. -tests/e-acsl-runtime/at.i:13:[value] Assertion got status valid. tests/e-acsl-runtime/at.i:14:[value] cannot evaluate ACSL term, \at() on a C label is unsupported -tests/e-acsl-runtime/at.i:14:[value] Assertion got status unknown. -tests/e-acsl-runtime/at.i:15:[value] Assertion got status valid. -tests/e-acsl-runtime/at.i:16:[value] Assertion got status valid. -tests/e-acsl-runtime/at.i:9:[value] Function f: postcondition got status valid. -tests/e-acsl-runtime/at.i:9:[value] Function __e_acsl_f: postcondition got status valid. +tests/e-acsl-runtime/at.i:14:[value] warning: assertion got status unknown. tests/e-acsl-runtime/at.i:53:[value] cannot evaluate ACSL term, \at() on a C label is unsupported -tests/e-acsl-runtime/at.i:53:[value] Assertion got status unknown. +tests/e-acsl-runtime/at.i:53:[value] warning: assertion got status unknown. tests/e-acsl-runtime/at.i:54:[value] cannot evaluate ACSL term, \at() on a C label is unsupported -tests/e-acsl-runtime/at.i:54:[value] Assertion got status unknown. +tests/e-acsl-runtime/at.i:54:[value] warning: assertion got status unknown. tests/e-acsl-runtime/at.i:55:[value] cannot evaluate ACSL term, \at() on a C label is unsupported -tests/e-acsl-runtime/at.i:55:[value] Assertion got status unknown. +tests/e-acsl-runtime/at.i:55:[value] warning: assertion got status unknown. [value] using specification for function __initialize [value] using specification for function __valid_read -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. tests/e-acsl-runtime/at.i:32:[value] cannot evaluate ACSL term, \at() on a C label is unsupported -tests/e-acsl-runtime/at.i:32:[value] Assertion got status unknown. +tests/e-acsl-runtime/at.i:32:[value] warning: assertion got status unknown. tests/e-acsl-runtime/at.i:34:[value] cannot evaluate ACSL term, \at() on a C label is unsupported -tests/e-acsl-runtime/at.i:34:[value] Assertion got status unknown. +tests/e-acsl-runtime/at.i:34:[value] warning: assertion got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle index 6ba9bf6d9e72bc6e64cd61688f8cdcc5fdf226c7..05a4c55b977b967768e46c015e0e4a04b15a8fcd 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle @@ -14,45 +14,27 @@ [value] using specification for function __store_block [value] using specification for function __full_init [value] using specification for function __delete_block -tests/e-acsl-runtime/at.i:40:[value] Function h: postcondition got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/e-acsl-runtime/at.i:40:[value] Function __e_acsl_h: postcondition got status valid. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. [value] using specification for function __gmpz_add -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid. [value] using specification for function __gmpz_init_set -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:46:[value] Function __gmpz_init_set: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:47:[value] Function __gmpz_init_set: precondition got status valid. -tests/e-acsl-runtime/at.i:48:[value] Assertion got status valid. -tests/e-acsl-runtime/at.i:13:[value] Assertion got status valid. tests/e-acsl-runtime/at.i:14:[value] cannot evaluate ACSL term, \at() on a C label is unsupported -tests/e-acsl-runtime/at.i:14:[value] Assertion got status unknown. -tests/e-acsl-runtime/at.i:15:[value] Assertion got status valid. -tests/e-acsl-runtime/at.i:16:[value] Assertion got status valid. -tests/e-acsl-runtime/at.i:9:[value] Function f: postcondition got status valid. -tests/e-acsl-runtime/at.i:9:[value] Function __e_acsl_f: postcondition got status valid. +tests/e-acsl-runtime/at.i:14:[value] warning: assertion got status unknown. tests/e-acsl-runtime/at.i:53:[value] cannot evaluate ACSL term, \at() on a C label is unsupported -tests/e-acsl-runtime/at.i:53:[value] Assertion got status unknown. +tests/e-acsl-runtime/at.i:53:[value] warning: assertion got status unknown. tests/e-acsl-runtime/at.i:54:[value] cannot evaluate ACSL term, \at() on a C label is unsupported -tests/e-acsl-runtime/at.i:54:[value] Assertion got status unknown. +tests/e-acsl-runtime/at.i:54:[value] warning: assertion got status unknown. tests/e-acsl-runtime/at.i:55:[value] cannot evaluate ACSL term, \at() on a C label is unsupported -tests/e-acsl-runtime/at.i:55:[value] Assertion got status unknown. +tests/e-acsl-runtime/at.i:55:[value] warning: assertion got status unknown. [value] using specification for function __initialize [value] using specification for function __valid_read tests/e-acsl-runtime/at.i:32:[value] cannot evaluate ACSL term, \at() on a C label is unsupported -tests/e-acsl-runtime/at.i:32:[value] Assertion got status unknown. +tests/e-acsl-runtime/at.i:32:[value] warning: assertion got status unknown. tests/e-acsl-runtime/at.i:34:[value] cannot evaluate ACSL term, \at() on a C label is unsupported -tests/e-acsl-runtime/at.i:34:[value] Assertion got status unknown. +tests/e-acsl-runtime/at.i:34:[value] warning: assertion got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.0.res.oracle index 5b143f91676c7f263265557b474ff4dcf2d3cbcb..faed34d88a8025557e34b38394dfc056d5839c3f 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.0.res.oracle @@ -27,14 +27,12 @@ FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic functio [value] using specification for function __full_init FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156 [value] using specification for function __delete_block -FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156_0 [value] using specification for function __initialize -tests/e-acsl-runtime/call.c:12:[value] Function f: postcondition got status valid. [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/call.c:12:[value] Function __e_acsl_f: postcondition got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle index 16b7e91901b0fd39c87ee5d7c745e1bedbfe6768..67d328ebf2ebf9badfbda61edc5ba8c7ded90b39 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/call.1.res.oracle @@ -23,14 +23,12 @@ tests/e-acsl-runtime/call.c:18:[e-acsl] warning: E-ACSL construct `logic functio [value] using specification for function __full_init FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156 [value] using specification for function __delete_block -FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156_0 [value] using specification for function __initialize -tests/e-acsl-runtime/call.c:12:[value] Function f: postcondition got status valid. [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/call.c:12:[value] Function __e_acsl_f: postcondition got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.0.res.oracle index 61fa2dd0ad737859c8c17bf3114aa8a6233b21c0..f0d9dbf6c715c6fb6e5314a8a737295cb93f35a9 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.0.res.oracle @@ -10,12 +10,5 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/cast.i:12:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/cast.i:13:[value] Assertion got status valid. -tests/e-acsl-runtime/cast.i:15:[value] Assertion got status valid. -tests/e-acsl-runtime/cast.i:16:[value] Assertion got status valid. -tests/e-acsl-runtime/cast.i:19:[value] Assertion got status valid. -tests/e-acsl-runtime/cast.i:20:[value] Assertion got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle index ec9a37710689a807271a4b7d015cf756100ae640..1b00f8980afcfa2cb328cdcdaf438d9f2fe503b3 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle @@ -10,25 +10,12 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/cast.i:12:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/e-acsl-runtime/cast.i:13:[value] Assertion got status valid. -tests/e-acsl-runtime/cast.i:15:[value] Assertion got status valid. -tests/e-acsl-runtime/cast.i:16:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid. -tests/e-acsl-runtime/cast.i:19:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_str -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:73:[value] Function __gmpz_init_set_str: precondition got status valid. [value] using specification for function __gmpz_get_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid. -tests/e-acsl-runtime/cast.i:20:[value] Assertion got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.0.res.oracle index f25ea08678e5dca1acc1c4fda798f23547278742..f0d9dbf6c715c6fb6e5314a8a737295cb93f35a9 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.0.res.oracle @@ -10,23 +10,5 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/comparison.i:9:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/comparison.i:10:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:11:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:12:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:14:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:17:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:18:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:19:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:20:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:21:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:22:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:24:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:25:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:26:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:27:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:28:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:29:[value] Assertion got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle index 738cbde7a5c418b012ff4946a583db61460c8d3a..7f46b34e22aa5e7107856ec9c3db59f822de65c3 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle @@ -10,36 +10,11 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/comparison.i:9:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/e-acsl-runtime/comparison.i:10:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:11:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:12:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:14:[value] Assertion got status valid. -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/comparison.i:17:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:18:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:19:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:20:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:21:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:22:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:24:[value] Assertion got status valid. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. [value] using specification for function __gmpz_neg -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:137:[value] Function __gmpz_neg: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:138:[value] Function __gmpz_neg: precondition got status valid. -tests/e-acsl-runtime/comparison.i:25:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:26:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:27:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:28:[value] Assertion got status valid. -tests/e-acsl-runtime/comparison.i:29:[value] Assertion got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle index f8184dd9d7f961f26e8c6a45a6b414e94727def2..22916af593bc51d099f1c9fbd3f61d3bc28369bf 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.0.res.oracle @@ -30,23 +30,11 @@ [value] using specification for function __store_block [value] using specification for function __full_init [value] using specification for function __literal_string -tests/e-acsl-runtime/compound_initializers.c:35:[value] Assertion got status valid. [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/compound_initializers.c:36:[value] Assertion got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __initialized [value] using specification for function __valid_read -tests/e-acsl-runtime/compound_initializers.c:37:[value] Assertion got status valid. -tests/e-acsl-runtime/compound_initializers.c:38:[value] Assertion got status valid. -tests/e-acsl-runtime/compound_initializers.c:39:[value] Assertion got status valid. -tests/e-acsl-runtime/compound_initializers.c:40:[value] Assertion got status valid. -tests/e-acsl-runtime/compound_initializers.c:41:[value] Assertion got status valid. -tests/e-acsl-runtime/compound_initializers.c:42:[value] Assertion got status valid. -tests/e-acsl-runtime/compound_initializers.c:43:[value] Assertion got status valid. -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/compound_initializers.c:44:[value] Assertion got status valid. -tests/e-acsl-runtime/compound_initializers.c:45:[value] Assertion got status valid. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.1.res.oracle index f170948d04d2eeaab43e6d9d08fe2e928d3a2abe..033d0a1dab083b7871c7c9c419b1e24d76c8ed3a 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/compound_initializers.1.res.oracle @@ -30,29 +30,14 @@ [value] using specification for function __store_block [value] using specification for function __full_init [value] using specification for function __literal_string -tests/e-acsl-runtime/compound_initializers.c:35:[value] Assertion got status valid. [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/compound_initializers.c:36:[value] Assertion got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __initialized [value] using specification for function __valid_read -tests/e-acsl-runtime/compound_initializers.c:37:[value] Assertion got status valid. -tests/e-acsl-runtime/compound_initializers.c:38:[value] Assertion got status valid. -tests/e-acsl-runtime/compound_initializers.c:39:[value] Assertion got status valid. -tests/e-acsl-runtime/compound_initializers.c:40:[value] Assertion got status valid. -tests/e-acsl-runtime/compound_initializers.c:41:[value] Assertion got status valid. -tests/e-acsl-runtime/compound_initializers.c:42:[value] Assertion got status valid. -tests/e-acsl-runtime/compound_initializers.c:43:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/e-acsl-runtime/compound_initializers.c:44:[value] Assertion got status valid. -tests/e-acsl-runtime/compound_initializers.c:45:[value] Assertion got status valid. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle index 690693003a4cb5e6428789685ebfa94282e7f540..dfd6c7dcbab95dc74e4309982d4234ee5a5d2772 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.0.res.oracle @@ -32,7 +32,7 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] [value] using specification for function __store_block -tests/e-acsl-runtime/freeable.c:15:[value] Assertion got status unknown. +tests/e-acsl-runtime/freeable.c:15:[value] warning: assertion got status unknown. tests/e-acsl-runtime/freeable.c:15:[value] completely invalid value in evaluation of argument (void *)p tests/e-acsl-runtime/freeable.c:15:[kernel] warning: accessing uninitialized left-value. assert \initialized(&p); diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle index 2f31a65647b8efb236c41fe7b016b2051288870b..48a19d4a6d12defc4ec3a28f2ddcf5e33f07e8c1 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/freeable.1.res.oracle @@ -24,7 +24,7 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] [value] using specification for function __store_block -tests/e-acsl-runtime/freeable.c:15:[value] Assertion got status unknown. +tests/e-acsl-runtime/freeable.c:15:[value] warning: assertion got status unknown. tests/e-acsl-runtime/freeable.c:15:[value] completely invalid value in evaluation of argument (void *)p tests/e-acsl-runtime/freeable.c:15:[kernel] warning: accessing uninitialized left-value. assert \initialized(&p); diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.0.res.oracle index 1bbc0c9654d741b860380ee0c7d2bb622777b7fb..1e2b88ff34e699465b85de3400d61a0e30a1420f 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.0.res.oracle @@ -12,51 +12,5 @@ __memory_size ∈ [--..--] X ∈ {0} Y ∈ {2} -tests/e-acsl-runtime/function_contract.i:10:[value] Function f: postcondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:10:[value] Function __e_acsl_f: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:14:[value] Function g: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:15:[value] Function g: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:14:[value] Function __e_acsl_g: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:15:[value] Function __e_acsl_g: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:19:[value] Function __e_acsl_h: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:19:[value] Function h: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:23:[value] Function __e_acsl_i: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:24:[value] Function __e_acsl_i: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:23:[value] Function i: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:24:[value] Function i: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:29:[value] Function __e_acsl_j, behavior b1: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:32:[value] Function __e_acsl_j, behavior b2: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:33:[value] Function __e_acsl_j, behavior b2: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:29:[value] Function j, behavior b1: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:32:[value] Function j, behavior b2: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:33:[value] Function j, behavior b2: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:30:[value] Function j, behavior b1: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:34:[value] Function j, behavior b2: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:30:[value] Function __e_acsl_j, behavior b1: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:34:[value] Function __e_acsl_j, behavior b2: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:40:[value] Function __e_acsl_k, behavior b1: assumes got status invalid; precondition not evaluated. -tests/e-acsl-runtime/function_contract.i:44:[value] Function __e_acsl_k, behavior b2: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:45:[value] Function __e_acsl_k, behavior b2: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:40:[value] Function k, behavior b1: assumes got status invalid; precondition not evaluated. -tests/e-acsl-runtime/function_contract.i:44:[value] Function k, behavior b2: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:45:[value] Function k, behavior b2: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:51:[value] Assertion got status valid. -tests/e-acsl-runtime/function_contract.i:49:[value] Function l: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:49:[value] Function __e_acsl_l: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:58:[value] Function m, behavior b1: assumes got status invalid; postcondition not evaluated. -tests/e-acsl-runtime/function_contract.i:62:[value] Function m, behavior b2: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:63:[value] Function m, behavior b2: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:58:[value] Function __e_acsl_m, behavior b1: assumes got status invalid; postcondition not evaluated. -tests/e-acsl-runtime/function_contract.i:62:[value] Function __e_acsl_m, behavior b2: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:63:[value] Function __e_acsl_m, behavior b2: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:67:[value] Function __e_acsl_n: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:68:[value] Function __e_acsl_n: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:67:[value] Function n: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:68:[value] Function n: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:71:[value] Function n, behavior b1: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:74:[value] Function n, behavior b2: assumes got status invalid; postcondition not evaluated. -tests/e-acsl-runtime/function_contract.i:71:[value] Function __e_acsl_n, behavior b1: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:74:[value] Function __e_acsl_n, behavior b2: assumes got status invalid; postcondition not evaluated. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle index 2cc6f18177e38838932c94c70ad4d9f6ec49da31..a5904b43663292ab0de1360a9433bd24c9feaecf 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle @@ -12,64 +12,11 @@ __memory_size ∈ [--..--] X ∈ {0} Y ∈ {2} -tests/e-acsl-runtime/function_contract.i:10:[value] Function f: postcondition got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:10:[value] Function __e_acsl_f: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:14:[value] Function g: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:15:[value] Function g: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:14:[value] Function __e_acsl_g: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:15:[value] Function __e_acsl_g: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:19:[value] Function __e_acsl_h: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:19:[value] Function h: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:23:[value] Function __e_acsl_i: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:24:[value] Function __e_acsl_i: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:23:[value] Function i: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:24:[value] Function i: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:29:[value] Function __e_acsl_j, behavior b1: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:32:[value] Function __e_acsl_j, behavior b2: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:33:[value] Function __e_acsl_j, behavior b2: precondition got status valid. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. [value] using specification for function __gmpz_add -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:29:[value] Function j, behavior b1: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:32:[value] Function j, behavior b2: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:33:[value] Function j, behavior b2: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:30:[value] Function j, behavior b1: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:34:[value] Function j, behavior b2: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:30:[value] Function __e_acsl_j, behavior b1: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:34:[value] Function __e_acsl_j, behavior b2: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:40:[value] Function __e_acsl_k, behavior b1: assumes got status invalid; precondition not evaluated. -tests/e-acsl-runtime/function_contract.i:44:[value] Function __e_acsl_k, behavior b2: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:45:[value] Function __e_acsl_k, behavior b2: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:40:[value] Function k, behavior b1: assumes got status invalid; precondition not evaluated. -tests/e-acsl-runtime/function_contract.i:44:[value] Function k, behavior b2: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:45:[value] Function k, behavior b2: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:51:[value] Assertion got status valid. -tests/e-acsl-runtime/function_contract.i:49:[value] Function l: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:49:[value] Function __e_acsl_l: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:58:[value] Function m, behavior b1: assumes got status invalid; postcondition not evaluated. -tests/e-acsl-runtime/function_contract.i:62:[value] Function m, behavior b2: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:63:[value] Function m, behavior b2: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:58:[value] Function __e_acsl_m, behavior b1: assumes got status invalid; postcondition not evaluated. -tests/e-acsl-runtime/function_contract.i:62:[value] Function __e_acsl_m, behavior b2: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:63:[value] Function __e_acsl_m, behavior b2: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:67:[value] Function __e_acsl_n: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:68:[value] Function __e_acsl_n: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:67:[value] Function n: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:68:[value] Function n: precondition got status valid. -tests/e-acsl-runtime/function_contract.i:71:[value] Function n, behavior b1: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:74:[value] Function n, behavior b2: assumes got status invalid; postcondition not evaluated. -tests/e-acsl-runtime/function_contract.i:71:[value] Function __e_acsl_n, behavior b1: postcondition got status valid. -tests/e-acsl-runtime/function_contract.i:74:[value] Function __e_acsl_n, behavior b2: assumes got status invalid; postcondition not evaluated. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.0.res.oracle index 97bb0712a0349c42d8143936a53e0225a1de5860..7cff290b275d8f4e24d70c347dd3f46a64df9c2b 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.0.res.oracle @@ -17,11 +17,9 @@ [value] using specification for function __initialize [value] using specification for function __valid_read [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __valid -tests/e-acsl-runtime/ghost.i:17:[value] Assertion got status valid. [value] using specification for function __initialized -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle index 2cee1d69b38777ad323fcae841388704d3f43b10..91c132e3a5a8f7b1d88dfed2352302cc7c2f0048 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ghost.1.res.oracle @@ -17,16 +17,11 @@ [value] using specification for function __initialize [value] using specification for function __valid_read [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __valid -tests/e-acsl-runtime/ghost.i:17:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.0.res.oracle index d0c22cc84bc5858e31c82c35029cd68e9bb80876..d19125c9928b692c449c286979527491007caaef 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.0.res.oracle @@ -14,13 +14,9 @@ b ∈ {0} [value] using specification for function __store_block [value] using specification for function __full_init -tests/e-acsl-runtime/init.c:11:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/init.c:12:[value] Assertion got status valid. [value] using specification for function __initialized -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/init.c:13:[value] Assertion got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle index d0c22cc84bc5858e31c82c35029cd68e9bb80876..d19125c9928b692c449c286979527491007caaef 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/init.1.res.oracle @@ -14,13 +14,9 @@ b ∈ {0} [value] using specification for function __store_block [value] using specification for function __full_init -tests/e-acsl-runtime/init.c:11:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/init.c:12:[value] Assertion got status valid. [value] using specification for function __initialized -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/init.c:13:[value] Assertion got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.0.res.oracle index f7340321cd0498bee0597b1d17fac485ffeb73f1..294e77a267cfd533f8e1b334baa024b8b3bff780 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.0.res.oracle @@ -10,18 +10,9 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/integer_constant.i:8:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/integer_constant.i:10:[value] Assertion got status valid. -tests/e-acsl-runtime/integer_constant.i:11:[value] Assertion got status valid. -tests/e-acsl-runtime/integer_constant.i:13:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_str -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:73:[value] Function __gmpz_init_set_str: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle index db4cb25cd186a33fd8b4a9edb4f398e8ab9929fa..dd977035dae231f610550b119b68930e04bdab24 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle @@ -10,19 +10,10 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/integer_constant.i:8:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/e-acsl-runtime/integer_constant.i:10:[value] Assertion got status valid. -tests/e-acsl-runtime/integer_constant.i:11:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_str -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:73:[value] Function __gmpz_init_set_str: precondition got status valid. -tests/e-acsl-runtime/integer_constant.i:13:[value] Assertion got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.0.res.oracle index ada600909030a9236134c45221480e4010d7d1a9..c23dbf0116b90a43d690e5ac4edad3a1d95dc58f 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.0.res.oracle @@ -12,7 +12,6 @@ __memory_size ∈ [--..--] tests/e-acsl-runtime/invariant.i:8:[value] entering loop for the first time [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. tests/e-acsl-runtime/invariant.i:10:[kernel] warning: signed overflow. assert x+i ≤ 2147483647; [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle index adb93500ead6803a182070f51da5d55da0c60890..097c17aa47de4a463334f05f7d6bc509f5867f7d 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle @@ -12,13 +12,9 @@ __memory_size ∈ [--..--] tests/e-acsl-runtime/invariant.i:8:[value] entering loop for the first time [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. tests/e-acsl-runtime/invariant.i:10:[kernel] warning: signed overflow. assert x+i ≤ 2147483647; [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.0.res.oracle index ea82cb27ffb5ea7f7466582b93de03784f651004..6dce2057d115e695e8f1317f9befcc3796e6b93f 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.0.res.oracle @@ -11,9 +11,5 @@ __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] X ∈ {0} -tests/e-acsl-runtime/labeled_stmt.i:12:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function __e_acsl_main: postcondition got status valid. -tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function main: postcondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle index 34d08a38a829e7832700cdf01e9aa249e21bbbfa..1e90496d9c4ef17f4d8bafec3db447d73b400b88 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle @@ -11,16 +11,9 @@ __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] X ∈ {0} -tests/e-acsl-runtime/labeled_stmt.i:12:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function __e_acsl_main: postcondition got status valid. -tests/e-acsl-runtime/labeled_stmt.i:9:[value] Function main: postcondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.0.res.oracle index 67f5d8e043597363555e7e3747373d0a3a79bf18..044d08c5d631bfcc524a1c04f938d880702f1141 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.0.res.oracle @@ -10,22 +10,8 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/lazy.i:11:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/lazy.i:12:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:13:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:14:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:15:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:16:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:17:[value] Assertion got status unknown. -tests/e-acsl-runtime/lazy.i:18:[value] Assertion got status unknown. -tests/e-acsl-runtime/lazy.i:19:[value] Assertion got status unknown. -tests/e-acsl-runtime/lazy.i:22:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:23:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:26:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:27:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:28:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:29:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:30:[value] Assertion got status valid. +tests/e-acsl-runtime/lazy.i:17:[value] warning: assertion got status unknown. +tests/e-acsl-runtime/lazy.i:18:[value] warning: assertion got status unknown. +tests/e-acsl-runtime/lazy.i:19:[value] warning: assertion got status unknown. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle index 55a6dc8a5ed9f671198fde6e06e7452b308c7d30..9be75f5ecfa652d68514833cbf17f937eafc1fa6 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle @@ -10,38 +10,17 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/lazy.i:11:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/lazy.i:12:[value] Assertion got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. -tests/e-acsl-runtime/lazy.i:12:[value] Assertion 'E_ACSL' got status invalid (stopping propagation). -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/lazy.i:13:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:14:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:14:[value] Assertion 'E_ACSL' got status invalid (stopping propagation). -tests/e-acsl-runtime/lazy.i:15:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:16:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:16:[value] Assertion 'E_ACSL' got status invalid (stopping propagation). -tests/e-acsl-runtime/lazy.i:17:[value] Assertion got status unknown. -tests/e-acsl-runtime/lazy.i:18:[value] Assertion got status unknown. -tests/e-acsl-runtime/lazy.i:19:[value] Assertion got status unknown. -tests/e-acsl-runtime/lazy.i:22:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:23:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:26:[value] Assertion got status valid. +tests/e-acsl-runtime/lazy.i:12:[value] warning: assertion 'E_ACSL' got status invalid (stopping propagation). +tests/e-acsl-runtime/lazy.i:14:[value] warning: assertion 'E_ACSL' got status invalid (stopping propagation). +tests/e-acsl-runtime/lazy.i:16:[value] warning: assertion 'E_ACSL' got status invalid (stopping propagation). +tests/e-acsl-runtime/lazy.i:17:[value] warning: assertion got status unknown. +tests/e-acsl-runtime/lazy.i:18:[value] warning: assertion got status unknown. +tests/e-acsl-runtime/lazy.i:19:[value] warning: assertion got status unknown. [value] using specification for function __gmpz_init_set -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:46:[value] Function __gmpz_init_set: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:47:[value] Function __gmpz_init_set: precondition got status valid. -tests/e-acsl-runtime/lazy.i:27:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:28:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:29:[value] Assertion got status valid. -tests/e-acsl-runtime/lazy.i:30:[value] Assertion got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle index 7b2aac32b7ae44a4c9a77e1b84860e8449e2ad1a..0c2754d6b55e4db46c632db9b7533c36142f9ab6 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.0.res.oracle @@ -12,24 +12,20 @@ __memory_size ∈ [--..--] A[0..9] ∈ {0} tests/e-acsl-runtime/linear_search.i:30:[value] entering loop for the first time -tests/e-acsl-runtime/linear_search.i:9:[value] Function __e_acsl_search: precondition got status unknown. +tests/e-acsl-runtime/linear_search.i:9:[value] warning: function __e_acsl_search: precondition got status unknown. tests/e-acsl-runtime/linear_search.i:9:[value] entering loop for the first time [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. tests/e-acsl-runtime/linear_search.i:14:[value] entering loop for the first time tests/e-acsl-runtime/linear_search.i:11:[value] entering loop for the first time -tests/e-acsl-runtime/linear_search.i:9:[value] Function search: precondition got status unknown. +tests/e-acsl-runtime/linear_search.i:9:[value] warning: function search: precondition got status unknown. tests/e-acsl-runtime/linear_search.i:20:[value] entering loop for the first time -tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid. -tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown. +tests/e-acsl-runtime/linear_search.i:20:[value] warning: loop invariant got status unknown. tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time -tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown. -tests/e-acsl-runtime/linear_search.i:36:[value] Assertion got status unknown. +tests/e-acsl-runtime/linear_search.i:12:[value] warning: function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) +tests/e-acsl-runtime/linear_search.i:15:[value] warning: function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) +tests/e-acsl-runtime/linear_search.i:12:[value] warning: function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +tests/e-acsl-runtime/linear_search.i:15:[value] warning: function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +tests/e-acsl-runtime/linear_search.i:33:[value] warning: assertion got status unknown. +tests/e-acsl-runtime/linear_search.i:36:[value] warning: assertion got status unknown. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle index feccbdb6ddb785f724c6161f27796d73f1476dc5..3fc3a773adc49ec26062657e4ddce027cfa61838 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle @@ -12,47 +12,33 @@ __memory_size ∈ [--..--] A[0..9] ∈ {0} tests/e-acsl-runtime/linear_search.i:30:[value] entering loop for the first time -tests/e-acsl-runtime/linear_search.i:9:[value] Function __e_acsl_search: precondition got status unknown. +tests/e-acsl-runtime/linear_search.i:9:[value] warning: function __e_acsl_search: precondition got status unknown. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_set -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. tests/e-acsl-runtime/linear_search.i:9:[value] entering loop for the first time [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function __gmpz_get_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid. tests/e-acsl-runtime/linear_search.i:9:[kernel] warning: accessing out of bounds index. assert __e_acsl_i_2 < 10; [value] using specification for function __gmpz_add -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid. tests/e-acsl-runtime/linear_search.i:9:[kernel] warning: accessing out of bounds index. assert __e_acsl_3 < 10; [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. tests/e-acsl-runtime/linear_search.i:14:[value] entering loop for the first time tests/e-acsl-runtime/linear_search.i:14:[kernel] warning: accessing out of bounds index. assert __e_acsl_j_4 < 10; tests/e-acsl-runtime/linear_search.i:11:[value] entering loop for the first time tests/e-acsl-runtime/linear_search.i:11:[kernel] warning: accessing out of bounds index. assert __e_acsl_j_2 < 10; -tests/e-acsl-runtime/linear_search.i:9:[value] Function search: precondition got status unknown. +tests/e-acsl-runtime/linear_search.i:9:[value] warning: function search: precondition got status unknown. tests/e-acsl-runtime/linear_search.i:20:[value] entering loop for the first time tests/e-acsl-runtime/linear_search.i:20:[kernel] warning: accessing out of bounds index. assert __e_acsl_i_2 < 10; -tests/e-acsl-runtime/linear_search.i:19:[value] Loop invariant got status valid. -tests/e-acsl-runtime/linear_search.i:20:[value] Loop invariant got status unknown. +tests/e-acsl-runtime/linear_search.i:20:[value] warning: loop invariant got status unknown. tests/e-acsl-runtime/linear_search.i:21:[value] entering loop for the first time tests/e-acsl-runtime/linear_search.i:20:[kernel] warning: accessing out of bounds index. assert __e_acsl_i_4 < 10; -tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/linear_search.i:12:[value] Function search, behavior exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status valid. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/linear_search.i:15:[value] Function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/linear_search.i:12:[value] Function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/linear_search.i:15:[value] Function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown. -tests/e-acsl-runtime/linear_search.i:36:[value] Assertion got status unknown. +tests/e-acsl-runtime/linear_search.i:12:[value] warning: function search, behavior exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) +tests/e-acsl-runtime/linear_search.i:15:[value] warning: function search, behavior not_exists: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) +tests/e-acsl-runtime/linear_search.i:12:[value] warning: function __e_acsl_search, behavior exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +tests/e-acsl-runtime/linear_search.i:15:[value] warning: function __e_acsl_search, behavior not_exists: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +tests/e-acsl-runtime/linear_search.i:33:[value] warning: assertion got status unknown. +tests/e-acsl-runtime/linear_search.i:36:[value] warning: assertion got status unknown. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.0.res.oracle index c04d9a8f696904fa8df6921de8706b24764cdf10..db70db6e090a3ef3ef3ec981520781fa5467e18b 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.0.res.oracle @@ -24,17 +24,11 @@ [value] using specification for function __store_block [value] using specification for function __full_init [value] using specification for function __literal_string -tests/e-acsl-runtime/literal_string.i:24:[value] Assertion got status valid. [value] using specification for function __valid_read [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/literal_string.i:25:[value] Assertion got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __initialized -tests/e-acsl-runtime/literal_string.i:26:[value] Assertion got status valid. -tests/e-acsl-runtime/literal_string.i:27:[value] Assertion got status valid. [value] using specification for function __valid -tests/e-acsl-runtime/literal_string.i:13:[value] Assertion got status valid. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle index dcdcf9a030ef2a43fcafc5365d2b28e72ff0bb33..dcc82287939e3ee20dcfca37f1382d8ed32f34b5 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/literal_string.1.res.oracle @@ -24,23 +24,14 @@ [value] using specification for function __store_block [value] using specification for function __full_init [value] using specification for function __literal_string -tests/e-acsl-runtime/literal_string.i:24:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/e-acsl-runtime/literal_string.i:25:[value] Assertion got status valid. [value] using specification for function __initialized -tests/e-acsl-runtime/literal_string.i:26:[value] Assertion got status valid. [value] using specification for function __valid_read -tests/e-acsl-runtime/literal_string.i:27:[value] Assertion got status valid. [value] using specification for function __valid -tests/e-acsl-runtime/literal_string.i:13:[value] Assertion got status valid. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle index 2e97f3d935b6dde42b7bcb1dd6027f97f9123872..512eccd64dea1799e476e543a7a9838f06477949 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.0.res.oracle @@ -27,13 +27,12 @@ FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic functio [value] using specification for function __full_init FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156 [value] using specification for function __delete_block -FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid. +FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) [value] using specification for function __initialized [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __initialize FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156_0 [value] using specification for function __e_acsl_memory_clean diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle index 7bcb0d299272e897bb857a1ffc73892ee4b0a4b0..954b596c4564fe2101c6113d14e67a2ca20c2aca 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/localvar.1.res.oracle @@ -23,13 +23,12 @@ tests/e-acsl-runtime/localvar.c:26:[e-acsl] warning: E-ACSL construct `logic fun [value] using specification for function __full_init FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156 [value] using specification for function __delete_block -FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/localvar.c:20:[value] Assertion got status valid. +FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) [value] using specification for function __initialized [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __initialize FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156_0 [value] using specification for function __e_acsl_memory_clean diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle index 62d88b891511673e59d75a1b5235efde47aafe93..05f59d98e5e0b32f63057a2314f237804f7c5d52 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.0.res.oracle @@ -18,35 +18,18 @@ tests/e-acsl-runtime/longlong.i:11:[value] warning: recursive call during value [value] using specification for function my_pow tests/e-acsl-runtime/longlong.i:12:[kernel] warning: signed overflow. assert -2147483648 ≤ tmp*tmp; tests/e-acsl-runtime/longlong.i:12:[kernel] warning: signed overflow. assert tmp*tmp ≤ 2147483647; -tests/e-acsl-runtime/longlong.i:19:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. [value] using specification for function __gmpz_import -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:82:[value] Function __gmpz_import: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:82:[value] warning: function __gmpz_import: precondition got status unknown. [value] using specification for function __gmpz_mul -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:157:[value] Function __gmpz_mul: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid. [value] using specification for function __gmpz_add -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. -tests/e-acsl-runtime/longlong.i:19:[value] Assertion 'E_ACSL' got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_tdiv_r -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:171:[value] Function __gmpz_tdiv_r: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:172:[value] Function __gmpz_tdiv_r: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:173:[value] Function __gmpz_tdiv_r: precondition got status valid. [value] using specification for function __gmpz_get_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid. tests/e-acsl-runtime/longlong.i:19:[kernel] warning: pointer comparison. assert \pointer_comparable((void *)__e_acsl_4, (void *)1); [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle index 5fd7d5e29dbaa816a6764c1c024995dfda165e50..382e1ff4d9982a73481965743000bb0828c5a82b 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/longlong.1.res.oracle @@ -18,33 +18,17 @@ tests/e-acsl-runtime/longlong.i:11:[value] warning: recursive call during value [value] using specification for function my_pow tests/e-acsl-runtime/longlong.i:12:[kernel] warning: signed overflow. assert -2147483648 ≤ tmp*tmp; tests/e-acsl-runtime/longlong.i:12:[kernel] warning: signed overflow. assert tmp*tmp ≤ 2147483647; -tests/e-acsl-runtime/longlong.i:19:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. [value] using specification for function __gmpz_import -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:82:[value] Function __gmpz_import: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:82:[value] warning: function __gmpz_import: precondition got status unknown. [value] using specification for function __gmpz_mul -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:157:[value] Function __gmpz_mul: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid. [value] using specification for function __gmpz_add -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. -tests/e-acsl-runtime/longlong.i:19:[value] Assertion 'E_ACSL' got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_tdiv_r -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:171:[value] Function __gmpz_tdiv_r: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:172:[value] Function __gmpz_tdiv_r: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:173:[value] Function __gmpz_tdiv_r: precondition got status valid. tests/e-acsl-runtime/longlong.i:19:[kernel] warning: pointer comparison. assert \pointer_comparable((void *)__e_acsl_eq, (void *)0); [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.0.res.oracle index 37df3cbad2f71abe2dbd53c0726fe49701b16d02..34f20cf19c253e09f0de059456214d2c02ce6fcb 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.0.res.oracle @@ -11,15 +11,10 @@ __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/loop.i:10:[value] Loop invariant got status valid. -tests/e-acsl-runtime/loop.i:17:[value] Loop invariant got status valid. -tests/e-acsl-runtime/loop.i:19:[value] Loop invariant got status valid. -tests/e-acsl-runtime/loop.i:21:[value] Loop invariant got status unknown. +tests/e-acsl-runtime/loop.i:21:[value] warning: loop invariant got status unknown. [value] Semantic level unrolling superposing up to 100 states tests/e-acsl-runtime/loop.i:21:[value] entering loop for the first time -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status invalid. tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing uninitialized left-value. assert \initialized(&t[__e_acsl_k_2][__e_acsl_l_2]); -tests/e-acsl-runtime/loop.i:28:[value] Loop invariant got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle index 671b142c0380d4f5d044ba919fa3114c0b4e6262..2a9a74a05aa97d694e0cfb1a62dfe96163b5dc64 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/loop.1.res.oracle @@ -11,24 +11,14 @@ __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status invalid. -tests/e-acsl-runtime/loop.i:10:[value] Loop invariant got status valid. -tests/e-acsl-runtime/loop.i:17:[value] Loop invariant got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status invalid. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. [value] using specification for function __gmpz_set -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid. [value] using specification for function __gmpz_get_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid. tests/e-acsl-runtime/loop.i:21:[value] completely invalid value in evaluation of argument (long)t[__e_acsl_k_2][__e_acsl_l_2] tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index. assert __e_acsl_k_2 < 10; @@ -36,21 +26,12 @@ tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index. tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing uninitialized left-value. assert \initialized(&t[__e_acsl_k_2][__e_acsl_l_2]); [value] using specification for function __gmpz_add -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/loop.i:19:[value] Loop invariant got status valid. -tests/e-acsl-runtime/loop.i:21:[value] Loop invariant got status unknown. +tests/e-acsl-runtime/loop.i:21:[value] warning: loop invariant got status unknown. tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index. assert __e_acsl_k_4 < 10; tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing out of bounds index. assert __e_acsl_l_4 < 15; tests/e-acsl-runtime/loop.i:21:[kernel] warning: accessing uninitialized left-value. assert \initialized(&t[__e_acsl_k_4][__e_acsl_l_4]); [value] using specification for function __gmpz_mul -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:157:[value] Function __gmpz_mul: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid. [value] Semantic level unrolling superposing up to 100 states tests/e-acsl-runtime/loop.i:21:[value] entering loop for the first time -tests/e-acsl-runtime/loop.i:28:[value] Loop invariant got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle index db7d99e671c08bdc8eb7d5c58870f1883377fe21..570e5a2cd7ddf866a6a3442f37e6d744e161c11d 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.0.res.oracle @@ -20,31 +20,29 @@ FRAMAC_SHARE/libc/string.h:93:[e-acsl] warning: E-ACSL construct `applying logic __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] [value] using specification for function __init_args -tests/e-acsl-runtime/mainargs.c:12:[value] Assertion got status valid. [value] using specification for function __store_block [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/mainargs.c:13:[value] Assertion got status valid. -tests/e-acsl-runtime/mainargs.c:14:[value] Assertion got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. +tests/e-acsl-runtime/mainargs.c:14:[value] warning: assertion got status unknown. tests/e-acsl-runtime/mainargs.c:14:[value] entering loop for the first time -tests/e-acsl-runtime/mainargs.c:15:[value] Assertion got status unknown. +tests/e-acsl-runtime/mainargs.c:15:[value] warning: assertion got status unknown. [value] using specification for function __block_length -tests/e-acsl-runtime/mainargs.c:17:[value] Assertion got status unknown. +tests/e-acsl-runtime/mainargs.c:17:[value] warning: assertion got status unknown. [value] using specification for function __valid_read tests/e-acsl-runtime/mainargs.c:17:[kernel] warning: out of bounds read. assert \valid_read(argv+argc); -tests/e-acsl-runtime/mainargs.c:18:[value] Assertion got status unknown. +tests/e-acsl-runtime/mainargs.c:18:[value] warning: assertion got status unknown. [value] using specification for function __initialized tests/e-acsl-runtime/mainargs.c:18:[kernel] warning: out of bounds read. assert \valid_read(argv+argc); tests/e-acsl-runtime/mainargs.c:19:[value] entering loop for the first time -FRAMAC_SHARE/libc/string.h:91:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown. +FRAMAC_SHARE/libc/string.h:91:[value] warning: function __e_acsl_strlen: precondition 'valid_string_src' got status unknown. [value] using specification for function strlen -FRAMAC_SHARE/libc/string.h:91:[value] Function 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:91:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates [value] using specification for function __delete_block -FRAMAC_SHARE/libc/string.h:93:[value] Function __e_acsl_strlen: postcondition got status unknown. -tests/e-acsl-runtime/mainargs.c:21:[value] Assertion got status unknown. -tests/e-acsl-runtime/mainargs.c:22:[value] Assertion got status unknown. +FRAMAC_SHARE/libc/string.h:93:[value] warning: function __e_acsl_strlen: postcondition got status unknown. +tests/e-acsl-runtime/mainargs.c:21:[value] warning: assertion got status unknown. +tests/e-acsl-runtime/mainargs.c:22:[value] warning: assertion got status unknown. tests/e-acsl-runtime/mainargs.c:22:[value] entering loop for the first time [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle index d3b2a7b1d26620c85beacd090db3d66dc331e57e..2a1ee9c62a4fb78cb8039f24823f045324341114 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/mainargs.1.res.oracle @@ -20,55 +20,38 @@ FRAMAC_SHARE/libc/string.h:93:[e-acsl] warning: E-ACSL construct `applying logic __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] [value] using specification for function __init_args -tests/e-acsl-runtime/mainargs.c:12:[value] Assertion got status valid. [value] using specification for function __store_block [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/mainargs.c:13:[value] Assertion got status valid. -tests/e-acsl-runtime/mainargs.c:14:[value] Assertion got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. +tests/e-acsl-runtime/mainargs.c:14:[value] warning: assertion got status unknown. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_set -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. tests/e-acsl-runtime/mainargs.c:14:[value] entering loop for the first time [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function __gmpz_get_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid. [value] using specification for function __gmpz_add -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid. -tests/e-acsl-runtime/mainargs.c:15:[value] Assertion got status unknown. +tests/e-acsl-runtime/mainargs.c:15:[value] warning: assertion got status unknown. [value] using specification for function __block_length [value] using specification for function __gmpz_init_set_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid. [value] using specification for function __gmpz_mul -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:157:[value] Function __gmpz_mul: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid. -tests/e-acsl-runtime/mainargs.c:17:[value] Assertion got status unknown. +tests/e-acsl-runtime/mainargs.c:17:[value] warning: assertion got status unknown. [value] using specification for function __valid_read tests/e-acsl-runtime/mainargs.c:17:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)argc); -tests/e-acsl-runtime/mainargs.c:18:[value] Assertion got status unknown. +tests/e-acsl-runtime/mainargs.c:18:[value] warning: assertion got status unknown. [value] using specification for function __initialized tests/e-acsl-runtime/mainargs.c:18:[kernel] warning: out of bounds read. assert \valid_read(argv+(long)argc); tests/e-acsl-runtime/mainargs.c:19:[value] entering loop for the first time -FRAMAC_SHARE/libc/string.h:91:[value] Function __e_acsl_strlen: precondition 'valid_string_src' got status unknown. +FRAMAC_SHARE/libc/string.h:91:[value] warning: function __e_acsl_strlen: precondition 'valid_string_src' got status unknown. [value] using specification for function strlen -FRAMAC_SHARE/libc/string.h:91:[value] Function 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:91:[value] cannot evaluate ACSL term, unsupported ACSL construct: logic functions or predicates [value] using specification for function __delete_block -FRAMAC_SHARE/libc/string.h:93:[value] Function __e_acsl_strlen: postcondition got status unknown. -tests/e-acsl-runtime/mainargs.c:21:[value] Assertion got status unknown. -tests/e-acsl-runtime/mainargs.c:22:[value] Assertion got status unknown. +FRAMAC_SHARE/libc/string.h:93:[value] warning: function __e_acsl_strlen: postcondition got status unknown. +tests/e-acsl-runtime/mainargs.c:21:[value] warning: assertion got status unknown. +tests/e-acsl-runtime/mainargs.c:22:[value] warning: assertion got status unknown. tests/e-acsl-runtime/mainargs.c:22:[value] entering loop for the first time [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.0.res.oracle index 4769e9abc329d64c3555173b0283bb8663baef4e..615aab08721db66c094c650ae74d98e0e4c402d6 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.0.res.oracle @@ -55,10 +55,9 @@ FRAMAC_SHARE/libc/stdlib.h:146:[kernel] warning: Neither code nor specification [value] using specification for function __full_init [value] using specification for function __malloc [value] using specification for function __delete_block -FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/memsize.c:24:[value] Assertion got status unknown. +FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +tests/e-acsl-runtime/memsize.c:24:[value] warning: assertion got status unknown. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/memsize.c:26:[value] Assertion got status invalid (stopping propagation). +tests/e-acsl-runtime/memsize.c:26:[value] warning: assertion got status invalid (stopping propagation). [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.1.res.oracle index b5e711cfb61c3f9c2cd5d263b53933de27f608b1..d832fd1ab14dd163ae0b56d3592049f0695477e9 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/memsize.1.res.oracle @@ -43,19 +43,14 @@ FRAMAC_SHARE/libc/stdlib.h:146:[kernel] warning: Neither code nor specification [value] using specification for function __full_init [value] using specification for function __malloc [value] using specification for function __delete_block -FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/memsize.c:24:[value] Assertion got status unknown. +FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +tests/e-acsl-runtime/memsize.c:24:[value] warning: assertion got status unknown. [value] using specification for function __gmpz_init_set_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/e-acsl-runtime/memsize.c:26:[value] Assertion got status invalid (stopping propagation). +tests/e-acsl-runtime/memsize.c:26:[value] warning: assertion got status invalid (stopping propagation). [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.0.res.oracle index 151f864ecdd500fa488537b7a014ce8494bd6cc5..f0d9dbf6c715c6fb6e5314a8a737295cb93f35a9 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.0.res.oracle @@ -10,7 +10,5 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/nested_code_annot.i:9:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle index 8a8222523676e72bcfd05feaffb8090b026f21e5..af524ffc3d7df40abb2b39677fbbaa828e6cb126 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle @@ -10,14 +10,9 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/nested_code_annot.i:9:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.0.res.oracle index c4513a0cf3efae76f1bcf98037fd67ee37f3150e..f0d9dbf6c715c6fb6e5314a8a737295cb93f35a9 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.0.res.oracle @@ -10,7 +10,5 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/not.i:8:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle index 57e6831e42f440dc422074515b54e430423919e0..af524ffc3d7df40abb2b39677fbbaa828e6cb126 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle @@ -10,14 +10,9 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/not.i:8:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.0.res.oracle index 6d317b9c751dc5b6bcf67ac364b320f0d6fda1d1..f0d9dbf6c715c6fb6e5314a8a737295cb93f35a9 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.0.res.oracle @@ -10,7 +10,5 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/null.i:8:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle index 6d317b9c751dc5b6bcf67ac364b320f0d6fda1d1..f0d9dbf6c715c6fb6e5314a8a737295cb93f35a9 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle @@ -10,7 +10,5 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/null.i:8:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.0.res.oracle index dec8067549f0bf1957e11931a1fba51ccf39a0ef..f0d9dbf6c715c6fb6e5314a8a737295cb93f35a9 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.0.res.oracle @@ -10,8 +10,5 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/other_constants.i:12:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/other_constants.i:13:[value] Assertion got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle index 4c6b098dd0854b40e73fc6e248f2297b735c794b..af524ffc3d7df40abb2b39677fbbaa828e6cb126 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle @@ -10,15 +10,9 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/other_constants.i:12:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/e-acsl-runtime/other_constants.i:13:[value] Assertion got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.0.res.oracle index 3815dcb62e094b9f98b97808c5d4ec59262bacf3..b71f628f99927201274624278f0f7d3aa16c8c1e 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.0.res.oracle @@ -13,23 +13,14 @@ [value] using specification for function __store_block [value] using specification for function __full_init [value] using specification for function __initialize -tests/e-acsl-runtime/ptr.i:13:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function __valid_read [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/ptr.i:14:[value] Assertion got status valid. -tests/e-acsl-runtime/ptr.i:15:[value] Assertion got status valid. -tests/e-acsl-runtime/ptr.i:16:[value] Assertion got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. tests/e-acsl-runtime/ptr.i:18:[value] entering loop for the first time -tests/e-acsl-runtime/ptr.i:19:[value] Assertion got status valid. -tests/e-acsl-runtime/ptr.i:20:[value] Assertion got status valid. -tests/e-acsl-runtime/ptr.i:21:[value] Assertion got status valid. -tests/e-acsl-runtime/ptr.i:19:[value] Assertion got status unknown. -tests/e-acsl-runtime/ptr.i:20:[value] Assertion got status unknown. -tests/e-acsl-runtime/ptr.i:21:[value] Assertion got status unknown. -tests/e-acsl-runtime/ptr.i:27:[value] Assertion got status valid. +tests/e-acsl-runtime/ptr.i:19:[value] warning: assertion got status unknown. +tests/e-acsl-runtime/ptr.i:20:[value] warning: assertion got status unknown. +tests/e-acsl-runtime/ptr.i:21:[value] warning: assertion got status unknown. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle index c2049ced1b91b42cfcebef28fcac4a7b3f83f6e9..f70ee1b37e083b860a60e77ebb9112d9eec0566e 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle @@ -13,50 +13,23 @@ [value] using specification for function __store_block [value] using specification for function __full_init [value] using specification for function __initialize -tests/e-acsl-runtime/ptr.i:13:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/e-acsl-runtime/ptr.i:14:[value] Assertion got status valid. -tests/e-acsl-runtime/ptr.i:15:[value] Assertion got status valid. -tests/e-acsl-runtime/ptr.i:16:[value] Assertion got status valid. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. [value] using specification for function __gmpz_mul -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:157:[value] Function __gmpz_mul: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid. -tests/e-acsl-runtime/ptr.i:16:[value] Assertion 'E_ACSL' got status valid. [value] using specification for function __gmpz_tdiv_q -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:164:[value] Function __gmpz_tdiv_q: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:166:[value] Function __gmpz_tdiv_q: precondition got status valid. [value] using specification for function __gmpz_get_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid. tests/e-acsl-runtime/ptr.i:16:[kernel] warning: accessing out of bounds index. assert __e_acsl_9 < 3; tests/e-acsl-runtime/ptr.i:18:[value] entering loop for the first time -tests/e-acsl-runtime/ptr.i:19:[value] Assertion got status valid. [value] using specification for function __gmpz_add -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid. -tests/e-acsl-runtime/ptr.i:20:[value] Assertion got status valid. [value] using specification for function __gmpz_sub -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:150:[value] Function __gmpz_sub: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:151:[value] Function __gmpz_sub: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:152:[value] Function __gmpz_sub: precondition got status valid. tests/e-acsl-runtime/ptr.i:20:[kernel] warning: accessing out of bounds index. assert __e_acsl_15 < 3; -tests/e-acsl-runtime/ptr.i:21:[value] Assertion got status valid. -tests/e-acsl-runtime/ptr.i:19:[value] Assertion got status unknown. -tests/e-acsl-runtime/ptr.i:20:[value] Assertion got status unknown. -tests/e-acsl-runtime/ptr.i:21:[value] Assertion got status unknown. -tests/e-acsl-runtime/ptr.i:27:[value] Assertion got status valid. +tests/e-acsl-runtime/ptr.i:19:[value] warning: assertion got status unknown. +tests/e-acsl-runtime/ptr.i:20:[value] warning: assertion got status unknown. +tests/e-acsl-runtime/ptr.i:21:[value] warning: assertion got status unknown. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.0.res.oracle index f43059447740071878c53a8503137c8d87361289..21b5d6c647fff39a396d068a1984811e2898f579 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.0.res.oracle @@ -29,14 +29,10 @@ FRAMAC_SHARE/libc/stdlib.h:165:[e-acsl] warning: E-ACSL construct `logic functio [value] using specification for function __full_init [value] using specification for function __malloc [value] using specification for function __delete_block -FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/ptr_init.c:28:[value] Assertion got status valid. +FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/ptr_init.c:29:[value] Assertion got status valid. [value] using specification for function __initialized -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle index c4219110595d31982ec8e4ddd3249c573b6e6e48..2e95ba4b0343eb3ad517b7c0837febe7ea59e5de 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr_init.1.res.oracle @@ -25,14 +25,10 @@ tests/e-acsl-runtime/ptr_init.c:22:[e-acsl] warning: E-ACSL construct `logic fun [value] using specification for function __full_init [value] using specification for function __malloc [value] using specification for function __delete_block -FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/ptr_init.c:28:[value] Assertion got status valid. +FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/ptr_init.c:29:[value] Assertion got status valid. [value] using specification for function __initialized -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/ptr_init.c:19:[value] Assertion got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.0.res.oracle index 953488ee27e808fe594665de5b13b3a3315402c7..e0ebf45e128eca822961123d7e337097f902e58f 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.0.res.oracle @@ -10,22 +10,21 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/quantif.i:11:[value] Assertion got status unknown. +tests/e-acsl-runtime/quantif.i:11:[value] warning: assertion got status unknown. tests/e-acsl-runtime/quantif.i:11:[value] entering loop for the first time [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/quantif.i:12:[value] Assertion got status unknown. +tests/e-acsl-runtime/quantif.i:12:[value] warning: assertion got status unknown. tests/e-acsl-runtime/quantif.i:12:[value] entering loop for the first time -tests/e-acsl-runtime/quantif.i:13:[value] Assertion got status unknown. +tests/e-acsl-runtime/quantif.i:13:[value] warning: assertion got status unknown. tests/e-acsl-runtime/quantif.i:13:[value] entering loop for the first time -tests/e-acsl-runtime/quantif.i:14:[value] Assertion got status unknown. +tests/e-acsl-runtime/quantif.i:14:[value] warning: assertion got status unknown. tests/e-acsl-runtime/quantif.i:14:[value] entering loop for the first time -tests/e-acsl-runtime/quantif.i:18:[value] Assertion got status unknown. +tests/e-acsl-runtime/quantif.i:18:[value] warning: assertion got status unknown. tests/e-acsl-runtime/quantif.i:18:[value] entering loop for the first time -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/quantif.i:23:[value] Assertion got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. +tests/e-acsl-runtime/quantif.i:23:[value] warning: assertion got status unknown. tests/e-acsl-runtime/quantif.i:23:[value] entering loop for the first time -tests/e-acsl-runtime/quantif.i:27:[value] Assertion got status unknown. +tests/e-acsl-runtime/quantif.i:27:[value] warning: assertion got status unknown. tests/e-acsl-runtime/quantif.i:27:[value] entering loop for the first time tests/e-acsl-runtime/quantif.i:28:[value] entering loop for the first time [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle index f57dd54e53ffebbcbf3011c4e11fc11e343db5d8..5f380012785867d1870e6f42134ee0204da33a35 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle @@ -10,51 +10,30 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/quantif.i:11:[value] Assertion got status unknown. +tests/e-acsl-runtime/quantif.i:11:[value] warning: assertion got status unknown. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_set -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:94:[value] Function __gmpz_set: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:95:[value] Function __gmpz_set: precondition got status valid. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. tests/e-acsl-runtime/quantif.i:11:[value] entering loop for the first time [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function __gmpz_add -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/quantif.i:12:[value] Assertion got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. +tests/e-acsl-runtime/quantif.i:12:[value] warning: assertion got status unknown. tests/e-acsl-runtime/quantif.i:12:[value] entering loop for the first time -tests/e-acsl-runtime/quantif.i:13:[value] Assertion got status unknown. +tests/e-acsl-runtime/quantif.i:13:[value] warning: assertion got status unknown. tests/e-acsl-runtime/quantif.i:13:[value] entering loop for the first time -tests/e-acsl-runtime/quantif.i:14:[value] Assertion got status unknown. +tests/e-acsl-runtime/quantif.i:14:[value] warning: assertion got status unknown. tests/e-acsl-runtime/quantif.i:14:[value] entering loop for the first time -tests/e-acsl-runtime/quantif.i:18:[value] Assertion got status unknown. +tests/e-acsl-runtime/quantif.i:18:[value] warning: assertion got status unknown. tests/e-acsl-runtime/quantif.i:18:[value] entering loop for the first time -tests/e-acsl-runtime/quantif.i:23:[value] Assertion got status unknown. +tests/e-acsl-runtime/quantif.i:23:[value] warning: assertion got status unknown. tests/e-acsl-runtime/quantif.i:23:[value] entering loop for the first time -tests/e-acsl-runtime/quantif.i:27:[value] Assertion got status unknown. +tests/e-acsl-runtime/quantif.i:27:[value] warning: assertion got status unknown. tests/e-acsl-runtime/quantif.i:27:[value] entering loop for the first time -tests/e-acsl-runtime/quantif.i:28:[value] Assertion 'E_ACSL' got status valid. [value] using specification for function __gmpz_tdiv_r -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:171:[value] Function __gmpz_tdiv_r: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:172:[value] Function __gmpz_tdiv_r: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:173:[value] Function __gmpz_tdiv_r: precondition got status valid. tests/e-acsl-runtime/quantif.i:28:[value] entering loop for the first time -tests/e-acsl-runtime/quantif.i:28:[value] Assertion 'E_ACSL' got status valid. [value] using specification for function __gmpz_tdiv_q -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:164:[value] Function __gmpz_tdiv_q: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:165:[value] Function __gmpz_tdiv_q: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:166:[value] Function __gmpz_tdiv_q: precondition got status valid. [value] using specification for function __gmpz_mul -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:157:[value] Function __gmpz_mul: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:158:[value] Function __gmpz_mul: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:159:[value] Function __gmpz_mul: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.0.res.oracle index 7ffb06bab752ca3b2195b77a6562e7de54169ede..053606fa32ae592711d0f4658dcbef26a2718cd6 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.0.res.oracle @@ -11,12 +11,5 @@ __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] Y ∈ {1} -tests/e-acsl-runtime/result.i:7:[value] Function f: postcondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/result.i:7:[value] Function __e_acsl_f: postcondition got status valid. -tests/e-acsl-runtime/result.i:18:[value] Function g: postcondition got status valid. -tests/e-acsl-runtime/result.i:18:[value] Function __e_acsl_g: postcondition got status valid. -tests/e-acsl-runtime/result.i:23:[value] Function h: postcondition got status valid. -tests/e-acsl-runtime/result.i:23:[value] Function __e_acsl_h: postcondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle index 768f090efb61438ee48bc21e95b83a5cdeb085a6..f17905f024ed6ed8e75e085bcaaf314b4880723e 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle @@ -11,27 +11,12 @@ __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] Y ∈ {1} -tests/e-acsl-runtime/result.i:7:[value] Function f: postcondition got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. [value] using specification for function __gmpz_sub -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:150:[value] Function __gmpz_sub: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:151:[value] Function __gmpz_sub: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:152:[value] Function __gmpz_sub: precondition got status valid. [value] using specification for function __gmpz_get_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:198:[value] Function __gmpz_get_ui: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -tests/e-acsl-runtime/result.i:7:[value] Function __e_acsl_f: postcondition got status valid. -tests/e-acsl-runtime/result.i:18:[value] Function g: postcondition got status valid. -tests/e-acsl-runtime/result.i:18:[value] Function __e_acsl_g: postcondition got status valid. -tests/e-acsl-runtime/result.i:23:[value] Function h: postcondition got status valid. -tests/e-acsl-runtime/result.i:23:[value] Function __e_acsl_h: postcondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.0.res.oracle index 3d936884430f4315dda3561e2fd36797eceaba98..f0d9dbf6c715c6fb6e5314a8a737295cb93f35a9 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.0.res.oracle @@ -10,7 +10,5 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/sizeof.i:10:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle index 505160e67de12c2668dc9cfc95a4ccbb67ef106b..af524ffc3d7df40abb2b39677fbbaa828e6cb126 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle @@ -10,14 +10,9 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/sizeof.i:10:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle index fb49c3698c32ef96cf5a665efb857c996306c35f..a0141f070c9fed6e0f9642d4663b8e597e06497d 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.0.res.oracle @@ -47,10 +47,9 @@ FRAMAC_SHARE/libc/stdio.h:107:[e-acsl] warning: E-ACSL construct `logic function [value] using specification for function __full_init [value] using specification for function __literal_string [value] using specification for function fopen -FRAMAC_SHARE/libc/stdio.h:106:[value] Function __e_acsl_fopen: postcondition got status valid. -tests/e-acsl-runtime/stdout.c:13:[value] Assertion got status unknown. +tests/e-acsl-runtime/stdout.c:13:[value] warning: assertion got status unknown. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle index c0cb27bc5fd0cba905f3854ffad52e06fb56390d..764e042f2f333a33526fced0f43038e5f282a50c 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stdout.1.res.oracle @@ -47,10 +47,9 @@ FRAMAC_SHARE/libc/stdio.h:106:[e-acsl] warning: E-ACSL construct `logic function [value] using specification for function __full_init [value] using specification for function __literal_string [value] using specification for function fopen -FRAMAC_SHARE/libc/stdio.h:106:[value] Function __e_acsl_fopen: postcondition got status valid. -tests/e-acsl-runtime/stdout.c:13:[value] Assertion got status unknown. +tests/e-acsl-runtime/stdout.c:13:[value] warning: assertion got status unknown. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __delete_block [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.0.res.oracle index 7e1ef6d4aa6f36be6b2098a8fc8ada9ada27fb83..f0d9dbf6c715c6fb6e5314a8a737295cb93f35a9 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.0.res.oracle @@ -11,5 +11,4 @@ __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle index c59e20f10fd17a74290d278d7ea5b649cf70a7d0..ffdab4d22524c62fcda52372fdf7d6549acefe03 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle @@ -11,18 +11,10 @@ __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. [value] using specification for function __gmpz_init -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:39:[value] Function __gmpz_init: precondition got status valid. [value] using specification for function __gmpz_add -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:143:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:144:[value] Function __gmpz_add: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:145:[value] Function __gmpz_add: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.0.res.oracle index 549d5a145b57a3cf106beb3e8cf8f10f6b8d921c..f0d9dbf6c715c6fb6e5314a8a737295cb93f35a9 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.0.res.oracle @@ -10,7 +10,5 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/true.i:10:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle index 549d5a145b57a3cf106beb3e8cf8f10f6b8d921c..f0d9dbf6c715c6fb6e5314a8a737295cb93f35a9 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle @@ -10,7 +10,5 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/true.i:10:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.0.res.oracle index 3e13beeb9f8206ad7c14d7a9d634b55e59cac7fc..f0d9dbf6c715c6fb6e5314a8a737295cb93f35a9 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.0.res.oracle @@ -10,7 +10,5 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/typedef.i:11:[value] Assertion got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle index eff640e073cf9b125066b2b65c845ede4420e963..b6b4bb04ed95620cf6071c806d0b3e188597abe7 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle @@ -10,16 +10,10 @@ __e_acsl_init ∈ [--..--] __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] -tests/e-acsl-runtime/typedef.i:11:[value] Assertion got status valid. [value] using specification for function __gmpz_init_set_ui -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:55:[value] Function __gmpz_init_set_ui: precondition got status valid. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle index 56aa4ebae24aaf2e2853c8334206b779478ccd36..444b435a3dcd2efd9b4b2bfbd31680e9c5207978 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.0.res.oracle @@ -35,43 +35,26 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is Z ∈ {0} [value] using specification for function __store_block [value] using specification for function __full_init -tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156 [value] using specification for function __delete_block -FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/valid.c:37:[value] Assertion got status valid. -tests/e-acsl-runtime/valid.c:39:[value] Assertion got status valid. -tests/e-acsl-runtime/valid.c:15:[value] Function __e_acsl_f: precondition got status valid. -tests/e-acsl-runtime/valid.c:15:[value] Function f: precondition got status valid. -tests/e-acsl-runtime/valid.c:19:[value] Assertion got status valid. -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/valid.c:21:[value] Assertion got status valid. -tests/e-acsl-runtime/valid.c:16:[value] Function f: postcondition got status valid. -tests/e-acsl-runtime/valid.c:16:[value] Function __e_acsl_f: postcondition got status valid. -tests/e-acsl-runtime/valid.c:41:[value] Assertion got status valid. -tests/e-acsl-runtime/valid.c:43:[value] Assertion got status valid. -tests/e-acsl-runtime/valid.c:46:[value] Assertion got status valid. +FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) [value] using specification for function __valid_read -tests/e-acsl-runtime/valid.c:47:[value] Assertion got status valid. -FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. +FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. [value] using specification for function __freeable :0:[value] Assigning imprecise value to __e_acsl_implies. The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178} FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies. It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}. -FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown. -tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid. +FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown. tests/e-acsl-runtime/valid.c:49:[value] completely invalid value in evaluation of argument (void *)a tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses. assert ¬\dangling(&a); -tests/e-acsl-runtime/valid.c:50:[value] Assertion got status valid. -tests/e-acsl-runtime/valid.c:30:[value] Assertion got status valid. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle index e45b62a3e03ea69d8c4d3348f388169bbd133c49..15bf91ef5f0af8deb2f8ed5be276f1fde3307a33 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle @@ -27,43 +27,26 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is Z ∈ {0} [value] using specification for function __store_block [value] using specification for function __full_init -tests/e-acsl-runtime/valid.c:35:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function __valid [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156 [value] using specification for function __delete_block -FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) -tests/e-acsl-runtime/valid.c:37:[value] Assertion got status valid. -tests/e-acsl-runtime/valid.c:39:[value] Assertion got status valid. -tests/e-acsl-runtime/valid.c:15:[value] Function __e_acsl_f: precondition got status valid. -tests/e-acsl-runtime/valid.c:15:[value] Function f: precondition got status valid. -tests/e-acsl-runtime/valid.c:19:[value] Assertion got status valid. -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/valid.c:21:[value] Assertion got status valid. -tests/e-acsl-runtime/valid.c:16:[value] Function f: postcondition got status valid. -tests/e-acsl-runtime/valid.c:16:[value] Function __e_acsl_f: postcondition got status valid. -tests/e-acsl-runtime/valid.c:41:[value] Assertion got status valid. -tests/e-acsl-runtime/valid.c:43:[value] Assertion got status valid. -tests/e-acsl-runtime/valid.c:46:[value] Assertion got status valid. +FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) [value] using specification for function __valid_read -tests/e-acsl-runtime/valid.c:47:[value] Assertion got status valid. -FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. +FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. [value] using specification for function __freeable :0:[value] Assigning imprecise value to __e_acsl_implies. The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178} FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies. It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}. -FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown. -tests/e-acsl-runtime/valid.c:49:[value] Assertion got status valid. +FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown. tests/e-acsl-runtime/valid.c:49:[value] completely invalid value in evaluation of argument (void *)a tests/e-acsl-runtime/valid.c:49:[kernel] warning: accessing left-value that contains escaping addresses. assert ¬\dangling(&a); -tests/e-acsl-runtime/valid.c:50:[value] Assertion got status valid. -tests/e-acsl-runtime/valid.c:30:[value] Assertion got status valid. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle index e867ea1e46ba6b2b4259bd1ae885598c2dc5bf2c..ee78cd2f531c426b963ff033754a2fb576bc14a5 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.0.res.oracle @@ -32,30 +32,25 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] [value] using specification for function __store_block -tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] using specification for function __full_init FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156 [value] using specification for function __delete_block -FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) [value] using specification for function __initialize -tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid. [value] using specification for function __valid -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/valid_alias.c:17:[value] Assertion got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __valid_read -FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. +FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. [value] using specification for function __freeable :0:[value] Assigning imprecise value to __e_acsl_implies. The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178} FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies. It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}. -FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown. -tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid. +FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown. tests/e-acsl-runtime/valid_alias.c:19:[value] completely invalid value in evaluation of argument (void *)a tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses. diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle index 250286e8054158bc0197beb7806654cd1c449c4c..abe5975be18e431dca83df14b958c9756ac86608 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle @@ -24,36 +24,27 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is __e_acsl_internal_heap ∈ [--..--] __memory_size ∈ [--..--] [value] using specification for function __store_block -tests/e-acsl-runtime/valid_alias.c:12:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. [value] using specification for function __full_init FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156 [value] using specification for function __delete_block -FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) [value] using specification for function __initialize -tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid. [value] using specification for function __valid -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. -tests/e-acsl-runtime/valid_alias.c:17:[value] Assertion got status valid. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. +FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. [value] using specification for function __freeable :0:[value] Assigning imprecise value to __e_acsl_implies. The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178} FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies. It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}. -FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown. -tests/e-acsl-runtime/valid_alias.c:19:[value] Assertion got status valid. +FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown. tests/e-acsl-runtime/valid_alias.c:19:[value] completely invalid value in evaluation of argument (void *)a tests/e-acsl-runtime/valid_alias.c:19:[kernel] warning: accessing left-value that contains escaping addresses. diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.0.res.oracle index 47b252b6e28e1f578cc74ae87b45af269855d08b..3ae32e3ef4f528f185deee6287ac47b57d7de41a 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.0.res.oracle @@ -15,16 +15,11 @@ [value] using specification for function __initialized [value] using specification for function __valid_read [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. tests/e-acsl-runtime/valid_in_contract.c:21:[value] completely invalid value in evaluation of argument (void *)l->next tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read. assert \valid_read(&l->next); [value] using specification for function __full_init [value] using specification for function __delete_block -tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid. -tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function __e_acsl_f, behavior B1: postcondition got status valid. -tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.) [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle index 47b252b6e28e1f578cc74ae87b45af269855d08b..3ae32e3ef4f528f185deee6287ac47b57d7de41a 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_in_contract.1.res.oracle @@ -15,16 +15,11 @@ [value] using specification for function __initialized [value] using specification for function __valid_read [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. tests/e-acsl-runtime/valid_in_contract.c:21:[value] completely invalid value in evaluation of argument (void *)l->next tests/e-acsl-runtime/valid_in_contract.c:21:[kernel] warning: out of bounds read. assert \valid_read(&l->next); [value] using specification for function __full_init [value] using specification for function __delete_block -tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function f, behavior B1: postcondition got status valid. -tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status valid. -tests/e-acsl-runtime/valid_in_contract.c:18:[value] Function __e_acsl_f, behavior B1: postcondition got status valid. -tests/e-acsl-runtime/valid_in_contract.c:22:[value] Function __e_acsl_f, behavior B2: postcondition got status valid. (Behavior may be inactive, no reduction performed.) [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle index a4d6c584761e714e906fbff5d7754489519c5866..e1d8fe9f8046126203e87bd5af370b27d8a23cdf 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.0.res.oracle @@ -34,26 +34,25 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is LAST ∈ {0} [value] using specification for function __store_block [value] using specification for function __initialize -tests/e-acsl-runtime/vector.c:26:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __full_init FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156 [value] using specification for function __delete_block -FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/vector.c:16:[value] entering loop for the first time -tests/e-acsl-runtime/vector.c:29:[value] Assertion got status unknown. -tests/e-acsl-runtime/vector.c:30:[value] Assertion got status unknown. +tests/e-acsl-runtime/vector.c:29:[value] warning: assertion got status unknown. +tests/e-acsl-runtime/vector.c:30:[value] warning: assertion got status unknown. tests/e-acsl-runtime/vector.c:30:[kernel] warning: accessing uninitialized left-value. assert \initialized(&LAST); -FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. +FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. [value] using specification for function __freeable :0:[value] Assigning imprecise value to __e_acsl_implies. The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178} FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies. It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}. -FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown. +FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle index 449c89e8f5ea578aa172378cb4285ad035500188..0055ceb37e74217117f644469918125c5c364961 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/vector.1.res.oracle @@ -26,33 +26,28 @@ FRAMAC_SHARE/libc/stdlib.h:177:[e-acsl] warning: E-ACSL construct `\allocate' is LAST ∈ {0} [value] using specification for function __store_block [value] using specification for function __initialize -tests/e-acsl-runtime/vector.c:26:[value] Assertion got status valid. [value] using specification for function __initialized [value] using specification for function e_acsl_assert -FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] Function e_acsl_assert: precondition got status unknown. +FRAMAC_SHARE/e-acsl/e_acsl.h:34:[value] warning: function e_acsl_assert: precondition got status unknown. [value] using specification for function __full_init FRAMAC_SHARE/libc/stdlib.h:156:[value] allocating variable __malloc___e_acsl_malloc_l156 [value] using specification for function __delete_block -FRAMAC_SHARE/libc/stdlib.h:163:[value] Function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) -FRAMAC_SHARE/libc/stdlib.h:168:[value] Function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:163:[value] warning: function __e_acsl_malloc, behavior allocation: postcondition got status unknown. (Behavior may be inactive, no reduction performed.) +FRAMAC_SHARE/libc/stdlib.h:168:[value] warning: function __e_acsl_malloc, behavior no_allocation: postcondition got status invalid. (Behavior may be inactive, no reduction performed.) tests/e-acsl-runtime/vector.c:16:[value] entering loop for the first time -tests/e-acsl-runtime/vector.c:29:[value] Assertion got status unknown. -tests/e-acsl-runtime/vector.c:30:[value] Assertion got status unknown. +tests/e-acsl-runtime/vector.c:29:[value] warning: assertion got status unknown. +tests/e-acsl-runtime/vector.c:30:[value] warning: assertion got status unknown. tests/e-acsl-runtime/vector.c:30:[kernel] warning: accessing uninitialized left-value. assert \initialized(&LAST); [value] using specification for function __gmpz_init_set_si -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:64:[value] Function __gmpz_init_set_si: precondition got status valid. [value] using specification for function __gmpz_cmp -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:127:[value] Function __gmpz_cmp: precondition got status valid. -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:128:[value] Function __gmpz_cmp: precondition got status valid. [value] using specification for function __gmpz_clear -FRAMAC_SHARE/e-acsl/e_acsl_gmp.h:117:[value] Function __gmpz_clear: precondition got status valid. -FRAMAC_SHARE/libc/stdlib.h:178:[value] Function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. +FRAMAC_SHARE/libc/stdlib.h:178:[value] warning: function __e_acsl_free, behavior deallocation: precondition 'freeable' got status unknown. [value] using specification for function __freeable :0:[value] Assigning imprecise value to __e_acsl_implies. The imprecision originates from Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178} FRAMAC_SHARE/libc/stdlib.h:178:[value] Reading left-value __e_acsl_implies. It contains a garbled mix of {__malloc___e_acsl_malloc_l156} because of Arithmetic {FRAMAC_SHARE/libc/stdlib.h:178}. -FRAMAC_SHARE/libc/stdlib.h:180:[value] Function __e_acsl_free, behavior deallocation: postcondition got status unknown. +FRAMAC_SHARE/libc/stdlib.h:180:[value] warning: function __e_acsl_free, behavior deallocation: postcondition got status unknown. [value] using specification for function __e_acsl_memory_clean [value] done for function main