diff options
| author |  rustanleino <unknown> | 2010-03-19 04:22:48 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-03-19 04:22:48 +0000 |
| commit | b58961dc4485114212cc6948d0e966bf73087685 (patch) | |
| tree | 7dbd7c217186f5d32b09a7f4f9af8ad5ab71cd7f /Binaries | |
| parent | 946c1329d9cda4ec68abc9b326c6ac7163c63cd8 (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;
|