From 5351eaba85bf93daa6f9c6a27407bc478de19f70 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 26 Mar 2021 13:58:14 +0100
Subject: [PATCH] [wp] conforms to EXIT
---
src/plugins/wp/tests/wp_plugin/bigarray.c | 2 ++
.../wp/tests/wp_plugin/oracle/bigarray.0.res.oracle | 6 +++---
.../wp/tests/wp_plugin/oracle/bigarray.1.res.oracle | 8 ++++----
3 files changed, 9 insertions(+), 7 deletions(-)
diff --git a/src/plugins/wp/tests/wp_plugin/bigarray.c b/src/plugins/wp/tests/wp_plugin/bigarray.c
index 266998147bf..05b9c3f9bce 100644
--- a/src/plugins/wp/tests/wp_plugin/bigarray.c
+++ b/src/plugins/wp/tests/wp_plugin/bigarray.c
@@ -1,5 +1,7 @@
/* run.config
+ EXIT: 0
OPT: -cpp-extra-args="-DFIT"
+ EXIT: 1
OPT: -cpp-extra-args="-DLARGE"
*/
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bigarray.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.0.res.oracle
index c62b8402ac0..9fd78a23491 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/bigarray.0.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.0.res.oracle
@@ -1,6 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/bigarray.c (with preprocessing)
-[kernel] tests/wp_plugin/bigarray.c:26: Warning:
+[kernel] tests/wp_plugin/bigarray.c:28: Warning:
Cannot represent length of array as an attribute
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
@@ -8,13 +8,13 @@
Function f
------------------------------------------------------------
-Goal Loop assigns (file tests/wp_plugin/bigarray.c, line 25):
+Goal Loop assigns (file tests/wp_plugin/bigarray.c, line 27):
Prove: true.
------------------------------------------------------------
Goal Assigns nothing in 'f':
-Effect at line 26
+Effect at line 28
Prove: true.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bigarray.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.1.res.oracle
index 08244d758f0..f997c62a18c 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/bigarray.1.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.1.res.oracle
@@ -1,13 +1,13 @@
# frama-c -wp [...]
[kernel] Parsing tests/wp_plugin/bigarray.c (with preprocessing)
-[kernel] tests/wp_plugin/bigarray.c:26: Warning:
+[kernel] tests/wp_plugin/bigarray.c:28: Warning:
Cannot represent length of array as an attribute
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
-[wp] tests/wp_plugin/bigarray.c:26: Warning:
+[wp] tests/wp_plugin/bigarray.c:28: Warning:
Array size too large (0xFFFFFFFFFFFFFFFF)
-[wp] tests/wp_plugin/bigarray.c:27: Warning:
+[wp] tests/wp_plugin/bigarray.c:29: Warning:
Array size too large (0xFFFFFFFFFFFFFFFF)
-[wp] tests/wp_plugin/bigarray.c:19: User Error:
+[wp] tests/wp_plugin/bigarray.c:21: User Error:
Array size too large (0xFFFFFFFFFFFFFFFF)
[kernel] Plug-in wp aborted: invalid user input.
--
GitLab