Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | changed inlining code so that candidate preconditions and postconditions are ↵ | 2011-11-15 | |
| | | | | ignored | ||
* | fixed another bug in model parser related to datatype values | 2011-11-14 | |
| | | | | cleaned up the code related to v1model | ||
* | added the option /inlineDepth:n. This option defaults to -1. If the user ↵ | 2011-11-13 | |
| | | | | | | provides a non-negative number then that number is used to inline procedures not annotated by {:inline n} attribute. | ||
* | Merge | 2011-11-11 | |
|\ | |||
| * | moved the addition of selectors and testers to program.Resolve | 2011-11-11 | |
| | | |||
* | | Produce unsat cores only when enabled (in stratified inlining) | 2011-11-11 | |
|/ | |||
* | Dafny: allow assert/assume expressions in more places | 2011-11-09 | |
| | |||
* | Dafny: added assert/assume expressions | 2011-11-09 | |
| | |||
* | Merge | 2011-11-09 | |
|\ | |||
* | | copied all attributes of the constructor (except for :constructor) to the ↵ | 2011-11-09 | |
| | | | | | | | | selector and membership functions | ||
| * | VCC: remove _vcc_math_type_ from type names | 2011-11-09 | |
| | | |||
| * | VCC: hide #limited# functions | 2011-11-09 | |
| | | |||
| * | Merge | 2011-11-09 | |
| |\ | |||
| * | | Dafny: moved definition of class.array into prelude, anticipating writing ↵ | 2011-11-09 | |
| | | | | | | | | | | | | axioms that use it | ||
| | * | Refactoring, and work on race checking contracts | 2011-11-09 | |
| |/ | |||
| * | Merge | 2011-11-09 | |
| |\ | |||
| * | | Dafny: fixed part of a type-inference issue with datatypes and the < ↵ | 2011-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 | ||
| | * | BVD: don't do the "Duplicate entry exception"; uncomment for debugging | 2011-11-08 | |
| | | | |||
| | * | VCC: show output parameters as roots | 2011-11-08 | |
| |/ |/| | |||
* | | moved GPUVerify into its own solution | 2011-11-08 | |
|/ | |||
* | Merge | 2011-11-08 | |
|\ | |||
* | | Dafny: fixed bug in reads checking of array-to-sequence conversions | 2011-11-08 | |
| | | |||
| * | Merge | 2011-11-08 | |
| |\ | |||
| * | | Additions to GPU Verify for paper submission. | 2011-11-08 | |
| | | | |||
| | * | some refactoring suggested by Michal | 2011-11-07 | |
| | | | |||
| | * | Merge | 2011-11-07 | |
| | |\ | |||
| | * \ | Merge | 2011-11-07 | |
| | |\ \ | |_|/ / |/| | | | |||
| | * | | change in model parsing with datatype values | 2011-11-07 | |
| | | | | |||
* | | | | Dafny: added a new /inductionHeuristic option | 2011-11-04 | |
| | | | | |||
* | | | | Dafny: added options to make Induction Heuristic apply to array index ↵ | 2011-11-04 | |
| | | | | | | | | | | | | | | | | expressions | ||
| | * | | deleted unused code | 2011-11-01 | |
| |/ / |/| | | |||
* | | | Merge | 2011-10-31 | |
|\ \ \ | |||
* | | | | Fixed the generation of names for datatype functions to use the API for | 2011-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. | ||
| * | | | Merge | 2011-10-29 | |
| |\ \ \ | |/ / / |/| | | | |||
| * | | | Dafny induction: | 2011-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: Updated the error message for old versions of Z3. | 2011-10-28 | |
| | | | | |||
* | | | | Boogie: Get rid of {:inline} attributes on axioms | 2011-10-27 | |
| | | | | |||
* | | | | Boogie: Get rid of {:ignore} feature on axioms | 2011-10-27 | |
| | | | | |||
* | | | | Boogie: Present a nice error message when Z3 of lesser version than 3.2 is found | 2011-10-27 | |
| | | | | |||
* | | | | Merge | 2011-10-27 | |
|\ \ \ \ | |||
* | | | | | Restart prover after out-of-memory error; honour -restartProver option | 2011-10-27 | |
| | | | | | |||
| * | | | | Boogie: removed unreachable or unused code | 2011-10-27 | |
| | | | | | |||
| * | | | | Boogie: internal clean-up, removed BvHandling type, everything now behaves ↵ | 2011-10-27 | |
| | | | | | | | | | | | | | | | | | | | | as if the old /bv:z were used | ||
| * | | | | Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ↵ | 2011-10-27 | |
| | | | | | | | | | | | | | | | | | | | | The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated. | ||
| * | | | | Boogie: Changed default /prover to SMTLIB | 2011-10-27 | |
| | | | | | |||
| | | | * | Merge | 2011-10-27 | |
| | | | |\ | | |_|_|/ | |/| | | | |||
| | | | * | various refactorings | 2011-10-27 | |
| | | | | | |||
| | * | | | Dafny: allow attributes on function/method declarations to refer to the (in- ↵ | 2011-10-26 | |
| |/ / / | | | | | | | | | | | | | and out-)parameters | ||
| * | | | Dafny: removed Dafny's "foreach" statements (replaced by the new "parallel" ↵ | 2011-10-26 | |
| | | | | | | | | | | | | | | | | statement) | ||
| * | | | Dafny: removed support for assigning to an array-range (that is, an ↵ | 2011-10-26 | |
| | | | | | | | | | | | | | | | | assignment statement where the LHS has the form a[lo..hi]) |