From 819e4ddad06543fcd6056323f4cee8e1a0fe2eb2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 23 Feb 2021 16:14:24 +0100
Subject: [PATCH] [aorai] updated tests wrt new upgraded wp
---
.../aorai/tests/ya/oracle_prove/declared_function.res.oracle | 4 ++--
src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle | 2 +-
src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle | 4 ++--
.../aorai/tests/ya/oracle_prove/test_acces_params.res.oracle | 2 --
.../aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle | 2 --
5 files changed, 5 insertions(+), 9 deletions(-)
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
index 500161bb9b8..7ae3924febd 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/ya/declared_function.i (no preprocessing)
[kernel] Parsing TMPDIR/aorai_declared_function_0.i (no preprocessing)
-[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0.i:50: Warning:
- Neither code nor specification for function f, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
+[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0.i:105: Warning:
+ Neither code nor specification for function f, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
index 30ba0541d81..45281711822 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
@@ -2,5 +2,5 @@
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing TMPDIR/aorai_incorrect_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0.i:69: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0.i:70: Warning:
Neither code nor specification for function f, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
index 2dd3de37879..504add72c15 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/serial.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing tests/ya/serial.c (with preprocessing)
[kernel] Parsing TMPDIR/aorai_serial_0.i (no preprocessing)
-[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:738: Warning:
- Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
+[kernel:annot:missing-spec] TMPDIR/aorai_serial_0.i:1450: Warning:
+ Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle
index 0bf1b088bf5..6af6c903d75 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params.res.oracle
@@ -1,5 +1,3 @@
[kernel] Parsing tests/ya/test_acces_params.c (with preprocessing)
[kernel] Parsing TMPDIR/aorai_test_acces_params_0.i (no preprocessing)
-[wp] TMPDIR/aorai_test_acces_params_0.i:4: Warning:
- Global invariant not handled yet ('inv' ignored)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle
index 82a83a9128b..9e85d00f9ba 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/test_acces_params2.res.oracle
@@ -1,5 +1,3 @@
[kernel] Parsing tests/ya/test_acces_params2.c (with preprocessing)
[kernel] Parsing TMPDIR/aorai_test_acces_params2_0.i (no preprocessing)
-[wp] TMPDIR/aorai_test_acces_params2_0.i:3: Warning:
- Global invariant not handled yet ('inv' ignored)
[wp] Warning: Missing RTE guards
--
GitLab