From 72e835e7dde9c2abdfdd0749187ebb30685a991f Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 11 Oct 2019 12:10:45 +0200
Subject: [PATCH] [tests] fixes ill-formed test
---
tests/spec/assigns_array.c | 4 ++--
tests/spec/oracle/assigns_array.res.oracle | 4 ++--
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/tests/spec/assigns_array.c b/tests/spec/assigns_array.c
index ae1e717e53b..c044389fd8a 100644
--- a/tests/spec/assigns_array.c
+++ b/tests/spec/assigns_array.c
@@ -9,7 +9,7 @@
assigns ghost_loctable;
*/
-void acquire_lock(int m) { ghost_loctable[m]++; }
+void acquire_lock(int m) { /*@ ghost ghost_loctable[m]++; */ }
// The specification above should be accepted
/*@
@@ -18,7 +18,7 @@ void acquire_lock(int m) { ghost_loctable[m]++; }
ensures !ghost_loctable[m];
assigns ghost_loctable[..];
*/
-void release_lock(int m) { ghost_loctable[m]--; }
+void release_lock(int m) { /*@ ghost ghost_loctable[m]--; */ }
diff --git a/tests/spec/oracle/assigns_array.res.oracle b/tests/spec/oracle/assigns_array.res.oracle
index 4a571e41bf1..6e4846e218d 100644
--- a/tests/spec/oracle/assigns_array.res.oracle
+++ b/tests/spec/oracle/assigns_array.res.oracle
@@ -5,7 +5,7 @@
/*@ ghost int ghost_loctable[100]; */
void acquire_lock(int m)
{
- (ghost_loctable[m]) ++;
+ /*@ ghost (ghost_loctable[m]) ++; */
return;
}
@@ -16,7 +16,7 @@ void acquire_lock(int m)
*/
void release_lock(int m)
{
- (ghost_loctable[m]) --;
+ /*@ ghost (ghost_loctable[m]) --; */
return;
}
--
GitLab