| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Boogie: Did some minor refactoring. |  wuestholz | 2010-12-10 |
| | | |||
| * | Construct @MV_state function only once so it doesn't get renamed to ↵ | MichalMoskal | 2010-12-02 |
| | | | | | @MV_state@@0 when we have more than one procedure to verify | ||
| * | Refactoring: pulled out all code for stratified inlining to a new file. | akashlal | 2010-11-23 |
| | | |||
| * | Dafny: a partial first crack at a Dafny model-viewer provider, including ↵ | rustanleino | 2010-11-01 |
| | | | | | captureState mark-ups in the Boogie code generated from Dafny | ||
| * | Skip unchagned variables in model dumps. Fix testcase | MichalMoskal | 2010-10-14 |
| | | |||
| * | Add interfaces for langauge providers. Start with VCC provider. | MichalMoskal | 2010-10-12 |
| | | |||
| * | Add missing Clone() when storing incarnation maps; update testcase to make ↵ | MichalMoskal | 2010-10-12 |
| | | | | | | | this clear Construct states in Model properly, nuke direct printing. | ||
| * | Make the -mv option use the new Model class. | MichalMoskal | 2010-10-12 |
| | | |||
| * | Boogie: | rustanleino | 2010-10-12 |
| | | | | | | | * enhanced the printing of captured states * addressed some warnings issued by VS 2010 * some code formatting | ||
| * | Boogie: fixed a Code Contract in the source | rustanleino | 2010-10-09 |
| | | |||
| * | Add state sequence API and creation, still untested | MichalMoskal | 2010-10-08 |
| | | |||
| * | Boogie: | rustanleino | 2010-09-24 |
| | | | | | | * Added Test/textbook/DivMod.bpl, which embodies a conversion between C's div/mod operators and SMT Lib's div/mod operators. * Added a rudimentary printing of variables for captured states. It doesn't attempt to print everything at this time, and it doesn't work when variables get unique-ified by @@-suffixes. A more complete implementation will be added at a later time. | ||
| * | Boogie: | rustanleino | 2010-09-23 |
| | | | | | | | * Added /mv flag as the start of a Boogie replacement for /cev * Allow attributes on assume statements * /mv looks for the assume-statement attribute :captureState with a string-literal argument | ||
| * | Added a new VC.ConditionGeneration.Outcome: StratifiedInlining can signal ↵ | akashlal | 2010-09-05 |
| | | | | | that it has reached the recursion bound. | ||
| * | Henrique's addition to the the ErrorHandler API to retrieve models | qadeer | 2010-09-03 |
| | | |||
| * | Added a way of recovering counterexample paths after loop extraction. ↵ | akashlal | 2010-09-01 |
| | | | | | Stable, but still buggy. | ||
| * | Boogie: Commented out all occurences of repeated inherited contracts - makes ↵ | tabarbe | 2010-08-27 |
| | | | | | fewer error messages when compiling with runtime checking on. | ||
| * | Boogie: Removed some errors with code contracts (commenting out ↵ | tabarbe | 2010-08-27 |
| | | | | | doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however). | ||
| * | Boogie: Fixed some doubly-inherited-contract occurrences. | tabarbe | 2010-08-20 |
| | | |||
| * | Boogie: Added boolean code expressions (sans well-formedness checks on the ↵ | rustanleino | 2010-08-10 |
| | | | | | input). | ||
| * | More line ending fixups. | MichalMoskal | 2010-08-06 |
| | | |||
| * | Boogie: Removed trailing spaces in code | tabarbe | 2010-08-04 |
| | | |||
| * | Boogie: VCGeneration port part 1/3: Replacing old source files with ported ↵ | tabarbe | 2010-07-28 |
| | | | | | version | ||
| * | Boogie\VCGeneration: Renaming sources in preparation for my addition of the ↵ | tabarbe | 2010-07-28 |
| ported C# version | |||
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |