diff options
| author |  rustanleino <unknown> | 2010-03-19 04:22:48 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-03-19 04:22:48 +0000 |
| commit | 4622c8070d0c9601dbe2fcdd57f68850f1fbda3f (patch) | |
| tree | 25190c5ef23ab440dc9e10a50b6850d790a34197 /Binaries | |
| parent | 525020dacd005014ec4b90e9ce619979d5396232 (diff) | |
Dafny: Ensures that function axioms are not being used while their consistency is being checked.
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 50433b54..253cfd12 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -207,6 +207,13 @@ function DtRank(DatatypeType) returns (int); // ---------------------------------------------------------------
+// used to make sure function axioms are not used while their consistency is being checked
+const $ModuleContextHeight: int;
+const $FunctionContextHeight: int;
+const $InMethodContext: bool;
+
+// ---------------------------------------------------------------
+
type Field alpha;
type HeapType = <alpha>[ref,Field alpha]alpha;
|