| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
preconditions), and include missing well-formedness assumption afer async method calls.
|
| |
|
|
| |
"acc(o.f,100-rd) && acc(o.f,rd)" resulted in a contradiction. This is now solved by using a two-step exhale (loosely speaking, read permissions and functional properties are exhaled first, and only afterwards all other permissions). Extended testcases appropriately.
|
| |\ |
|
| | |
| |
| |
| | |
verification problems, even though the axioms should be sufficient to handle this case (and also trigger).
|
| | | |
|
| | |
| |
| |
| | |
scripts now set the errorlevel to the number of failed tests.
|
| | |
| |
| |
| | |
'<undefined position>'. Reference output of one affected test updated.
|
| |/
|
|
| |
demonstrated in a new test case.
|
| | |
|
| | |
|
| |
|
|
| |
Boogie code).
|
| |\ |
|
| | | |
|
| |/
|
|
| |
correct reference output). The example FictionallyDisjointCells.chalice is due to Yannis Kassios. Small fix to test script.
|
| |
|
|
| |
Boogie options containing white space characters
|
| |
|
|
| |
fine-grained testing) and remove old test.bat. New testing scripts are described in Chalice/tests/readme.txt.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
flexibility. Details of the model can be found in the paper 'Fractional Permissions without the Fractions', FTfJP 2011 (see http://www.pm.inf.ethz.ch/publications/).
This changeset also fixes several bugs not directly related to the permissions model and improves the error handling. The following features have been added or enhanced:
- Error handling: If exceptions (e.g. about not supported features) are encountered, a user-friendly message is displayed
- Sequence axioms: There is an additional axiom for singleton lists, which is helpful in some cases
- Prelude: Chalice's prelude has been split into sections (e.g. one for permission-related stuff, one for sequence axioms, and so on), which are included on demand (less superfluous axioms, etc.)
Currently not working - but planned to be updated as well - are the following features:
- Stepwise refinements
- autoFold
- read locks
There is a performance issue with permission scaling (i.e., taking non-full versions of predicates that contain read-permissions). Details can be found in the following file: Chalice/tests/permission-model/scaling.chalice.
A list of fixed bugs (see http://boogie.codeplex.com/workitem/<workitem number> for details on the individual bugs)
- workitem 10200: Issue with the axiom of framing functions
- workitem 10197: The translation of old(waitlevel) resultet in Boogie error
- workitem 10196: Quantification over empty sequences
- workitem 10195: Contradiction when descending sequences are used
- workitem 10192: Invalid translation of old-construct in certain cases
- workitem 10190: Stack overflow when parsing large comment blocks
- workitem 10147: Duplicated method parameters and return values are not detected
|
| |
|
|
|
| |
Check for Boogie.exe only on Windows.
Fix parser (_ is a keyword, not a delimiter)
|
| |
|
|
| |
are not detected (neither duplicated methods, nor fields).
|
| | |
|
| |
|
|
| |
combined predicates, read permissions to predicates, and forks.
|
| | |
|
| |
|
|
| |
Dafny: Simplified VSComp2010/Problem4-Queens.dfy from using an inductive ghost-method lemmas to just using an assert
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
* Also copy CodeContractExtender in PrepareBoogieZip.bat
* Added some comments and a new program in Test/textbook
* Included refinement keywords in Chalice emacs mode
* Used assignment instead of spec statement in DuplicatesVideo.chalice
|
| |
|
|
| |
warnings, though. If 2.8.0 terminates with a stack overflow, increase stack size of the JVM (-Xss16M)
|
| | |
|
| |
|
|
|
| |
* extended the cheap type inference to also consider "in" expressions and quantifiers
* added some refinement keywords to the Emacs mode for Chalice
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
synonym to "var"
|
| |
|
|
| |
next goal is to make this verify!
|
| |
|
|
|
| |
* fix bugs -- translateAssert and etran.fromPreGlobals were referring to globals by name instead of using current globals
* example of finding duplicate elements in a sequence using a bitset
|
| |
|
|
| |
translation; tag global coupling assertions (bug fix)
|
| |
|
|
| |
"this"
|
| |
|
|
|
|
| |
* added celebrity example (theory of sequences is still weak to prove basic things...)
* bug in Chalice: old in while loops is ignored, needs to be fixed if ever want to complete DSW example
* evil input from Z3 makes subsequent refinement proofs unsound; need to debug before building upon DSW.chalice; the error is triggered when adding parent field to Node
|
| |
|
|
| |
evil input again...
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
* coupling invariants work (with certain restrictions as described in TODO comments)
|
| |
|
|
|
| |
* fix a compilation problem (scalac relied on old binaries)
* combinator parser and state don't work well together -- added higher-order parser for method transform
|
| | |
|
| | |
|
| |
|
|
| |
positions were negative
|
| | |
|
| | |
|
stefanheule
Unknown
Unknown