summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Chalice: New test script to execute all tests (in all folder) at once. Test s...Gravatar stefanheule2011-07-07
* Chalice: Error message of the valid-permission-check often included '<undefin...Gravatar stefanheule2011-07-07
* Chalice: Allow _ as wildcard in the eval construct for parameters. Usage is d...Gravatar stefanheule2011-07-07
* - fixed some bugs with applying unification over list elementsGravatar Unknown2011-07-06
* 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 no...Gravatar Jason Koenig2011-07-06
| * | MergeGravatar Unknown2011-07-06
| |\ \ | |/ / |/| |
| * | - implemented some sorts of symbolic evaluation of expressionsGravatar Unknown2011-07-06
| | * 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
* | | 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 norm...Gravatar qadeer2011-07-05
| * | | 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 Boogie...Gravatar stefanheule2011-07-05
* | | | 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
|/ / / /
* | | | MergeGravatar mschwerhoff2011-07-05
|\ \ \ \
* | | | | Chalice: Fixed a bug that prevented Chalice from correctly dealing with Boogi...Gravatar Unknown2011-07-05
| * | | | Boogie: New cli option -z3exe:"path-to-z3.exe" allowing specifying path to th...Gravatar Unknown2011-07-05
|/ / / /
* | | | Chalice: Completely switch to new testing scripts (more flexible and fine-gra...Gravatar stefanheule2011-07-05
* | | | MergeGravatar qadeer2011-07-04
|\ \ \ \
* | | | | 1. generating a separate dipatchcontinuation label for each trycatchfinally ...Gravatar qadeer2011-07-04
| | | * | added some doc commentsGravatar Unknown2011-07-03
| | | * | - when analyzing a constructor, repeated "assume <inv>" statement explicitlyGravatar Unknown2011-07-02
| | | * | - generates "Valid()" for preconditionsGravatar Unknown2011-07-01
| | | * | - removed the "Constructor" discriminator from type Member, and added aGravatar Unknown2011-07-01
| * | | | MergeGravatar Jason Koenig2011-07-01
| |\ \ \ \ | |/ / / / |/| | | |
| * | | | Added the /noCheating option. (treats assume as assert and drops free.)Gravatar Jason Koenig2011-07-01
| | | | * MergeGravatar Mike Barnett2011-07-01
| | | | |\ | |_|_|_|/ |/| | | |
* | | | | Chalice: New permission model that provides more abstraction and more flexibi...Gravatar stefanheule2011-07-01
* | | | | bug fix in heap access for splitfield optionGravatar qadeer2011-06-30
|/ / / /
| * | | Update the RECENT_Z3 #define to include SORT_AND_ORGravatar Michal Moskal2011-06-30
| * | | Let = in options be passed down to the runtest.batGravatar Michal Moskal2011-06-30
| * | | Add /T: option to Z3 to kill it if it exceeds soft timeout by more than 1sGravatar Michal Moskal2011-06-30
| * | | Allow : instead of = in optionsGravatar Michal Moskal2011-06-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 14:59:54 +0000