Skip to content
Snippets Groups Projects
Commit 72e835e7 authored by Virgile Prevosto's avatar Virgile Prevosto Committed by Allan Blanchard
Browse files

[tests] fixes ill-formed test

parent f562009c
No related branches found
No related tags found
No related merge requests found
...@@ -9,7 +9,7 @@ ...@@ -9,7 +9,7 @@
assigns ghost_loctable; 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 // The specification above should be accepted
/*@ /*@
...@@ -18,7 +18,7 @@ void acquire_lock(int m) { ghost_loctable[m]++; } ...@@ -18,7 +18,7 @@ void acquire_lock(int m) { ghost_loctable[m]++; }
ensures !ghost_loctable[m]; ensures !ghost_loctable[m];
assigns ghost_loctable[..]; assigns ghost_loctable[..];
*/ */
void release_lock(int m) { ghost_loctable[m]--; } void release_lock(int m) { /*@ ghost ghost_loctable[m]--; */ }
......
...@@ -5,7 +5,7 @@ ...@@ -5,7 +5,7 @@
/*@ ghost int ghost_loctable[100]; */ /*@ ghost int ghost_loctable[100]; */
void acquire_lock(int m) void acquire_lock(int m)
{ {
(ghost_loctable[m]) ++; /*@ ghost (ghost_loctable[m]) ++; */
return; return;
} }
...@@ -16,7 +16,7 @@ void acquire_lock(int m) ...@@ -16,7 +16,7 @@ void acquire_lock(int m)
*/ */
void release_lock(int m) void release_lock(int m)
{ {
(ghost_loctable[m]) --; /*@ ghost (ghost_loctable[m]) --; */
return; return;
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment