Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | made delegate a datatype | 2011-12-30 | |
| | | | | added a DatatypeConstructor class | ||
* | fixed problems with datatypes | 2011-12-29 | |
| | | | | | removed stale contracts in stratified inlining added test to datatypes | ||
* | fixed a completeness problem in houdini with inlining | 2011-12-18 | |
| | |||
* | Fixed the Boogie build. | 2011-12-16 | |
| | |||
* | Dafny: Made sure that error locations refer to the Dafny program, even if ↵ | 2011-12-15 | |
| | | | | the /print option is used. | ||
* | Boogie: Changed Expr.Not to keep swap arguments rather change direction of ↵ | 2011-12-12 | |
| | | | | operator when negating <, <=, >=, or > | ||
* | Merge | 2011-12-07 | |
|\ | |||
| * | Merge | 2011-12-07 | |
| |\ | |||
| * | | Fix atg file and add comment about Set/*Variable*/ | 2011-12-07 | |
| | | | |||
| * | | Make set iteration order deterministic | 2011-12-07 | |
| | | | | | | | | | | | | Make the set class generic | ||
* | | | Merge | 2011-12-05 | |
|\ \ \ | | |/ | |/| | |||
* | | | Boogie: Added new abstract interpretation harness, which uses native Boogie ↵ | 2011-12-05 | |
| |/ |/| | | | | | | | | | | | | | Expr's, not the more abstract AIExpr's. Boogie: Added Trivial Domain (/infer:t), which just detects assume/assert false. Boogie: Added new Interval Domain (/infer:j), which is stronger than the /infer:i intervals (because the also include preconditions, booleans, and more constraints) and may also be more efficient than previous intervals Boogie: Mark all inferred conditions with attribute {:inferred} | ||
| * | Emit attribute on a requires | 2011-12-04 | |
|/ | |||
* | Added option of turning off model generation in SI. Can be very expensive ↵ | 2011-11-26 | |
| | | | | sometimes. | ||
* | fixed bug in the inlineDepth option for houdini | 2011-11-23 | |
| | | | | small clean up in the inlining implementation | ||
* | Merge | 2011-11-22 | |
|\ | |||
| * | Boogie: don't resolve ignored types (that is, "extern" types that have been ↵ | 2011-11-22 | |
| | | | | | | | | thrown out) | ||
* | | added support for handling duplicate axioms | 2011-11-22 | |
|/ | |||
* | Added lazy summary computation to stratified inlining (not finished yet) | 2011-11-20 | |
| | |||
* | commented calls to GC.Collect() | 2011-11-18 | |
| | |||
* | changed the semantics of requires and ensures for inlined procedures | 2011-11-17 | |
| | |||
* | Boogie: fixed build error (incorrect type in Contract.Result) | 2011-11-16 | |
| | |||
* | Merge | 2011-11-16 | |
|\ | |||
| * | Debugging output for stratified inlining. Emit attribute on Ensures while | 2011-11-16 | |
| | | | | | | | | printing it. | ||
* | | Boogie (and Dafny, with effects also on SscBoogie): I refactored ↵ | 2011-11-15 | |
|/ | | | | CommandLineOptions to separate the options that belong to these 3 tools. | ||
* | changed inlining code so that candidate preconditions and postconditions are ↵ | 2011-11-15 | |
| | | | | ignored | ||
* | 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. | ||
* | moved the addition of selectors and testers to program.Resolve | 2011-11-11 | |
| | |||
* | Merge | 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-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: Get rid of {:inline} attributes on axioms | 2011-10-27 | |
| | | |||
| * | Boogie: Get rid of {:ignore} feature on axioms | 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 | |
|/ | |||
* | Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only) | 2011-10-19 | |
| | |||
* | Merge | 2011-09-28 | |
|\ | |||
| * | bitvector fixes | 2011-09-24 | |
| | | |||
| * | Dafny: Fixed an assertion violation in the "Checked" configuration. | 2011-09-20 | |
| | | |||
* | | Merge | 2011-09-17 | |
|\ \ | |||
| | * | Dafny: Added support for attributes on methods and constructors. | 2011-09-16 | |
| | | | |||
| | * | Fixed test failures in the "Checked" configuration. | 2011-09-19 | |
| |/ | |||
| * | Added "free call" statements that don't check the precondition in the caller. | 2011-09-14 | |
| | | |||
* | | Dafny: generate a compiler error upon encountering an assume statement | 2011-09-11 | |
|/ | | | | Dafny: don't compile programs unless all methods have been verified (or a forced compile is requested) | ||
* | further edits | 2011-09-01 | |
| |