Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | using model instead of labels | 2012-02-23 | ||
| | ||||
* | Use DateTime.UtcNow instead of DateTime.Now | 2012-01-11 | ||
| | | | | see http://blogs.msdn.com/b/kirillosenkov/archive/2012/01/10/datetime-utcnow-is-generally-preferable-to-datetime-now.aspx | |||
* | Boogie: fixed proof-obligation counting | 2012-01-09 | ||
| | ||||
* | Boogie: output number of proof obligations (asserts) along with timing ↵ | 2012-01-09 | ||
| | | | | information when using the /trace option | |||
* | Boogie: Fixed a crash due to old expressions in lambda expressions that were ↵ | 2011-12-02 | ||
| | | | | | | not replaced after lambda expansion. (reported by Florian Egli) | |||
* | Remove invariant that was just wrong | 2011-11-28 | ||
| | ||||
* | refactoring houdini so that it creates only a single instance of z3 | 2011-11-16 | ||
| | ||||
* | Boogie (and Dafny, with effects also on SscBoogie): I refactored ↵ | 2011-11-15 | ||
| | | | | CommandLineOptions to separate the options that belong to these 3 tools. | |||
* | partial check in regarding getting states working with stratified inlining | 2011-09-06 | ||
| | ||||
* | reverting irreducible handling temporarily | 2011-08-21 | ||
|\ | ||||
* | | added code to handle irreducible graphs | 2011-08-20 | ||
| | | ||||
* | | minor refactoring | 2011-08-17 | ||
| | | ||||
* | | deleted lazyinlining option 2 and 3 | 2011-08-17 | ||
| | | | | | | | | fixed proc copy bounding | |||
* | | Added "procedure-copy bounding" for lazy inlining | 2011-08-10 | ||
| | | ||||
* | | further changes for making houdini work | 2011-08-04 | ||
|/ | ||||
* | ported all the counterexample code to Michal's new Model class; the goal is ↵ | 2011-06-27 | ||
| | | | | to eliminate the class ErrorModel from the codebase. | |||
* | early clearing of live variables and incarnation maps | 2011-06-24 | ||
| | ||||
* | implementation of iterative LetVC | 2011-06-23 | ||
| | ||||
* | Bug fix for trace generation with extractLoop option | 2011-06-23 | ||
| | ||||
* | LetVC can get null label2absy from lazy inlining. So, I weakened the ↵ | 2011-05-03 | ||
| | | | | precondition otherwise the checked build was failing | |||
* | modified letvc generation so that the use of control flow function and ↵ | 2011-04-15 | ||
| | | | | labels is decoupled. Former is controled by controlFlowVariable and the latter by label2Absy. | |||
* | added reachability information to the VC and used that to support arbitrary ↵ | 2011-04-14 | ||
| | | | | asserts in lazy inlining | |||
* | minor fix with loopy counterexample generation | 2011-03-18 | ||
| | ||||
* | new algorithm for dead code detection (vc:doomed) | 2011-03-15 | ||
| | ||||
* | Replaced all dictionaries that mapped to bool (i.e., were being used to ↵ | 2011-03-10 | ||
| | | | | implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null. | |||
* | Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵ | 2011-03-10 | ||
| | | | | | | dictionaries are non-null, which is enforced by the implementation of Dictionary. Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked. | |||
* | Fix contracts so runtime checking can be turned on. | 2011-03-07 | ||
| | ||||
* | Don't treat "Inconclusive" answer as fatal when splitting. | 2011-02-02 | ||
| | ||||
* | Add new feature: {:selective_checking} on procedures. See testcase for a ↵ | 2010-12-17 | ||
| | | | | description (it was implemented in VCC before and is quite useful). | |||
* | Add functions generated in lambda-expansion of function body to top-level ↵ | 2010-12-17 | ||
| | | | | program declarations. | |||
* | Refactoring: pulled out all code for stratified inlining to a new file. | 2010-11-23 | ||
| | ||||
* | Changed stratified inlining: can now be user-guided | 2010-11-22 | ||
| | ||||
* | Minor updates for printing coverage graph of stratified inlining | 2010-11-14 | ||
| | ||||
* | Make the -mv option use the new Model class. | 2010-10-12 | ||
| | ||||
* | Boogie: | 2010-10-12 | ||
| | | | | | | * enhanced the printing of captured states * addressed some warnings issued by VS 2010 * some code formatting | |||
* | Minor fix to recursion depth in stratified inlining algorithm. | 2010-10-02 | ||
| | ||||
* | Boogie: | 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: | 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 | |||
* | Some simplifications to coverage reporting for StratifiedInlining. | 2010-09-19 | ||
| | ||||
* | Fixed an off-by-one error. Added "ReachedBound" as a valid boogie outcome. | 2010-09-18 | ||
| | ||||
* | Added more stat printing | 2010-09-16 | ||
| | ||||
* | Added a new VC.ConditionGeneration.Outcome: StratifiedInlining can signal ↵ | 2010-09-05 | ||
| | | | | that it has reached the recursion bound. | |||
* | Fixed a performance issue with StratifiedInlining | 2010-09-05 | ||
| | ||||
* | Fix for extractLoops | 2010-09-04 | ||
| | ||||
* | Henrique's addition to the the ErrorHandler API to retrieve models | 2010-09-03 | ||
| | ||||
* | Bug fix for StratifiedInlining. Use extra Booleans to model procedure calls, ↵ | 2010-09-02 | ||
| | | | | instead of uninterpreted predicates. | |||
* | Minor fix to my previous commit | 2010-09-01 | ||
| | ||||
* | Added a way of recovering counterexample paths after loop extraction. ↵ | 2010-09-01 | ||
| | | | | Stable, but still buggy. | |||
* | Boogie: Commented out all occurences of repeated inherited contracts - makes ↵ | 2010-08-27 | ||
| | | | | fewer error messages when compiling with runtime checking on. | |||
* | bug fixes in z3api | 2010-08-26 | ||
| |