| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Put in proper namespace, move files around. |  MichalMoskal | 2010-10-12 |
| | | |||
| * | Make the -mv option use the new Model class. | MichalMoskal | 2010-10-12 |
| | | |||
| * | Starting work on Boogie Model Viewer. | 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 |
| | | |||
| * | Fixes in state printing/initialization | MichalMoskal | 2010-10-09 |
| | | |||
| * | Fix some bugs. | MichalMoskal | 2010-10-09 |
| | | |||
| * | Add model/state printing and parsing | MichalMoskal | 2010-10-09 |
| | | |||
| * | Add state sequence API and creation, still untested | MichalMoskal | 2010-10-08 |
| | | |||
| * | Add the new model interface. Untested, doesn't yet include state sequence | MichalMoskal | 2010-10-08 |
| | | |||
| * | Get rid of some CCI dependencies in Driver | MichalMoskal | 2010-10-07 |
| | | |||
| * | Update to VS2010. | MichalMoskal | 2010-10-07 |
| | | |||
| * | Minor fix to recursion depth in stratified inlining algorithm. | akashlal | 2010-10-02 |
| | | |||
| * | 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 | ||
| * | Dafny: Compilation of multi-dimensional arrays | rustanleino | 2010-09-21 |
| | | |||
| * | Some simplifications to coverage reporting for StratifiedInlining. | akashlal | 2010-09-19 |
| | | |||
| * | Fixed an off-by-one error. Added "ReachedBound" as a valid boogie outcome. | akashlal | 2010-09-18 |
| | | |||
| * | Dafny: | rustanleino | 2010-09-17 |
| | | | | | | | * Added full support for multi-dimensional arrays (except for one issue that still needs to be added in compilation) * Changed syntax of array length from |a| to a.Length (for one-dimensional arrays). The syntax for either dimensions is, for example, b.Length0 and b.Length1 for 2-dimensional arrays. * Internally, this meant adding support for built-in classes and readonly fields | ||
| * | Added more stat printing | akashlal | 2010-09-16 |
| | | |||
| * | Dafny: | rustanleino | 2010-09-14 |
| | | | | | | | | | * Added internal support for multi-dimensional arrays (but not all surface syntax is there yet) * Removed unused variables from Dafny.atg Boogie and Dafny: * Improved error message for postcondition violations | ||
| * | 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(). | ||
| * | Fixed a performance issue with StratifiedInlining | akashlal | 2010-09-05 |
| | | |||
| * | Fix for extractLoops | akashlal | 2010-09-04 |
| | | |||
| * | Henrique's addition to the the ErrorHandler API to retrieve models | qadeer | 2010-09-03 |
| | | |||
| * | 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. | ||
| * | Changed the interface of Parse so that it can consume a program from a Stream | akashlal | 2010-09-03 |
| | | |||
| * | bunch of fixes related to Boogie error model generation from the Z3 error ↵ | qadeer | 2010-09-03 |
| | | | | | model generation | ||
| * | Bug fix for StratifiedInlining. Use extra Booleans to model procedure calls, ↵ | akashlal | 2010-09-02 |
| | | | | | instead of uninterpreted predicates. | ||
| * | fixed bug in extract loops by ensuring that loop extraction is done in ↵ | qadeer | 2010-09-01 |
| | | | | | nesting order | ||
| * | Minor fix to my previous commit | akashlal | 2010-09-01 |
| | | |||
| * | Added a way of recovering counterexample paths after loop extraction. ↵ | akashlal | 2010-09-01 |
| | | | | | Stable, but still buggy. | ||
| * | Version-stamp CCE assembly | stobies | 2010-09-01 |
| | | |||
| * | Added a new class LoopProcedure to represent the procedures representing ↵ | qadeer | 2010-09-01 |
| | | | | | extracted loops. | ||
| * | Dafny: added a command-line option to change the prelude file | sboehme | 2010-08-30 |
| | | |||
| * | added a new api to Z3apiProcessTheoremProver for asserting axioms | qadeer | 2010-08-29 |
| | | |||
| * | created a new build target called z3apidebug. | qadeer | 2010-08-29 |
| | | | | | | only this target has a compile time dependency on Microsoft.Z3.dll. To compile this target, a reference to z3api must be manually added to BoogieDriver. | ||
| * | BeginCheck now adds context.Axioms as well as the conjecture to the context. | qadeer | 2010-08-29 |
| | | | | | Also started using the new quantifier api. | ||
| * | Added a constructor to a contract class otherwise the compiler complained ↵ | mikebarnett | 2010-08-28 |
| | | | | | about the default nullary one calling its base class nullary ctor, and there wasn't one. | ||
| * | Boogie: Accidentally created a service references folder in Boogie's folder ↵ | tabarbe | 2010-08-27 |
| | | | | | tree. Fixed that error. | ||
| * | Boogie: Simplify: Added a contracts class that I forgot in the initial porting. | tabarbe | 2010-08-27 |
| | | |||
| * | Dafny: fallback to ShallowType (elements of IndexField arrays seem to have ↵ | sboehme | 2010-08-27 |
| | | | | | Type null) | ||
| * | 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). | ||
| * | Dafny: added inlined functions making reads and updates of the heap explicit | sboehme | 2010-08-27 |
| | | |||
| * | Boogie: Removed an incorrect Ensures clause on a void method. | tabarbe | 2010-08-27 |
| | | |||
| * | fixed bug with function name look up | qadeer | 2010-08-27 |
| | | |||
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |