Chalice uses in its Boogie encoding a "versioning scheme" for predicates, where intuitively the version changes whenever a "different" copy of a predicate is held (that potentially abstracts over a...
Id #10216 |
Planned Release:
None
|
Last Updated: Sat at 6:35 AM by stefanheule |
Created On: Sat at 6:35 AM by stefanheule
It looks as if the return type of the ternary operator "e0 ? e1 : e2" doesn't get type-checked properly. When e1 and e2 are not booleans, e.g. ints, the clause "requires e0 ? e1 : e2" causes Boogie...
Id #10215 |
Planned Release:
None
|
Last Updated: Jan 12 at 1:18 PM by mschwerhoff |
Created On: Jan 12 at 1:17 PM by mschwerhoff
Why Dafny says `assertion violation' on this code: http://rise4fun.com/Dafny/S02 ? Does the ghost method `theorem' depend on array `a' which isn't its parameter ? I think Dafny has to be able to co...
Id #10213 |
Planned Release:
None
|
Last Updated: Dec 1 2011 at 4:16 PM by kornevgen |
Created On: Dec 1 2011 at 10:49 AM by kornevgen
Dafny seems to have problems with array-to-sequence conversions in combination with old expressions. Attached is an example of a method that does a no-op on an array. Proving the postcondition "a =...
Id #10212 |
Planned Release:
None
|
Last Updated: Nov 29 2011 at 6:13 PM by kornevgen |
Created On: Nov 14 2011 at 10:51 PM by stefanheule
The attached file produces four type-checking errors of Boogie. I don't know the exact cause, but all of the code seems to be relevant for the problem to show up.
Id #10211 |
Planned Release:
None
|
Last Updated: Nov 11 2011 at 9:00 AM by stefanheule |
Created On: Nov 11 2011 at 9:00 AM by stefanheule
Chalice's type checker does not complaint about method return values occurring in preconditions. Calling such a method results in "undeclared identifier" errors reported by Boogie.
Id #10210 |
Planned Release:
None
|
Last Updated: Sep 14 2011 at 1:38 PM by mschwerhoff |
Created On: Sep 14 2011 at 1:38 PM by mschwerhoff
Having permissions under a conditional in the precondition of a function causes Chalice to output invalid Boogie output (the typechecker complains). Attached is an illustrative example.
Id #10209 |
Planned Release:
None
|
Last Updated: Aug 10 2011 at 11:18 AM by stefanheule |
Created On: Aug 10 2011 at 11:18 AM by stefanheule
The treatment of predicates in Chalice is not sound at the moment: If a predicate p is given away and later returned (e.g., via a method call), the knowledge about the state abstracted over by the ...
Id #10208 |
Planned Release:
None
|
Last Updated: Aug 10 2011 at 9:28 AM by stefanheule |
Created On: Aug 10 2011 at 9:28 AM by stefanheule
The test case AssociationList.chalice (in directory Chalice/tests/examples) seems to be completely broken. The failing assertion about locking/unlocking too much causes an inconsistency and all fol...
Id #10207 |
Planned Release:
None
|
Last Updated: Aug 4 2011 at 3:13 PM by stefanheule |
Created On: Aug 4 2011 at 3:13 PM by stefanheule
See attached file, which crashes with a null reference exception.
Id #10206 |
Planned Release:
None
|
Last Updated: Aug 16 2011 at 11:53 PM by MichalMoskal |
Created On: Jul 29 2011 at 8:38 AM by stobies
|
|
|
|
|