summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* VCC: Recognize $resultGravatar Michal Moskal2011-11-15
* MergeGravatar qadeer2011-11-15
|\
* | changed inlining code so that candidate preconditions and postconditions are ...Gravatar qadeer2011-11-15
| * Some fixes for race checking contractsGravatar Unknown2011-11-15
| * Modified solution to build on all platforms.Gravatar Unknown2011-11-15
|/
* MergeGravatar qadeer2011-11-14
|\
* | fixed another bug in model parser related to datatype valuesGravatar qadeer2011-11-14
| * For some reason, these didn't get into the last commit.Gravatar Mike Barnett2011-11-14
| * Trying to get the generics translation correct...Gravatar Mike Barnett2011-11-14
|/
* added the option /inlineDepth:n. This option defaults to -1. If the user prov...Gravatar qadeer2011-11-13
* Boogie build succeededGravatar CodeplexBot2011-11-12
* MergeGravatar qadeer2011-11-11
|\
| * moved the addition of selectors and testers to program.ResolveGravatar qadeer2011-11-11
* | Produce unsat cores only when enabled (in stratified inlining)Gravatar Unknown2011-11-11
|/
* Many, many bug fixes related to generics and some other random problems.Gravatar Mike Barnett2011-11-10
* 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
| * | Dafny: allow single-quote as a character in identifiers in the VS2010 modeGravatar Rustan Leino2011-11-09
| * | Dafny: added "multiset" keyword to syntax highlighting in emacs, vim, latex, VSXGravatar 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
| | * Tagging EMIC CC.NET build 2.1.31109.0Gravatar VccBuildServer2011-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
* | Dafny: Cleaned up proof of RevConcat in test caseGravatar 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: in test suite (Rippling.dfy), replaced an inline lemma with a call to ...Gravatar Rustan Leino2011-11-04
* | | | Dafny: added options to make Induction Heuristic apply to array index express...Gravatar Rustan Leino2011-11-04
* | | | MergeGravatar Rustan Leino2011-11-03
|\ \ \ \
* | | | | Added some Dafny and Boogie test cases, including Turing's factorial program,...Gravatar Rustan Leino2011-11-03
| | | * | MergeGravatar qadeer2011-11-01
| | | |\ \ | | |_|/ / | |/| | |
| | | * | deleted unused codeGravatar qadeer2011-11-01
| * | | | Don't wipe out existing attributes when adding {:extern}Gravatar Mike Barnett2011-11-01
| | |/ / | |/| |
| * | | Boogie build succeededGravatar CodeplexBot2011-11-01
|/ / /