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 399b44fc764c07acec092f1d873b3a378d4802cb..1ef42679fd65765b6e8cc711958134a1e7ad0d4e 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 @@ -92,6 +92,8 @@ PROJECT_FILE.i:247:[value] Assertion got status valid. [value] computing for function __gmpz_clear <- f <- main. Called from PROJECT_FILE.i:257. [value] Done for function __gmpz_clear +PROJECT_FILE.i:261:[value] cannot evaluate ACSL term, + unsupported ACSL construct: \at() on a C label PROJECT_FILE.i:261:[value] Assertion got status unknown. [value] computing for function __gmpz_init_set_si <- f <- main. Called from PROJECT_FILE.i:266. @@ -132,6 +134,8 @@ PROJECT_FILE.i:275:[value] Assertion got status valid. [value] computing for function __gmpz_clear <- f <- main. Called from PROJECT_FILE.i:286. [value] Done for function __gmpz_clear +PROJECT_FILE.i:290:[value] cannot evaluate ACSL term, + unsupported ACSL construct: \at() on a C label PROJECT_FILE.i:290:[value] Assertion got status unknown. [value] computing for function __gmpz_init_set_si <- f <- main. Called from PROJECT_FILE.i:295. @@ -174,6 +178,8 @@ PROJECT_FILE.i:290:[value] Assertion got status unknown. PROJECT_FILE.i:231:[value] Function f: postcondition got status valid. [value] Recording results for f [value] Done for function f +PROJECT_FILE.i:418:[value] cannot evaluate ACSL term, + unsupported ACSL construct: \at() on a C label PROJECT_FILE.i:418:[value] Assertion got status unknown. [value] computing for function __gmpz_init_set_si <- main. Called from PROJECT_FILE.i:423. @@ -194,6 +200,8 @@ PROJECT_FILE.i:418:[value] Assertion got status unknown. [value] computing for function __gmpz_clear <- main. Called from PROJECT_FILE.i:428. [value] Done for function __gmpz_clear +PROJECT_FILE.i:432:[value] cannot evaluate ACSL term, + unsupported ACSL construct: \at() on a C label PROJECT_FILE.i:432:[value] Assertion got status unknown. [value] computing for function __gmpz_init_set_si <- main. Called from PROJECT_FILE.i:436. @@ -208,6 +216,8 @@ PROJECT_FILE.i:432:[value] Assertion got status unknown. [value] computing for function __gmpz_clear <- main. Called from PROJECT_FILE.i:439. [value] Done for function __gmpz_clear +PROJECT_FILE.i:443:[value] cannot evaluate ACSL term, + unsupported ACSL construct: \at() on a C label PROJECT_FILE.i:443:[value] Assertion got status unknown. [value] computing for function __gmpz_init_set_si <- main. Called from PROJECT_FILE.i:449. @@ -239,6 +249,8 @@ PROJECT_FILE.i:443:[value] Assertion got status unknown. [value] Done for function __gmpz_clear [value] computing for function g <- main. Called from PROJECT_FILE.i:461. +PROJECT_FILE.i:340:[value] cannot evaluate ACSL term, + unsupported ACSL construct: \at() on a C label PROJECT_FILE.i:340:[value] Assertion got status unknown. [value] computing for function __gmpz_init_set_si <- g <- main. Called from PROJECT_FILE.i:345. @@ -259,6 +271,8 @@ PROJECT_FILE.i:340:[value] Assertion got status unknown. [value] computing for function __gmpz_clear <- g <- main. Called from PROJECT_FILE.i:351. [value] Done for function __gmpz_clear +PROJECT_FILE.i:356:[value] cannot evaluate ACSL term, + unsupported ACSL construct: \at() on a C label PROJECT_FILE.i:356:[value] Assertion got status unknown. [value] computing for function __gmpz_init_set_si <- g <- main. Called from PROJECT_FILE.i:362. diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle index a5c5c549f1c9a4cfaf798c1743800c7c74c28d22..11c2e947f8959bef399aadf111dcfde0dae873a1 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle @@ -22,6 +22,8 @@ PROJECT_FILE.i:247:[value] Assertion got status valid. Called from PROJECT_FILE.i:248. [value] Recording results for e_acsl_assert [value] Done for function e_acsl_assert +PROJECT_FILE.i:250:[value] cannot evaluate ACSL term, + unsupported ACSL construct: \at() on a C label PROJECT_FILE.i:250:[value] Assertion got status unknown. [value] computing for function e_acsl_assert <- f <- main. Called from PROJECT_FILE.i:251. @@ -32,6 +34,8 @@ PROJECT_FILE.i:253:[value] Assertion got status valid. Called from PROJECT_FILE.i:255. [value] Recording results for e_acsl_assert [value] Done for function e_acsl_assert +PROJECT_FILE.i:257:[value] cannot evaluate ACSL term, + unsupported ACSL construct: \at() on a C label PROJECT_FILE.i:257:[value] Assertion got status unknown. [value] computing for function e_acsl_assert <- f <- main. Called from PROJECT_FILE.i:258. @@ -44,16 +48,22 @@ PROJECT_FILE.i:257:[value] Assertion got status unknown. PROJECT_FILE.i:231:[value] Function f: postcondition got status valid. [value] Recording results for f [value] Done for function f +PROJECT_FILE.i:317:[value] cannot evaluate ACSL term, + unsupported ACSL construct: \at() on a C label PROJECT_FILE.i:317:[value] Assertion got status unknown. [value] computing for function e_acsl_assert <- main. Called from PROJECT_FILE.i:318. [value] Recording results for e_acsl_assert [value] Done for function e_acsl_assert +PROJECT_FILE.i:320:[value] cannot evaluate ACSL term, + unsupported ACSL construct: \at() on a C label PROJECT_FILE.i:320:[value] Assertion got status unknown. [value] computing for function e_acsl_assert <- main. Called from PROJECT_FILE.i:321. [value] Recording results for e_acsl_assert [value] Done for function e_acsl_assert +PROJECT_FILE.i:324:[value] cannot evaluate ACSL term, + unsupported ACSL construct: \at() on a C label PROJECT_FILE.i:324:[value] Assertion got status unknown. [value] computing for function e_acsl_assert <- main. Called from PROJECT_FILE.i:325. @@ -61,11 +71,15 @@ PROJECT_FILE.i:324:[value] Assertion got status unknown. [value] Done for function e_acsl_assert [value] computing for function g <- main. Called from PROJECT_FILE.i:328. +PROJECT_FILE.i:285:[value] cannot evaluate ACSL term, + unsupported ACSL construct: \at() on a C label PROJECT_FILE.i:285:[value] Assertion got status unknown. [value] computing for function e_acsl_assert <- g <- main. Called from PROJECT_FILE.i:286. [value] Recording results for e_acsl_assert [value] Done for function e_acsl_assert +PROJECT_FILE.i:290:[value] cannot evaluate ACSL term, + unsupported ACSL construct: \at() on a C label PROJECT_FILE.i:290:[value] Assertion got status unknown. [value] computing for function e_acsl_assert <- g <- main. Called from PROJECT_FILE.i:292. 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 be718900a9126ecade137b82fd289d9579bf295f..3bbb69ed5dcfa5206fab0b9db878c3b7c56bb3be 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 @@ -96,6 +96,8 @@ PROJECT_FILE.i:295:[value] Assertion got status valid. PROJECT_FILE.i:221:[value] Function e_acsl_assert: precondition got status valid. [value] Recording results for e_acsl_assert [value] Done for function e_acsl_assert +PROJECT_FILE.i:298:[value] cannot evaluate ACSL term, + unsupported ACSL construct: unsupported ACSL construct "toto" PROJECT_FILE.i:298:[value] Assertion got status unknown. [value] computing for function e_acsl_assert <- main. Called from PROJECT_FILE.i:299. diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle index ea92e0e330db44f6e5a1517b37117c6f45d33ea2..d28013ed3c6e8fa05a81bcdd236d4d9d40e97ca2 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle @@ -28,6 +28,8 @@ PROJECT_FILE.i:251:[value] Assertion got status valid. Called from PROJECT_FILE.i:252. [value] Recording results for e_acsl_assert [value] Done for function e_acsl_assert +PROJECT_FILE.i:254:[value] cannot evaluate ACSL term, + unsupported ACSL construct: unsupported ACSL construct "toto" PROJECT_FILE.i:254:[value] Assertion got status unknown. [value] computing for function e_acsl_assert <- main. Called from PROJECT_FILE.i:255. 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 ab6c33e94b536cc1218655382dcdf359fccfeebb..be26a39c375869068565eac3a5fcbe8c88ae4f05 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 @@ -2,7 +2,7 @@ [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization -PROJECT_FILE.i:233:[value] Assertion got status unknown. +PROJECT_FILE.i:233:[value] Assertion got status valid. [value] computing for function e_acsl_assert <- main. Called from PROJECT_FILE.i:234. PROJECT_FILE.i:221:[value] Function e_acsl_assert: precondition got status valid. diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle index ab6c33e94b536cc1218655382dcdf359fccfeebb..be26a39c375869068565eac3a5fcbe8c88ae4f05 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle @@ -2,7 +2,7 @@ [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization -PROJECT_FILE.i:233:[value] Assertion got status unknown. +PROJECT_FILE.i:233:[value] Assertion got status valid. [value] computing for function e_acsl_assert <- main. Called from PROJECT_FILE.i:234. PROJECT_FILE.i:221:[value] Function e_acsl_assert: precondition got status valid. 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 1deb1f69c3cf3b2a30451be0a15f58caa7d6d54a..e21ba3d18b09b78966f76b238370802dfa968152 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 @@ -2,6 +2,8 @@ [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization +PROJECT_FILE.i:237:[value] cannot evaluate ACSL term, + unsupported ACSL construct: unsupported ACSL construct "toto" PROJECT_FILE.i:237:[value] Assertion got status unknown. [value] computing for function e_acsl_assert <- main. Called from PROJECT_FILE.i:238. diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle index 9f3ef2a8c533ce12f3f122c3662efedc4543fa50..5b085420e3919b94f0a8f914ef2e58cd4428942d 100644 --- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle +++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle @@ -2,6 +2,8 @@ [value] Computing initial state [value] Initial state computed [value] Values of globals at initialization +PROJECT_FILE.i:237:[value] cannot evaluate ACSL term, + unsupported ACSL construct: unsupported ACSL construct "toto" PROJECT_FILE.i:237:[value] Assertion got status unknown. [value] computing for function e_acsl_assert <- main. Called from PROJECT_FILE.i:238.