From 3bb699eb6356f05e58afe75f25d0ed6dd8728aca Mon Sep 17 00:00:00 2001
From: Julien Signoles <julien.signoles@cea.fr>
Date: Mon, 23 Apr 2012 13:23:55 +0000
Subject: [PATCH] [E-ACSL] update tests according to Value's changes
---
.../tests/e-acsl-runtime/oracle/at.1.res.oracle | 14 ++++++++++++++
.../tests/e-acsl-runtime/oracle/at.res.oracle | 14 ++++++++++++++
.../e-acsl-runtime/oracle/comparison.1.res.oracle | 2 ++
.../e-acsl-runtime/oracle/comparison.res.oracle | 2 ++
.../tests/e-acsl-runtime/oracle/null.1.res.oracle | 2 +-
.../tests/e-acsl-runtime/oracle/null.res.oracle | 2 +-
.../oracle/other_constants.1.res.oracle | 2 ++
.../oracle/other_constants.res.oracle | 2 ++
8 files changed, 38 insertions(+), 2 deletions(-)
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 399b44fc764..1ef42679fd6 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 a5c5c549f1c..11c2e947f89 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 be718900a91..3bbb69ed5dc 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 ea92e0e330d..d28013ed3c6 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 ab6c33e94b5..be26a39c375 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 ab6c33e94b5..be26a39c375 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 1deb1f69c3c..e21ba3d18b0 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 9f3ef2a8c53..5b085420e39 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.
--
GitLab