summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* 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
* 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
|/
* Dafny: continued translation of "parallel" statements (Assign and Proof forms...Gravatar Rustan Leino2011-10-24
* Dafny: added translation of Assign case of the parallel statementGravatar Rustan Leino2011-10-22
* MergeGravatar Rustan Leino2011-10-21
|\
* | Dafny: changed triggers (which are never really used, anyhow) from having a s...Gravatar Rustan Leino2011-10-21
| * Sync timeout messages with Z3 prover interfaceGravatar Michal Moskal2011-10-21
| * Don't pass /T: option to Z3 - it kills Z3 prematurely when there are multiple...Gravatar Michal Moskal2011-10-21
| * Improve logging when -proverOpt:VERBOSITY=1 or 2 is specifiedGravatar Michal Moskal2011-10-21
| * MergeGravatar Michal Moskal2011-10-19
| |\ | |/ |/|
| * VCC: support some more _(blob ...) buisnessGravatar Michal Moskal2011-10-19
* | MergeGravatar Rustan Leino2011-10-19
|\ \
* | | Dafny: fixed performance-buggy translation of exists, and also added some oth...Gravatar Rustan Leino2011-10-19
| | * BVD: Default to expert view; Only VCC uses that stuff now, and all VCC users ...Gravatar Michal Moskal2011-10-19
| |/
| * Performance improvements in BVDGravatar Michal Moskal2011-10-19
|/
* VCC: Fix problem with booleans being displayed as mapsGravatar Michal Moskal2011-10-19
* Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only)Gravatar Unknown2011-10-19
* added houdini to regressionGravatar qadeer2011-10-17
* revised implementation of proc copy boundingGravatar qadeer2011-10-16
* added membership testsGravatar qadeer2011-10-05
* implementing datatypesGravatar qadeer2011-10-05
* Link Model.cs in ModelViewer, so that BVD can be updated independtly of the r...Gravatar Michal Moskal2011-10-03
* MergeGravatar Unknown2011-09-30
|\
* | Started working on inter-procedural inferenceGravatar Unknown2011-09-30
| * MergeGravatar Rustan Leino2011-09-30
| |\
| * | Dafny: fixed bug in translator when LHS of a call was an array element or a natGravatar Rustan Leino2011-09-30
* | | MergeGravatar Unknown2011-09-30
|\ \ \ | | |/ | |/|
* | | Changes to GPUVerifyGravatar Unknown2011-09-30
| * | bug fix in houdiniGravatar qadeer2011-09-30
* | | Refactoring and reorganisation of GPUVerifyGravatar Unknown2011-09-30
|/ /
| * Dafny: improved a resolution error message, and fixed a crash in the resolverGravatar Rustan Leino2011-09-29
* | Added missing filesGravatar Unknown2011-09-29
* | MergeGravatar Unknown2011-09-29
|\|
* | Made use of Houdini optionalGravatar Unknown2011-09-29
| * VCC: Support _(blob ..) types; fix crashGravatar Michal Moskal2011-09-28
| * MergeGravatar Rustan Leino2011-09-28
| |\
* | \ MergeGravatar Unknown2011-09-28
|\ \ \ | | |/ | |/|
| * | MergeGravatar qadeer2011-09-27
| |\ \
| * | | updated Houdini so it works with SMTLibGravatar qadeer2011-09-27
| | * | Bug fix to stratified inlining error trace valuesGravatar Unknown2011-09-28
| |/ /