From f983d513084ce4f00efe69ffdf04d2cb0f5c7dca Mon Sep 17 00:00:00 2001
From: Lionel Blatter <lionel.blatter@kit.edu>
Date: Tue, 7 Jul 2020 14:50:51 +0200
Subject: [PATCH] Update test and oracle for recursive extended global
annotations
---
tests/spec/Extend_recursive_preprocess.i | 11 ++++++
.../Extend_recursive_preprocess.res.oracle | 37 ++++++++++++-------
2 files changed, 34 insertions(+), 14 deletions(-)
diff --git a/tests/spec/Extend_recursive_preprocess.i b/tests/spec/Extend_recursive_preprocess.i
index 6bd8a322856..7084d95178b 100644
--- a/tests/spec/Extend_recursive_preprocess.i
+++ b/tests/spec/Extend_recursive_preprocess.i
@@ -2,7 +2,18 @@
MODULE: @PTEST_DIR@/@PTEST_NAME@.cmxs
OPT: -no-autoload-plugins -kernel-warn-key=annot-error=active -print
*/
+/*@ gl_foo foo1 {
+ gl_fooo must_replace(x);
+ gl_fooo must_replace(x);
+ gl_fooo must_replace(x);
+}*/
+
+/*@ gl_foo foo1 {
+ gl_foo foo2 {
+ gl_fooo must_replace(x);
+ }
+}*/
/*@ gl_foo foo1 {
gl_fooo must_replace(x);
diff --git a/tests/spec/oracle/Extend_recursive_preprocess.res.oracle b/tests/spec/oracle/Extend_recursive_preprocess.res.oracle
index ec48b5138f4..0b8592e2baf 100644
--- a/tests/spec/oracle/Extend_recursive_preprocess.res.oracle
+++ b/tests/spec/oracle/Extend_recursive_preprocess.res.oracle
@@ -1,20 +1,29 @@
[kernel] Parsing tests/spec/Extend_recursive_preprocess.i (no preprocessing)
/* Generated by Frama-C */
+/*@ gl_foo foo1_ok {
+ gl_fooo \false;
+ gl_fooo \false;
+ gl_fooo \false;
+ }
+*/
+/*@ gl_foo foo1_ok {
+ gl_foo foo2_ok {
+ gl_fooo \false;
+ }
+ }
+*/
/*@
gl_foo foo1_ok {
- gl_fooo \false;
- gl_foo foo2_ok {
- gl_fooo \false;
- gl_foo foo3_ok {
- gl_fooo \false;
- gl_fooo \false;
- }
- ;
- gl_fooo \false;
- }
- ;
- gl_fooo \false;
- }
- ;
+ gl_fooo \false;
+ gl_foo foo2_ok {
+ gl_fooo \false;
+ gl_foo foo3_ok {
+ gl_fooo \false;
+ gl_fooo \false;
+ }
+ gl_fooo \false;
+ }
+ gl_fooo \false;
+ }
*/
--
GitLab