| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | 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 |