From 1113158137fab9fd039dc74fe08e752688e37428 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 8 Oct 2019 10:23:34 +0200
Subject: [PATCH] [wp] upgrade float oracles for qualif tests
---
.../wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle | 2 +-
.../wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle | 2 +-
.../cache/0229e4d03dbe5dab56c7710d10ede856.json | 2 ++
.../cache/5a2626cdfff12f90f4c43a8b11ff70fb.json | 2 ++
.../cache/d189bb3b47019848c9af5b14c2febb1c.json | 2 ++
.../cache/e2c00d7a3ff17960fa10dee8b619ee99.json | 2 ++
6 files changed, 10 insertions(+), 2 deletions(-)
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/0229e4d03dbe5dab56c7710d10ede856.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/5a2626cdfff12f90f4c43a8b11ff70fb.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/d189bb3b47019848c9af5b14c2febb1c.json
create mode 100644 src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/e2c00d7a3ff17960fa10dee8b619ee99.json
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle
index 0d2d5f9b4b0..ab4451e7b05 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.3.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-model 'Typed (Real)' -wp-timeout 45 -wp-steps 1500 [...]
+# frama-c -wp -wp-model 'Typed (Real)' [...]
[kernel] Parsing tests/wp_acsl/classify_float.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle
index df0b9d2b623..d2cccc3d319 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.res.oracle
@@ -1,4 +1,4 @@
-# frama-c -wp -wp-model 'Typed (Real)' -wp-timeout 45 -wp-steps 1500 [...]
+# frama-c -wp -wp-model 'Typed (Real)' [...]
[kernel] Parsing tests/wp_acsl/float_compare.i (no preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/0229e4d03dbe5dab56c7710d10ede856.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/0229e4d03dbe5dab56c7710d10ede856.json
new file mode 100644
index 00000000000..b875f728786
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/0229e4d03dbe5dab56c7710d10ede856.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0057,
+ "steps": 4 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/5a2626cdfff12f90f4c43a8b11ff70fb.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/5a2626cdfff12f90f4c43a8b11ff70fb.json
new file mode 100644
index 00000000000..cdba4fe1135
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/5a2626cdfff12f90f4c43a8b11ff70fb.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0047,
+ "steps": 4 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/d189bb3b47019848c9af5b14c2febb1c.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/d189bb3b47019848c9af5b14c2febb1c.json
new file mode 100644
index 00000000000..16eacff0af6
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/d189bb3b47019848c9af5b14c2febb1c.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0056,
+ "steps": 4 }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/e2c00d7a3ff17960fa10dee8b619ee99.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/e2c00d7a3ff17960fa10dee8b619ee99.json
new file mode 100644
index 00000000000..4d58671fa0e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/float_compare.1.session/cache/e2c00d7a3ff17960fa10dee8b619ee99.json
@@ -0,0 +1,2 @@
+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.005,
+ "steps": 4 }
--
GitLab