diff options
| author |  Rustan Leino <unknown> | 2014-02-13 15:32:48 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-13 15:32:48 -0800 |
| commit | be556deb1f82b9e16b7337422d80a2546559648e (patch) | |
| tree | ab73a1eb0f309587d23be3812e34c0acf0ce8e7a /Binaries/DafnyPrelude.bpl | |
| parent | 32f7e8341013b32c3cdc3548b2d6826a9013f7d1 (diff) | |
Fix soundness bug (Issue #9 on dafny.codeplex.com) in function axiom for literals.
Added axiom to better handle DtAlloc/GenericAlloc correspondence (which improves handling of computations).
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 1069f419..d4c97f0f 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -646,6 +646,9 @@ axiom (forall b: BoxType, h: HeapType, t: BoxType :: axiom (forall b: BoxType, h: HeapType ::
{ GenericAlloc(b, h), DtAlloc($Unbox(b): DatatypeType, h) }
GenericAlloc(b, h) <==> DtAlloc($Unbox(b): DatatypeType, h));
+axiom (forall dt: DatatypeType, h: HeapType ::
+ { GenericAlloc($Box(dt), h) }
+ GenericAlloc($Box(dt), h) <==> DtAlloc(dt, h));
// ==> GenericAlloc
axiom (forall b: bool, h: HeapType ::
$IsGoodHeap(h) ==> GenericAlloc($Box(b), h));
|