Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Procedure Copy Bounding for Stratified Inlinig | 2011-08-25 | |
| | |||
* | 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. | ||
* | Fixed non-incremental option of stratified inlining | 2011-06-27 | |
| | |||
* | FindLeastToVerify: accept multiple procedures | 2011-06-26 | |
| | |||
* | Avoid restarting the theorem prover for stratified inlining because it | 2011-06-25 | |
| | | | | | can lose context. Added a cache for FindLeastToVerify | ||
* | 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 | |
| | |||
* | Add a string for an uninterpreted value in errModel | 2011-06-06 | |
| | |||
* | 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. | ||
* | merge | 2011-04-14 | |
|\ | |||
* | | added reachability information to the VC and used that to support arbitrary ↵ | 2011-04-14 | |
| | | | | | | | | asserts in lazy inlining | ||
| * | Stratified Inlining: minor bux fix with recording model values | 2011-04-14 | |
|/ | |||
* | Minor fixes | 2011-03-27 | |
| | |||
* | Boogie: fixed contract violation in stratified inlining | 2011-03-23 | |
| | |||
* | Print recorded value of any type | 2011-03-21 | |
| | |||
* | Bug fix with model generation. | 2011-03-21 | |
| | |||
* | minor fix with loopy counterexample generation | 2011-03-18 | |
| | |||
* | Print out requested values in the counterexample trace | 2011-03-17 | |
| | |||
* | Re-enabled quantifier checking in the Checked configuration. | 2011-03-16 | |
| | |||
* | new algorithm for dead code detection (vc:doomed) | 2011-03-15 | |
| | |||
* | Turn off quantifier checking in the runtime checking. | 2011-03-14 | |
| | |||
* | 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. | ||
* | Updated PrepareBoogieZip.bat to include BVD and smt2 | 2011-03-10 | |
| | | | | Ignore duplicated else functions in models | ||
* | Added a new solution configuration, Checked, that builds the Checked ↵ | 2011-03-07 | |
| | | | | configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration. | ||
* | Fix contracts so runtime checking can be turned on. | 2011-03-07 | |
| | |||
* | Handle as-array[...] model elements | 2011-02-23 | |
| | |||
* | Parse else-> clauses in the model | 2011-02-23 | |
| | | | | Disable MODEL_PARTIAL in SMTLib | ||
* | Throw exceptions when push/pop interface is used but not implemented | 2011-02-23 | |
| | | | | Complete ErrorModel tables with the final bogus else clause | ||
* | Implement Push/Pop interface. | 2011-02-23 | |
| | | | | Implement ProverContext.Lookup method. | ||
* | Move model printing to ErrorModel class | 2011-02-21 | |
| | | | | Allow construction of ErrorModel instance from Model instance | ||
* | Allow use ErrorModel as a container for Model - make -mv work with SMTLib on Z3 | 2011-02-18 | |
| | |||
* | Kill {:prover "..."} attribute support; no one ever used this stuff | 2011-02-17 | |
| | |||
* | Stratified inlining: Added concrete values to error traces. Added an extra ↵ | 2011-02-17 | |
| | | | | flag "inferLeastForUnsat". | ||
* | Fix with timeout | 2011-02-12 | |
| | |||
* | Better support for timeout | 2011-02-12 | |
| | |||
* | Get rid of -smtOutput option. Add /proverOpt:OUTPUT=... to SMT and TPTP ↵ | 2011-02-11 | |
| | | | | provers. Add handling of help message about /proverOpt. | ||
* | Minor change to stratified inlining | 2011-02-11 | |
| | |||
* | Added a new method StratifiedVC for refinement. | 2011-02-08 | |
| | | | | Added a method to copy a FunctionCall. | ||
* | implemented /UseUnsatCoreForInlining option for use in stratified inlining | 2011-02-06 | |
| | |||
* | deleted debugging statement | 2011-02-05 | |
| | |||
* | Fix to counterexample generation for over-approx query | 2011-02-05 | |
| |