summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* Dafny: allow assert/assume expressions in more placesGravatar Rustan Leino2011-11-09
* Dafny: added assert/assume expressionsGravatar Rustan Leino2011-11-09
* MergeGravatar qadeer2011-11-09
|\
* | copied all attributes of the constructor (except for :constructor) to the sel...Gravatar qadeer2011-11-09
| * VCC: remove _vcc_math_type_ from type namesGravatar Michal Moskal2011-11-09
| * VCC: hide #limited# functionsGravatar Michal Moskal2011-11-09
| * MergeGravatar Rustan Leino2011-11-09
| |\
| * | Dafny: moved definition of class.array into prelude, anticipating writing axi...Gravatar Rustan Leino2011-11-09
| | * Refactoring, and work on race checking contractsGravatar Unknown2011-11-09
| |/
| * MergeGravatar Rustan Leino2011-11-09
| |\
| * | Dafny: fixed part of a type-inference issue with datatypes and the < operator...Gravatar Rustan Leino2011-11-09
| | * BVD: don't do the "Duplicate entry exception"; uncomment for debuggingGravatar Michal Moskal2011-11-08
| | * VCC: show output parameters as rootsGravatar Michal Moskal2011-11-08
| |/ |/|
* | moved GPUVerify into its own solutionGravatar qadeer2011-11-08
|/
* MergeGravatar Rustan Leino2011-11-08
|\
* | Dafny: fixed bug in reads checking of array-to-sequence conversionsGravatar Rustan Leino2011-11-08
| * MergeGravatar Unknown2011-11-08
| |\
| * | Additions to GPU Verify for paper submission.Gravatar Unknown2011-11-08
| | * some refactoring suggested by MichalGravatar qadeer2011-11-07
| | * MergeGravatar qadeer2011-11-07
| | |\
| | * \ MergeGravatar qadeer2011-11-07
| | |\ \ | |_|/ / |/| | |
| | * | change in model parsing with datatype valuesGravatar qadeer2011-11-07
* | | | Dafny: added a new /inductionHeuristic optionGravatar Rustan Leino2011-11-04
* | | | Dafny: added options to make Induction Heuristic apply to array index express...Gravatar Rustan Leino2011-11-04
| | * | deleted unused codeGravatar qadeer2011-11-01
| |/ / |/| |
* | | MergeGravatar Rustan Leino2011-10-31
|\ \ \
* | | | Fixed the generation of names for datatype functions to use the API forGravatar Mike Barnett2011-10-31
| * | | MergeGravatar Rustan Leino2011-10-29
| |\ \ \ | |/ / / |/| | |
| * | | Dafny induction:Gravatar Rustan Leino2011-10-29
* | | | Boogie: Updated the error message for old versions of Z3.Gravatar wuestholz2011-10-28
* | | | Boogie: Get rid of {:inline} attributes on axiomsGravatar Michal Moskal2011-10-27
* | | | Boogie: Get rid of {:ignore} feature on axiomsGravatar Michal Moskal2011-10-27
* | | | Boogie: Present a nice error message when Z3 of lesser version than 3.2 is foundGravatar Michal Moskal2011-10-27
* | | | MergeGravatar Michal Moskal2011-10-27
|\ \ \ \
* | | | | Restart prover after out-of-memory error; honour -restartProver optionGravatar Michal Moskal2011-10-27
| * | | | Boogie: removed unreachable or unused codeGravatar Rustan Leino2011-10-27
| * | | | Boogie: internal clean-up, removed BvHandling type, everything now behaves as...Gravatar Rustan Leino2011-10-27
| * | | | Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ...Gravatar Rustan Leino2011-10-27
| * | | | Boogie: Changed default /prover to SMTLIBGravatar Rustan Leino2011-10-27
| | | | * MergeGravatar qadeer2011-10-27
| | | | |\ | | |_|_|/ | |/| | |
| | | | * various refactoringsGravatar qadeer2011-10-27
| | * | | Dafny: allow attributes on function/method declarations to refer to the (in- ...Gravatar Rustan Leino2011-10-26
| |/ / /
| * | | Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" s...Gravatar Rustan Leino2011-10-26
| * | | Dafny: removed support for assigning to an array-range (that is, an assignmen...Gravatar Rustan Leino2011-10-26
| * | | MergeGravatar Rustan Leino2011-10-26
| |\ \ \ | |/ / / |/| | |
| * | | BVD: fixed two basic but damning problems with the Dafny provider, and elided...Gravatar Rustan Leino2011-10-26
* | | | VCC: Detect wrong model filesGravatar Michal Moskal2011-10-26
| |/ / |/| |
| * | Dafny: implemented compilation of parallel statementsGravatar Rustan Leino2011-10-25
* | | VCC: improvements in showing arrays, addresses, and embeddingsGravatar Michal Moskal2011-10-24
| * | Dafny: check subrange restriction in parallel Assign statementGravatar Rustan Leino2011-10-24
|/ /
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 09:27:16 +0000