summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Dafny: added "multiset" keyword to syntax highlighting in emacs, vim, latex, VSXGravatar Rustan Leino2011-11-09
|
* MergeGravatar Rustan Leino2011-11-09
|\
* | Dafny: fixed part of a type-inference issue with datatypes and the < ↵Gravatar Rustan Leino2011-11-09
| | | | | | | | | | | | operator on datatypes Dafny: allow the well-formedness check of a function's specification to know that the function, on the current arguments, returns a value of the declared result type
| * 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
| | | | | | | | | | | | | | | | a previous lemma
* | | | Dafny: added options to make Induction Heuristic apply to array index ↵Gravatar Rustan Leino2011-11-04
| | | | | | | | | | | | | | | | expressions
* | | | MergeGravatar Rustan Leino2011-11-03
|\ \ \ \
* | | | | Added some Dafny and Boogie test cases, including Turing's factorial ↵Gravatar Rustan Leino2011-11-03
| | | | | | | | | | | | | | | | | | | | program, Hoare's classic FIND, and some induction tests for negative integers
| | | * | 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
|/ / /
* | | MergeGravatar Rustan Leino2011-10-31
|\ \ \
| * | | File to experiment with type encoding for .NET.Gravatar Mike Barnett2011-10-31
| | | |
* | | | MergeGravatar Rustan Leino2011-10-31
|\ \ \ \
| | * | | Major changes to the translator traversers because they now are based on theGravatar Mike Barnett2011-10-31
| |/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | new traversers. (The old ones have been marked as obsolete.) All types are now encoded as "datatypes" in Boogie. So non-generic types are nullary functions and generic types just have at least one type argument. Lots of other fixes: string encoding of names is now done by negating Boogie's regular expression for identifiers, etc.
* | | | Fixed the generation of names for datatype functions to use the API forGravatar Mike Barnett2011-10-31
| | | | | | | | | | | | | | | | | | | | | | | | getting SMT-approved names. Fixed a bug in VisitDistinctOp where a bad axiom was being generated when no grouping had more than one occurrence.
* | | | Added information how to customize chalice.bat to find Boogie.exeGravatar peter mueller peter.mueller@inf.ethz.ch2011-10-30
| | | |
* | | | Removed prover option from runtest.bat because smtlib is now the defaultGravatar Mike Barnett2011-10-30
| | | | | | | | | | | | | | | | | | | | in Boogie. Added a test file for our encoding of .NET types in Boogie.
| * | | MergeGravatar Rustan Leino2011-10-29
| |\ \ \ | |/ / / |/| | |
| * | | Dafny induction:Gravatar Rustan Leino2011-10-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | * implemented induction tactic for result-less, non-mutating ghost methods * refine heuristics for determining if a variables is usefully passed to a recursive function * disallow certain "ensures" to use two-state features (needed for soundness of the parallel-statement translation, see comments in Resolver.cs and ParallelResolveErrors.dfy) * added command-line flags /induction and /inductionHeuristic (everything is on by default)
* | | | Boogie build succeededGravatar CodeplexBot2011-10-28
| | | |
* | | | Boogie: Updated the error message for old versions of Z3.Gravatar wuestholz2011-10-28
| | | |
* | | | Tagging EMIC CC.NET build 2.1.31028.0Gravatar VccBuildServer2011-10-28
| | | |
* | | | Boogie build succeeded, 28 test(s) failedGravatar CodeplexBot2011-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 ↵Gravatar Rustan Leino2011-10-27
| | | | | | | | | | | | | | | | | | | | as if the old /bv:z were used
| * | | | Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ↵Gravatar Rustan Leino2011-10-27
| | | | | | | | | | | | | | | | | | | | The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.
| * | | | 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
| |/ / / | | | | | | | | | | | | and out-)parameters
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 22:26:40 +0000