diff options
| author |  stefanheule <unknown> | 2011-07-01 11:40:18 +0200 |
|---|---|---|
| committer | stefanheule <unknown> | 2011-07-01 11:40:18 +0200 |
| commit | 29997a5dd73bfe92292caf1c26fea6b04082a7c9 (patch) | |
| tree | 075d85b62fe670d744384aabfc83b01199d36ca0 /Chalice/tests/examples/CopyLessMessagePassing.output.txt | |
| parent | 9dfd07f5afe943abf40eaa7a9351ea92748b59ab (diff) | |
Chalice: New permission model that provides more abstraction and more 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
Diffstat (limited to 'Chalice/tests/examples/CopyLessMessagePassing.output.txt')
| -rw-r--r-- | Chalice/tests/examples/CopyLessMessagePassing.output.txt | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Chalice/tests/examples/CopyLessMessagePassing.output.txt b/Chalice/tests/examples/CopyLessMessagePassing.output.txt new file mode 100644 index 00000000..d6fd8be3 --- /dev/null +++ b/Chalice/tests/examples/CopyLessMessagePassing.output.txt @@ -0,0 +1,4 @@ +Verification of CopyLessMessagePassing.chalice
+
+
+Boogie program verifier finished with 11 verified, 0 errors
|