diff options
| author |  rustanleino <unknown> | 2009-08-15 02:20:29 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-08-15 02:20:29 +0000 |
| commit | 3bd44c8d3a6780bbeea6bfedfe09732b83215271 (patch) | |
| tree | 11070457da97da394636256c1e3cff20a9844ebd /Binaries | |
| parent | 97a6519c245053811f8f394ba7c9c9875a094f9d (diff) | |
Incorporated Counterexample Visualizer (CEV) information in the generated Boogie.
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 76 |
1 files changed, 75 insertions, 1 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 7ff940b5..fde82b93 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -176,10 +176,84 @@ type Field alpha; type HeapType = <alpha>[ref,Field alpha]alpha;
function $IsGoodHeap(HeapType) returns (bool);
-var $Heap: HeapType where $IsGoodHeap($Heap);
+var $Heap: HeapType where $IsGoodHeap($Heap) && #cev_var_update(#cev_pc, cev_implicit, #loc.$Heap, $Heap);
+const unique #loc.$Heap: $token;
const unique alloc: Field bool;
function $HeapSucc(HeapType, HeapType) returns (bool);
axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) }
$HeapSucc(h,k) ==> (forall o: ref :: { k[o,alloc] } h[o,alloc] ==> k[o,alloc]));
+
+// ---------------------------------------------------------------
+
+type $token;
+function $file_name_is(id:int, tok:$token) returns(bool);
+
+
+type cf_event;
+type var_locglob;
+
+const unique conditional_moment : cf_event;
+const unique took_then_branch : cf_event;
+const unique took_else_branch : cf_event;
+
+const unique loop_register : cf_event;
+const unique loop_entered : cf_event;
+const unique loop_exited : cf_event;
+
+const unique cev_local : var_locglob;
+const unique cev_global : var_locglob;
+const unique cev_parameter : var_locglob;
+const unique cev_implicit : var_locglob;
+
+
+function #cev_init(n:int) returns(bool);
+
+function #cev_save_position(n:int) returns($token);
+
+function #cev_var_intro<T,U>(n:int, locorglob:var_locglob, name:$token, val:T, typ: U) returns(bool);
+
+function #cev_var_update<T>(n:int, locorglob:var_locglob, name:$token, val:T) returns(bool);
+
+function #cev_control_flow_event(n:int, tag : cf_event) returns(bool);
+
+function #cev_function_call(n:int) returns(bool);
+
+
+
+var #cev_pc: int;
+
+procedure CevVarIntro<T>(pos: $token, locorglob: var_locglob, name: $token, val: T);
+ modifies #cev_pc;
+ ensures #cev_var_intro(old(#cev_pc), locorglob, name, val, 0);
+ ensures #cev_save_position(old(#cev_pc)) == pos;
+ 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);
+
+procedure CevStep(pos: $token);
+ modifies #cev_pc;
+ ensures #cev_save_position(old(#cev_pc)) == pos;
+ ensures #cev_pc == old(#cev_pc) + 1;
+
+// 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_save_position(old(#cev_pc)) == pos;
+ ensures #cev_pc == old(#cev_pc) + 1;
+
+procedure CevEvent(pos: $token, tag: cf_event);
+ modifies #cev_pc;
+ ensures #cev_control_flow_event(old(#cev_pc), tag);
+ ensures #cev_save_position(old(#cev_pc)) == pos;
+ ensures #cev_pc == old(#cev_pc) + 1;
+
+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;
+
+// ---------------------------------------------------------------
|