From 11d95eabf8d0bf02059162f63c1ab0adba8a2ef8 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Fri, 18 Jan 2019 16:27:56 +0100
Subject: [PATCH] [tests] '//@ for bhv-list: extended-annotation;'
---
tests/spec/Extend.i | 4 ++--
tests/spec/oracle/Extend.res.oracle | 4 +++-
2 files changed, 5 insertions(+), 3 deletions(-)
diff --git a/tests/spec/Extend.i b/tests/spec/Extend.i
index f69d26eaa2c..dd42b218070 100644
--- a/tests/spec/Extend.i
+++ b/tests/spec/Extend.i
@@ -43,9 +43,9 @@ int k(int z) {
/*@ global_foo \forall integer x; x < x + 1
; */
-
+//@ behavior ca_foo: ensures ca_foo: \true;
void loop (void) {
- //@ ca_foo \true;
+ //@ for ca_foo: ca_foo \true;
//@ ns_foo \true;
//@ baz \true;
/*@ loop invariant \true; */
diff --git a/tests/spec/oracle/Extend.res.oracle b/tests/spec/oracle/Extend.res.oracle
index da72437c2ec..6fb85da86ba 100644
--- a/tests/spec/oracle/Extend.res.oracle
+++ b/tests/spec/oracle/Extend.res.oracle
@@ -48,9 +48,11 @@ int k(int z)
/*@ global_foo ∀ ℤ x; x < x + 1;
*/
+/*@ behavior ca_foo:
+ ensures ca_foo: \true; */
void loop(void)
{
- /*@ ca_foo \true; */ ;
+ /*@ for ca_foo: ca_foo \true; */ ;
/*@ ns_foo \true; */
/*@ baz \true; */
/*@ loop invariant \true; */
--
GitLab