| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | made delegate a datatype |  qadeer | 2011-12-30 |
| | | | | | added a DatatypeConstructor class | ||
| * | fixed problems with datatypes | qadeer | 2011-12-29 |
| | | | | | | removed stale contracts in stratified inlining added test to datatypes | ||
| * | Merge |  Rustan Leino | 2011-12-07 |
| |\ | |||
| | * | Merge |  Michal Moskal | 2011-12-07 |
| | |\ | |||
| | * | | Make set iteration order deterministic | Michal Moskal | 2011-12-07 |
| | | | | | | | | | | | | | Make the set class generic | ||
| * | | | Merge | Rustan Leino | 2011-12-05 |
| |\ \ \ | | |/ | |/| | |||
| * | | | Boogie: Added new abstract interpretation harness, which uses native Boogie ↵ | Rustan Leino | 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 |  akashlal | 2011-12-04 |
| |/ | |||
| * | Merge | qadeer | 2011-11-22 |
| |\ | |||
| | * | Boogie: don't resolve ignored types (that is, "extern" types that have been ↵ | Rustan Leino | 2011-11-22 |
| | | | | | | | | | thrown out) | ||
| * | | added support for handling duplicate axioms | qadeer | 2011-11-22 |
| |/ | |||
| * | Debugging output for stratified inlining. Emit attribute on Ensures while |  Unknown | 2011-11-16 |
| | | | | | printing it. | ||
| * | moved the addition of selectors and testers to program.Resolve | qadeer | 2011-11-11 |
| | | |||
| * | deleted unused code | qadeer | 2011-11-01 |
| | | |||
| * | Boogie: Get rid of {:inline} attributes on axioms | Michal Moskal | 2011-10-27 |
| | | |||
| * | Boogie: removed unreachable or unused code | Rustan Leino | 2011-10-27 |
| | | |||
| * | Dafny: Fixed an assertion violation in the "Checked" configuration. | wuestholz | 2011-09-20 |
| | | |||
| * | Dafny: Added support for attributes on methods and constructors. | wuestholz | 2011-09-16 |
| | | |||
| * | Fixed test failures in the "Checked" configuration. | wuestholz | 2011-09-19 |
| | | |||
| * | Support for irreducible graphs (with extractLoops) | Unknown | 2011-08-24 |
| | | |||
| * | reverting irreducible handling temporarily | qadeer | 2011-08-21 |
| |\ | |||
| * | | added code to handle irreducible graphs | qadeer | 2011-08-20 |
| | | | |||
| * | | ExtractLoops calls the same code for eliminating unreachable blocks that ↵ | qadeer | 2011-07-05 |
| |/ | | | | | | normal VCgen calls. Deleted a procedure that was not being used as a result. Added an extra assume(false) at the end of each DispatchContinuation to help boogie vcgen. | ||
| * | Boogie: white-space formating | Rustan Leino | 2011-06-05 |
| | | |||
| * | Boogie: added features to help with modular verification. In particular, ↵ | Rustan Leino | 2011-05-13 |
| | | | | | define FILE_n when parsing file n on the command line, and support :extern and :ignore attributes on top-level declarations. | ||
| * | Add labels to extracted procedures for loops | akashlal | 2011-03-14 |
| | | |||
| * | Changed the API for Declaration.AddAttribute so it takes a params argument ↵ | mikebarnett | 2011-02-09 |
| | | | | | so multiple parameters can be added to an attribute at one go. No calls had to be changed because of the way params arguments work. | ||
| * | Eliminated dependencies on SpecSharp and CCI from Boogie.sln and Dafny.sln | qadeer | 2010-12-01 |
| | | |||
| * | a bug fix in the loop extraction code | qadeer | 2010-10-19 |
| | | | | | optimized the signature of the extracted procedure | ||
| * | Boogie: | rustanleino | 2010-10-12 |
| | | | | | | | * enhanced the printing of captured states * addressed some warnings issued by VS 2010 * some code formatting | ||
| * | added an optimization to extract loops so that only loop targets are treated ↵ | qadeer | 2010-09-10 |
| | | | | | as output variables of the extracted procedure. | ||
| * | Added a new VC.ConditionGeneration.Outcome: StratifiedInlining can signal ↵ | akashlal | 2010-09-05 |
| | | | | | that it has reached the recursion bound. | ||
| * | Delete unreachable Blocks of an Impl before calling ExtractLoops(). | akashlal | 2010-09-05 |
| | | | | | This helps avoid a crash inside NewComputeDominators(). | ||
| * | Fix for extractLoops | akashlal | 2010-09-04 |
| | | |||
| * | more fixes to ExtractLoops | qadeer | 2010-09-03 |
| | | |||
| * | Added a fix to extract loops code so that it returns a more comprehensive ↵ | qadeer | 2010-09-03 |
| | | | | | map of block names to original blocks. | ||
| * | fixed bug in extract loops by ensuring that loop extraction is done in ↵ | qadeer | 2010-09-01 |
| | | | | | nesting order | ||
| * | Added a way of recovering counterexample paths after loop extraction. ↵ | akashlal | 2010-09-01 |
| | | | | | Stable, but still buggy. | ||
| * | Added a new class LoopProcedure to represent the procedures representing ↵ | qadeer | 2010-09-01 |
| | | | | | extracted loops. | ||
| * | Boogie: Commented out all occurences of repeated inherited contracts - makes ↵ | tabarbe | 2010-08-27 |
| | | | | | fewer error messages when compiling with runtime checking on. | ||
| * | Boogie: Committing changed source files | tabarbe | 2010-08-20 |
| | | |||
| * | Boogie: Renaming core sources in preparation for port commit | tabarbe | 2010-08-20 |
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |