summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* MergeGravatar Rustan Leino2011-08-18
|\
* | Dafny: fixed bug in looking at the arguments of the :induction attributeGravatar Rustan Leino2011-08-18
| * minor refactoringGravatar qadeer2011-08-17
| * deleted lazyinlining option 2 and 3Gravatar qadeer2011-08-17
| * MergeGravatar Michal Moskal2011-08-16
| |\
| | * Dafny: Fixed a bug in the printer that led to a stack overflow.Gravatar wuestholz2011-08-11
| | * Added "procedure-copy bounding" for lazy inliningGravatar Unknown2011-08-10
| | * further updates to bit vector analysisGravatar qadeer2011-08-09
| | * more changes to bitvector analysisGravatar qadeer2011-08-09
| | * another bug fix in bctGravatar qadeer2011-08-08
| | * added a new file and fixed a bug in bctGravatar qadeer2011-08-08
| | * various changes to boogie for bitvector analysis and bctproviderGravatar qadeer2011-08-08
| * | Fix null-refGravatar Michal Moskal2011-08-07
| | * further updates to bctproviderGravatar qadeer2011-08-05
| | * first addGravatar qadeer2011-08-05
| | * fixed the key signing problem with houdiniGravatar qadeer2011-08-05
| | * further changes for making houdini workGravatar qadeer2011-08-04
| | * MergeGravatar qadeer2011-08-04
| | |\ | |_|/ |/| |
| | * cleaned up houdini optionsGravatar qadeer2011-08-04
* | | MergeGravatar Rustan Leino2011-08-04
|\ \ \ | | |/ | |/|
| * | full port of houdini projectGravatar qadeer2011-08-04
| * | MergeGravatar qadeer2011-08-03
| |\|
| * | ported Houdini to C#, added Houdini project to the Boogie solutionGravatar qadeer2011-08-03
| |/
* / Dafny: fix resolution crash (using multi-dimensional arrays in loop alternative)Gravatar Rustan Leino2011-08-03
|/
* release build should not have z3api being builtGravatar Unknown2011-07-28
* Dafny: re-ran parser generator to include semicolon-less body-less functions/...Gravatar Rustan Leino2011-07-26
* MergeGravatar Jason Koenig2011-07-15
|\
* | Added compilation support for multisets and sequences from arrays.Gravatar Jason Koenig2011-07-15
| * Updated the Parser.cs and Scanner.cs files in Boogie and Dafny and removed so...Gravatar wuestholz2011-07-15
* | MergeGravatar Jason Koenig2011-07-14
|\|
* | Fixed bug where wellformedness for E in multiset(E) was checked in the "old" ...Gravatar Jason Koenig2011-07-14
* | Added multiset from sequence axioms, removed array range RHSs. Fixed issue wi...Gravatar Jason Koenig2011-07-13
| * Another test checkinGravatar Michal Moskal2011-07-12
* | Fixed printing of multisets.Gravatar Jason Koenig2011-07-11
* | Multiset forming operators added.Gravatar Jason Koenig2011-07-11
| * MergeGravatar Rustan Leino2011-07-11
| |\
| * | Dafny: allow constructors only inside classes, removed semi-colons at end of ...Gravatar Rustan Leino2011-07-11
* | | MergeGravatar Jason Koenig2011-07-11
|\ \ \
* \ \ \ MergeGravatar Jason Koenig2011-07-11
|\ \ \ \
* | | | | Added s[..] syntax in anticipation of sequence forming operation. (also updat...Gravatar Jason Koenig2011-07-11
| | | | * - fixed a bug in DafnyModelUtils.fs (reading set values from models)Gravatar Unknown2011-07-11
| | |_|/ | |/| |
| | * | Partial implementation of multisets.Gravatar Jason Koenig2011-07-11
| |/ / |/| |
| * | async call return value is either int or bv32Gravatar qadeer2011-07-09
| * | MergeGravatar qadeer2011-07-09
| |\ \ | |/ / |/| |
| * | fixed bug in vcgen for bitvectorsGravatar qadeer2011-07-09
| |/
* / Dafny: Dafny now uses the Euclidean definition of division. (Verifier and run...Gravatar Jason Koenig2011-07-08
|/
* Dafny: Fixed bug in call statements where mutability of out parameters was no...Gravatar Jason Koenig2011-07-06
* MergeGravatar 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