From e2358b0612a5dbf67b417f6de8fdf59f6b7e40a6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 18 Feb 2019 10:44:47 +0100
Subject: [PATCH] [wp] update builtin names in oracles
---
.../wp_acsl/float_compare.i.0.report.json | 39 +++++++++++++++++++
.../wp_acsl/oracle/classify_float.res.oracle | 6 +--
.../wp_acsl/oracle/float_compare.res.oracle | 16 ++++----
.../oracle_qualif/float_compare.res.oracle | 17 ++++++++
4 files changed, 67 insertions(+), 11 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_acsl/float_compare.i.0.report.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle
diff --git a/src/plugins/wp/tests/wp_acsl/float_compare.i.0.report.json b/src/plugins/wp/tests/wp_acsl/float_compare.i.0.report.json
new file mode 100644
index 00000000000..8ab9ce87bfc
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/float_compare.i.0.report.json
@@ -0,0 +1,39 @@
+{ "wp:global": { "alt-ergo": { "total": 4, "valid": 4, "rank": 8 },
+ "wp:main": { "total": 4, "valid": 4, "rank": 8 } },
+ "wp:axiomatics": { "": { "lemma_test_float_compare_greater": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "lemma_test_float_compare": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main": { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "lemma_test_double_compare_greater": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "lemma_test_double_compare": { "alt-ergo":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 },
+ "wp:main":
+ { "total": 1,
+ "valid": 1,
+ "rank": 8 } },
+ "wp:section": { "alt-ergo": { "total": 4,
+ "valid": 4,
+ "rank": 8 },
+ "wp:main": { "total": 4,
+ "valid": 4,
+ "rank": 8 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle
index c376b86e98c..8ce615934da 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/classify_float.res.oracle
@@ -8,17 +8,17 @@
Lemma InfN_not_finite:
Assume: 'InfP_not_finite' 'NaN_not_finite'
-Prove: (not (\is_finite x_0)) \/ (not (\is_minus_infinity x_0))
+Prove: (not (is_finite_f64 x_0)) \/ (not (is_negative_infinite_f64 x_0))
------------------------------------------------------------
Lemma InfP_not_finite:
Assume: 'NaN_not_finite'
-Prove: (not (\is_finite x_0)) \/ (not (\is_plus_infinity x_0))
+Prove: (not (is_finite_f64 x_0)) \/ (not (is_positive_infinite_f64 x_0))
------------------------------------------------------------
Lemma NaN_not_finite:
-Prove: (not (\is_finite x_0)) \/ (not (\is_NaN x_0))
+Prove: (not (is_finite_f64 x_0)) \/ (not (is_NaN_f64 x_0))
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
index f4648555636..a31e1893ff7 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/float_compare.res.oracle
@@ -8,28 +8,28 @@
Lemma test_double_compare:
Assume: 'test_float_compare'
-Prove: (\is_finite x_0) -> (\is_finite y_0) -> (\le_double x_0 y_0)
- -> ((\lt_double x_0 y_0) \/ (\eq_double x_0 y_0))
+Prove: (is_finite_f64 x_0) -> (is_finite_f64 y_0) -> (le_f64 x_0 y_0)
+ -> ((eq_f64 x_0 y_0) \/ (lt_f64 x_0 y_0))
------------------------------------------------------------
Lemma test_double_compare_greater:
Assume: 'test_float_compare_greater' 'test_double_compare'
'test_float_compare'
-Prove: (\is_finite x_0) -> (\is_finite y_0) -> (\le_double y_0 x_0)
- -> ((\lt_double y_0 x_0) \/ (\eq_double x_0 y_0))
+Prove: (is_finite_f64 x_0) -> (is_finite_f64 y_0) -> (le_f64 y_0 x_0)
+ -> ((eq_f64 x_0 y_0) \/ (lt_f64 y_0 x_0))
------------------------------------------------------------
Lemma test_float_compare:
-Prove: (\is_finite x_0) -> (\is_finite y_0) -> (\le_float x_0 y_0)
- -> ((\lt_float x_0 y_0) \/ (\eq_float x_0 y_0))
+Prove: (is_finite_f32 x_0) -> (is_finite_f32 y_0) -> (le_f32 x_0 y_0)
+ -> ((eq_f32 x_0 y_0) \/ (lt_f32 x_0 y_0))
------------------------------------------------------------
Lemma test_float_compare_greater:
Assume: 'test_double_compare' 'test_float_compare'
-Prove: (\is_finite x_0) -> (\is_finite y_0) -> (\le_float y_0 x_0)
- -> ((\lt_float y_0 x_0) \/ (\eq_float x_0 y_0))
+Prove: (is_finite_f32 x_0) -> (is_finite_f32 y_0) -> (le_f32 y_0 x_0)
+ -> ((eq_f32 x_0 y_0) \/ (lt_f32 y_0 x_0))
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle
new file mode 100644
index 00000000000..828ad921cb7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.res.oracle
@@ -0,0 +1,17 @@
+# frama-c -wp -wp-timeout 90 -wp-steps 1500 [...]
+[kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] 4 goals scheduled
+[wp] [Alt-Ergo] Goal typed_lemma_test_double_compare : Valid
+[wp] [Alt-Ergo] Goal typed_lemma_test_double_compare_greater : Valid
+[wp] [Alt-Ergo] Goal typed_lemma_test_float_compare : Valid
+[wp] [Alt-Ergo] Goal typed_lemma_test_float_compare_greater : Valid
+[wp] Proved goals: 4 / 4
+ Qed: 0
+ Alt-Ergo: 4
+[wp] Report 'tests/wp_acsl/float_compare.i.0.report.json'
+-------------------------------------------------------------
+Axiomatics WP Alt-Ergo Total Success
+Lemma - 4 (28..40) 4 100%
+-------------------------------------------------------------
--
GitLab