| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| |
|
|
| |
parts of that test case (they are now reported as workitem 10221). Also, the assertion is now written as a postcondition.
|
| |
|
|
| |
unfold/fold pairs which currently confuse the encoding.
|
| |\ |
|
| | |
| |
| |
| | |
absolute path as %0 instead of just the scripts name)
|
| | | |
|
| | |
| |
| |
| | |
changeset 30e940802059deb4d1e600c3c1fbcda5e39128eb).
|
| | |
| |
| |
| | |
failing test now verifies; i.e. Chalice is less incomplete).
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |\
| |/
|/| |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
last commit).
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |/
|
|
| |
be passed to Chalice
|
| | |
|
| |
|
|
| |
'examples' into "read" examples and general tests.
|
| |
|
|
| |
actually smoke warnings.
|
| |
|
|
| |
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.
|
| |
|
|
| |
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).
|
| | |
|
| |
|
|
| |
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.
|
| |
|
|
| |
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.
|
| |
|
|
| |
correct reference output). The example FictionallyDisjointCells.chalice is due to Yannis Kassios. Small fix to test script.
|
| |
|
|
| |
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
|
stefanheule
Unknown
Christian Klauser
Kuat Yessenov
Unknown