From 00dbdfbb3cd610873676050dafbb4e9bcf9d4672 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Wed, 19 Aug 2009 19:59:06 +0000
Subject: Full (?) support in Dafny for Counterexample Visualizer predicates.

---
 Binaries/DafnyPrelude.bpl | 23 ++++++++++++++++++-----
 1 file changed, 18 insertions(+), 5 deletions(-)

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index fde82b93..fa0d1529 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -231,7 +231,7 @@ procedure CevVarIntro<T>(pos: $token, locorglob: var_locglob, name: $token, val:
   ensures #cev_pc == old(#cev_pc) + 1;
 
 procedure CevUpdateHere<T>(name: $token, val: T);
-  ensures #cev_var_update(#cev_pc, cev_global/*BOGUS*/, name, val);
+  ensures #cev_var_update(#cev_pc, cev_local, name, val);
 
 procedure CevStep(pos: $token);
   modifies #cev_pc;
@@ -241,7 +241,13 @@ procedure CevStep(pos: $token);
 // CevUpdate == CevUpdateHere + CevStep
 procedure CevUpdate<T>(pos: $token, name: $token, val: T);
   modifies #cev_pc;
-  ensures #cev_var_update(old(#cev_pc), cev_global/*BOGUS*/, name, val);
+  ensures #cev_var_update(old(#cev_pc), cev_local, name, val);
+  ensures #cev_save_position(old(#cev_pc)) == pos;
+  ensures #cev_pc == old(#cev_pc) + 1;
+
+procedure CevUpdateHeap(pos: $token, name: $token, val: HeapType);
+  modifies #cev_pc;
+  ensures #cev_var_update(old(#cev_pc), cev_implicit, name, val);
   ensures #cev_save_position(old(#cev_pc)) == pos;
   ensures #cev_pc == old(#cev_pc) + 1;
 
@@ -251,9 +257,16 @@ procedure CevEvent(pos: $token, tag: cf_event);
   ensures #cev_save_position(old(#cev_pc)) == pos;
   ensures #cev_pc == old(#cev_pc) + 1;
 
+procedure CevStepEvent(pos: $token, tag: cf_event);
+  modifies #cev_pc;
+  ensures #cev_control_flow_event(old(#cev_pc)+1, tag);
+  ensures #cev_save_position(old(#cev_pc)+1) == pos;
+  ensures #cev_pc == old(#cev_pc) + 2;
+
 procedure CevPreLoop(pos: $token) returns (oldPC: int);
-  ensures #cev_control_flow_event(#cev_pc, loop_register);
-  ensures #cev_save_position(#cev_pc) == pos;
-  ensures oldPC == #cev_pc;
+  modifies #cev_pc;
+  ensures #cev_control_flow_event(old(#cev_pc), conditional_moment);
+  ensures #cev_save_position(old(#cev_pc)) == pos;
+  ensures oldPC == old(#cev_pc) && #cev_pc == old(#cev_pc) + 1;
 
 // ---------------------------------------------------------------
-- 
cgit v1.2.3