summaryrefslogtreecommitdiff
path: root/Chalice
Commit message (Collapse)AuthorAge
* Chalice: Added missing reference output for AVLTree examplesGravatar mschwerhoff2011-09-27
|
* Adapted batch file to use larger JVM stack size.Gravatar peter mueller peter.mueller@inf.ethz.ch2011-09-19
|
* Chalice: Modified chalice.bat s.t. it checks if all Java classpath elements ↵Gravatar mschwerhoff2011-09-19
| | | | exist
* Chalice: Modified chalice.bat s.t. it uses the Scala libraries downloaded ↵Gravatar mschwerhoff2011-09-16
| | | | but Sbt. This releaves the user from having to ensure that he/she has the same Scala version in the path as used by Sbt to build Chalice.
* Chalice: Modified sbt.bat s.t. JAVA_OPTS are forwarded to the JVM.Gravatar mschwerhoff2011-09-15
|
* Added Uri Juhasz' AVL-treesGravatar Unknown2011-09-08
|
* Chalice: Added a script gathering all files necessary and/or of interest for ↵Gravatar mschwerhoff2011-08-18
| | | | a Chalice release.
* Chalice: Changed tests/runalltests.bat such that additional parameters can ↵Gravatar mschwerhoff2011-08-15
| | | | be passed to Chalice
* Chalice: Disallow credit expressions in the specification of functions.Gravatar stefanheule2011-08-12
|
* Chalice: Add comment to a broken test-case.Gravatar stefanheule2011-08-04
|
* Chalie: Fix Visual Studio integration and add note about JVM stack size ↵Gravatar stefanheule2011-08-04
| | | | problems.
* Chalice: Add regression tests for all fixed bugs and separate the tests in ↵Gravatar stefanheule2011-08-03
| | | | 'examples' into "read" examples and general tests.
* Chalice: only show warning about misleading smoke warnings if there are ↵Gravatar stefanheule2011-08-03
| | | | actually smoke warnings.
* Chalice: Improve command line interface. Unknown options are no longer ↵Gravatar stefanheule2011-08-03
| | | | 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.
* Chalice: Add sbt to the repository.Gravatar stefanheule2011-08-02
|
* Chalice: Chalice is now built using sbt (simple built tool).Gravatar stefanheule2011-08-02
|
* Chalice: added string type and string literals (but no other string operations)Gravatar Rustan Leino2011-07-26
|
* Chalice: Check definedness of where-clause of channels (was missing before), ↵Gravatar stefanheule2011-07-22
| | | | 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).
* Chalice: Improve smoke testing: look for preconditions of functions, ↵Gravatar stefanheule2011-07-22
| | | | predicates and monitor invariants that are equivalent to false, and add a command line option "/smokeAll" to insert 'assert false' after *every* Chalice statement.
* Chalice: Only show the "first" smoke warning, as once the prover is able to ↵Gravatar stefanheule2011-07-21
| | | | | | | 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.
* Chalice: Use "/smoke" for the test suite by default to ensure test quality. ↵Gravatar stefanheule2011-07-20
| | | | Update all reference outputs accordingly.
* Chalice: improve smoke testing to use the subsumption option only for the ↵Gravatar stefanheule2011-07-20
| | | | "assert false" statements.
* Chalice: Improve command line help and allow both "-param" (old) and ↵Gravatar stefanheule2011-07-20
| | | | "/param" (new), similar to Boogie.
* Chalice: Uniform usage of Boogie syntax for functions.Gravatar stefanheule2011-07-20
|
* Chalice: Fix all three copyless message passing programs. There were ↵Gravatar stefanheule2011-07-19
| | | | 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).
* Chalice: Fix two nasty bugs that could lead to contradictions in the Boogie ↵Gravatar stefanheule2011-07-19
| | | | encoding for certain programs. See workitems 10203 and 10204.
* Chalice: Fix batch file problem and update reference output.Gravatar stefanheule2011-07-19
|
* Chalice: Smoke testing to find unreachable code, preconditions that are ↵Gravatar stefanheule2011-07-18
| | | | equivalent to false and assumptions that introduce contradictions. Can be used with the command line switch "-smoke".
* Chalice: Also exhale correctly in two steps for multiple contracts (e.g. two ↵Gravatar stefanheule2011-07-18
| | | | preconditions), and include missing well-formedness assumption afer async method calls.
* Chalice: Fix a problem with permission expressions. Prevsiously, exhaling ↵Gravatar stefanheule2011-07-18
| | | | "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.
* MergeGravatar Unknown2011-07-16
|\
* | Suppress generation of Drop(s, 0). This expression caused unnecessary ↵Gravatar Unknown2011-07-16
| | | | | | | | verification problems, even though the axioms should be sufficient to handle this case (and also trigger).
| * Chalice: Fix workitem 10191 (escaping method arguments).Gravatar stefanheule2011-07-07
| |
| * Chalice: New test script to execute all tests (in all folder) at once. Test ↵Gravatar stefanheule2011-07-07
| | | | | | | | scripts now set the errorlevel to the number of failed tests.
| * Chalice: Error message of the valid-permission-check often included ↵Gravatar stefanheule2011-07-07
| | | | | | | | '<undefined position>'. Reference output of one affected test updated.
| * Chalice: Allow _ as wildcard in the eval construct for parameters. Usage is ↵Gravatar stefanheule2011-07-07
|/ | | | demonstrated in a new test case.
* Chalice: fix workitem 10194 (unfolding and old-expressions).Gravatar stefanheule2011-07-06
|
* Chalice: fix workitem 10199 (partial unfolding of nested predicates).Gravatar stefanheule2011-07-06
|
* Chalice: fix workitem 8236 (lockchange on return values causes invalid ↵Gravatar stefanheule2011-07-05
| | | | Boogie code).
* MergeGravatar mschwerhoff2011-07-05
|\
* | Chalice: Removed debug codeGravatar mschwerhoff2011-07-05
| |
| * Chalice: Four new interesting Chalice examples (added to test suite with the ↵Gravatar stefanheule2011-07-05
|/ | | | correct reference output). The example FictionallyDisjointCells.chalice is due to Yannis Kassios. Small fix to test script.
* Chalice: Fixed a bug that prevented Chalice from correctly dealing with ↵Gravatar Unknown2011-07-05
| | | | Boogie options containing white space characters
* Chalice: Completely switch to new testing scripts (more flexible and ↵Gravatar stefanheule2011-07-05
| | | | fine-grained testing) and remove old test.bat. New testing scripts are described in Chalice/tests/readme.txt.
* Chalice: New permission model that provides more abstraction and more ↵Gravatar stefanheule2011-07-01
| | | | | | | | | | | | | | | | | | | | | | | 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
* Fix some deprecation warnings from scalac 2.8.0.Gravatar kyessenov2011-02-16
| | | | | Check for Boogie.exe only on Windows. Fix parser (_ is a keyword, not a delimiter)
* Chalice: Applied patch 7685, this fixes a small bug that duplicated members ↵Gravatar alexanderjsummers2011-01-12
| | | | are not detected (neither duplicated methods, nor fields).
* Applied patch 7636 - this fixes workitem 9978Gravatar alexanderjsummers2011-01-12
|
* Chalice: this fixes a bug (an unsoundness) that arose in when a program ↵Gravatar mueller2010-12-16
| | | | combined predicates, read permissions to predicates, and forks.
* Small changes to compile and test Chalice on Linux.Gravatar kyessenov2010-12-04
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-03 12:17:48 +0000