summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Dafny: Start of new refinement features -- clean out old onesGravatar Rustan Leino2012-01-04
|
* MergeGravatar Rustan Leino2012-01-04
|\
* | Dafny: compile let expressions efficiently (i.e., with an extra variable, ↵Gravatar Rustan Leino2012-01-04
| | | | | | | | not with a substitution)
* | Dafny: make /help also print the Boogie command-line optionsGravatar Rustan Leino2012-01-04
| |
| * Copy structs that are passed by value as method call arguments.Gravatar Mike Barnett2012-01-04
| | | | | | | | Define body for default struct ctors.
* | Dafny: don't allow ghost expressions in print statementsGravatar Rustan Leino2012-01-03
|/
* For now, just ignore "address of" nodes and translate the expression of whichGravatar Mike Barnett2012-01-03
| | | | the address is being taken.
* Boogie build succeeded, 1 test(s) failedGravatar CodeplexBot2012-01-01
|
* MergeGravatar qadeer2011-12-31
|\
* | new axioms for subtypingGravatar qadeer2011-12-31
| |
| * Boogie build succeeded, 1 test(s) failedGravatar CodeplexBot2011-12-31
| |
* | modeling multiset using generalized array theoryGravatar qadeer2011-12-30
| |
* | added a test for generalized array theoryGravatar qadeer2011-12-30
|/
* made delegate a datatypeGravatar qadeer2011-12-30
| | | | added a DatatypeConstructor class
* MergeGravatar qadeer2011-12-30
|\
* | problem fixed after CCI updateGravatar qadeer2011-12-30
| |
| * Boogie build succeeded, 1 test(s) failedGravatar CodeplexBot2011-12-30
|/
* added the datatypes testGravatar qadeer2011-12-29
|
* fixed problems with datatypesGravatar qadeer2011-12-29
| | | | | removed stale contracts in stratified inlining added test to datatypes
* MergeGravatar qadeer2011-12-28
|\
* | deleted some commented codeGravatar qadeer2011-12-28
| |
| * Add instrumentation for branches.Gravatar Mike Barnett2011-12-28
| |
| * Dafny: Fixed a bug in the pretty printer.Gravatar wuestholz2011-12-26
|/
* refactored AssertionInjector so that it works directly on bpl files as wellGravatar qadeer2011-12-26
|
* MergeGravatar Kuat Yessenov2011-12-23
|\
* | Chalice: fix for a bug - a source code line got duplicated somehowGravatar Kuat Yessenov2011-12-23
| |
| * Dafny: Extended the support for attributes on method/constructor calls.Gravatar wuestholz2011-12-23
| |
| * Boogie build succeededGravatar CodeplexBot2011-12-23
|/
* Chalice: fix all refinement regression testsGravatar Kuat Yessenov2011-12-23
|
* bug fix in the FreeRequiresVisitorGravatar qadeer2011-12-22
|
* Dafny: Added support for attributes on method/constructor calls.Gravatar wuestholz2011-12-21
|
* Chalice: partial fixes to the broken refinement extension regression tests.Gravatar Kuat Yessenov2011-12-21
|
* MergeGravatar qadeer2011-12-21
|\
| * forgot to check it inGravatar qadeer2011-12-21
| |
* | Boogie build succeeded, 1 test(s) failedGravatar CodeplexBot2011-12-20
| |
| * removed some extraneous parametersGravatar qadeer2011-12-19
|/
* Dafny: for a datatype with just one constructor, don't check (but do assume) ↵Gravatar Rustan Leino2011-12-19
| | | | that destructors are applied only to those values constructed by that one-and-only constructor
* Dafny: compile to .exe only if there is a Main method; otherwise, compile to ↵Gravatar Rustan Leino2011-12-19
| | | | a .dll
* fixed a completeness problem in houdini with inliningGravatar qadeer2011-12-18
|
* Boogie build succeededGravatar CodeplexBot2011-12-16
|
* Fixed the Boogie build.Gravatar wuestholz2011-12-16
|
* Boogie build failedGravatar CodeplexBot2011-12-16
|
* MergeGravatar Unknown2011-12-15
|\
* | A few fixes to get GPUVerify working with OpenCL front-end.Gravatar Unknown2011-12-15
| |
| * Dafny: Made sure that error locations refer to the Dafny program, even if ↵Gravatar wuestholz2011-12-15
| | | | | | | | the /print option is used.
| * Dafny: Added support for attributes on various specification constructs ↵Gravatar wuestholz2011-12-07
| | | | | | | | (assert, ensures, modifies, decreases, invariant).
| * Dafny: implemented thresholds for the new interval domain (/infer:j)Gravatar Rustan Leino2011-12-12
| |
| * Boogie: Changed Expr.Not to keep swap arguments rather change direction of ↵Gravatar Rustan Leino2011-12-12
| | | | | | | | operator when negating <, <=, >=, or >
| * MergeGravatar Rustan Leino2011-12-10
| |\ | |/ |/|
| * Dafny: fix bug in translation of (the splitting of) if-then-else expressions ↵Gravatar Rustan Leino2011-12-10
| | | | | | | | (see bug report Issue 10214 on codeplex)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 22:39:19 +0000