summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* phone injecting code traverserGravatar Unknown2011-07-08
|
* Dafny: Added Euclidean regression test (Verifier only).Gravatar Jason Koenig2011-07-08
|
* MergeGravatar Jason Koenig2011-07-08
|\
* | Dafny: Dafny now uses the Euclidean definition of division. (Verifier and ↵Gravatar Jason Koenig2011-07-08
| | | | | | | | runtime.)
| * MergeGravatar Mike Barnett2011-07-08
| |\
| * | Fix translation of "is" operator.Gravatar Mike Barnett2011-07-08
| | | | | | | | | | | | | | | Fix generation of type constants to avoid infinite loops for recursive type definitions.
| | * phone stuff optionsGravatar Unknown2011-07-08
| |/ |/|
* | phone control exploration for BCT, not integrated yetGravatar Unknown2011-07-07
|/ | | | should be made into a plugin sometime
* 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.
* - fixed some bugs with applying unification over list elementsGravatar Unknown2011-07-06
| | | | | | - fixed the List.jen example (generic list) - changed SeqConst and SetConst to contain a list/set of "Const" and not "Const option" like before
* MergeGravatar Unknown2011-07-06
|\
* | remove mscorlib stub project...write each as neededGravatar Unknown2011-07-06
| |
| * MergeGravatar Mike Barnett2011-07-06
| |\ | |/ |/|
| * Updated regression output.Gravatar Mike Barnett2011-07-06
| |
* | phone (static) controls extractorGravatar Unknown2011-07-06
| |
* | phone (static) controls extractor.Gravatar Unknown2011-07-06
| |
* | MergeGravatar Jason Koenig2011-07-06
|\ \
* | | Dafny: Fixed bug in call statements where mutability of out parameters was ↵Gravatar Jason Koenig2011-07-06
| | | | | | | | | | | | | | | | | | not checked. Added regression test.
| * | MergeGravatar Unknown2011-07-06
| |\ \ | |/ / |/| |
| * | - implemented some sorts of symbolic evaluation of expressionsGravatar Unknown2011-07-06
| | | | | | | | | | | | | | | | | | - changed that the intermediate dafny files are written into separate files for different method analyses - added README and StartDafny-jen.bat
| | * MergeGravatar Mike Barnett2011-07-06
| | |\ | |_|/ |/| |
| | * Beginning of encoding the subtype relation.Gravatar Mike Barnett2011-07-06
| | |
| | * Updated regression output.Gravatar Mike Barnett2011-07-06
| | |
* | | 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
| | |
| * | - implemented synthesis of some simple constructors with parametersGravatar Unknown2011-07-05
| | | | | | | | | | | | | | | | | | | | | - 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
* | | MergeGravatar Jason Koenig2011-07-05
|\ \ \
* | | | Dafny: Updated regression tests to include chaining disjoint operators.Gravatar Jason Koenig2011-07-05
| | | |
* | | | Dafny: Added chaining of disjoint (!!) using transitive chaining convention.Gravatar Jason Koenig2011-07-05
| | | |
| * | | ExtractLoops calls the same code for eliminating unreachable blocks that ↵Gravatar qadeer2011-07-05
| | | | | | | | | | | | | | | | | | | | | | | | 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.
| * | | Don't send (check-sat) after error limit is reachedGravatar Michal Moskal2011-07-05
| | | |
| * | | MergeGravatar Michal Moskal2011-07-05
| |\ \ \ | |/ / / |/| | |
| | | * MergeGravatar Mike Barnett2011-07-05
| | | |\ | |_|_|/ |/| | |
* | | | 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.
* | | | MergeGravatar mschwerhoff2011-07-05
|\ \ \ \
* | | | | Chalice: Fixed a bug that prevented Chalice from correctly dealing with ↵Gravatar Unknown2011-07-05
| | | | | | | | | | | | | | | | | | | | Boogie options containing white space characters
| * | | | Boogie: New cli option -z3exe:"path-to-z3.exe" allowing specifying path to ↵Gravatar Unknown2011-07-05
|/ / / / | | | | | | | | | | | | the Z3 version to use
* | | | 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.
* | | | MergeGravatar qadeer2011-07-04
|\ \ \ \
* | | | | 1. generating a separate dipatchcontinuation label for each trycatchfinally ↵Gravatar qadeer2011-07-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| | | * | added some doc commentsGravatar Unknown2011-07-03
| | | | |
| | | * | - when analyzing a constructor, repeated "assume <inv>" statement explicitlyGravatar Unknown2011-07-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | since "assume Valid()" doesn't always work - added optional verification step after code has been synthesized
| | | * | - generates "Valid()" for preconditionsGravatar Unknown2011-07-01
| | | | |
| | | * | - removed the "Constructor" discriminator from type Member, and added aGravatar Unknown2011-07-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-09 13:39:49 +0000