| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
'examples' into "read" examples and general tests.
|
| |
|
|
| |
actually smoke warnings.
|
| |
|
|
| |
silently passed to Boogie (but passing them to Boogie is still possible with /boogieOpt), and Chalice shows a message when it expects input from stdin.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
and smoke test for 'false' where clauses. Due to the missing definedness check, a mistake in the specification of CopyLessMessagePassing-with-ack2.chalice was not detected (and has been fixed now).
|
| |
|
|
| |
predicates and monitor invariants that are equivalent to false, and add a command line option "/smokeAll" to insert 'assert false' after *every* Chalice statement.
|
| |
|
|
|
|
|
| |
show false, all follwoing attempts will always succeed. However, smoke warnings on different paths through a method are still all reported.
Also, the places where to insert "assert false" are chosen more carefully (essentially always all statements that inhale something).
Update test reference outputs accordingly.
|
| |
|
|
| |
Update all reference outputs accordingly.
|
| |
|
|
| |
"assert false" statements.
|
| |
|
|
| |
"/param" (new), similar to Boogie.
|
| | |
|
| |
|
|
| |
problems in the specification (all three programs) and the program itself ("..with-ack2"). Furthermore, if only two types of messages can be sent, a boolean flag is now used instead of an integer (to simplify the specifications).
|
| |
|
|
| |
encoding for certain programs. See workitems 10203 and 10204.
|
| | |
|
| |
|
|
| |
equivalent to false and assumptions that introduce contradictions. Can be used with the command line switch "-smoke".
|
| |
|
|
| |
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
|
| | |
|
| | |
|
| | |
|
| | |
|
stefanheule
Rustan Leino
Unknown
Unknown