| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
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.
|
| |
|
|
|
|
| |
- fixed the List.jen example (generic list)
- changed SeqConst and SetConst to contain a list/set of "Const"
and not "Const option" like before
|
| |\ |
|
| | | |
|
| | |\
| |/
|/| |
|
| | | |
|
| | | |
|
| | | |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
not checked.
Added regression test.
|
| | |\ \
| |/ /
|/| | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
- changed that the intermediate dafny files are written into separate
files for different method analyses
- added README and StartDafny-jen.bat
|
| | | |\
| |_|/
|/| | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
- added some desugaring to help the verifier. Expression like
lst = [p] + [q r]
are desugared into
lst = [p] + [q r] && lst[0] = p && lst[1] = q && lst[2] = r
|
| |\ \ \ |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
normal VCgen calls. Deleted a procedure that was not being used as a result.
Added an extra assume(false) at the end of each DispatchContinuation to help boogie vcgen.
|
| | | | | |
|
| | |\ \ \
| |/ / /
|/| | | |
|
| | | | |\
| |_|_|/
|/| | | |
|
| | | | |
| | | |
| | | |
| | | | |
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
|
| |/ / / /
| | | |
| | | |
| | | | |
the Z3 version to use
|
| | | | |
| | | |
| | | |
| | | | |
fine-grained testing) and remove old test.bat. New testing scripts are described in Chalice/tests/readme.txt.
|
| |\ \ \ \ |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
statement; this should help in reducing the "loopiness" of the generated code.
2. added overrides for loop statements and continue statement; they just throw exception right now
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
since "assume Valid()" doesn't always work
- added optional verification step after code has been synthesized
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
boolean flag to the "Method" discriminator instead
- added a new example called "List3.jen". The difference between List2 is
that the IntNode class has a "succ" field that returns a list of all
successor nodes, instead of list of integers as in List2. In this example,
the invariant is very verbose because of the lack of better syntax, so
maybe we can add some syntactic sugar to Jennisys (e.g. for transitive
closure, comprehensions, etc.) and synthesize Dafny code from that.
- reading from BVD models now also reads Seq#Append, because some lists are
created only that way
|
| | |\ \ \ \
| |/ / / /
|/| | | | |
|
| | | | | | |
|
| | | | | |\
| |_|_|_|/
|/| | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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
Unknown
Mike Barnett
qadeer
Michal Moskal
Unknown