Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Minor change | 2015-12-29 | |
| | |||
* | Add experimental support for optimization (requires Z3 build after changeset ↵ | 2015-11-18 | |
| | | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7). | ||
* | Add support for identifying unnecessary assumes. | 2015-11-16 | |
| | |||
* | Normalise line endings using a .gitattributes file. Unfortunately | 2015-06-28 | |
| | | | | | | this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. | ||
* | Add some experimental support for diagnosing timeouts. | 2015-05-18 | |
| | |||
* | Minor change to the encoding of partially verified assertions as VC | 2015-01-30 | |
| | |||
* | Worked on the verification result caching (use native support for partially ↵ | 2015-01-16 | |
| | | | | verified assertions). | ||
* | Added a test and a todo. | 2015-01-02 | |
| | |||
* | Worked on more native support for partially-verified assertions. | 2014-12-28 | |
| | |||
* | Cleanup: removed unused code | 2014-09-29 | |
| | |||
* | Bug fix in stratified inlining (triggered by {:inline} functions) | 2013-10-21 | |
| | |||
* | fixed the problem with codexprs | 2013-09-07 | |
| | | | | now positive/negative context is detected and appropriate translation is done | ||
* | When a codeexpr is used at the top-level in an assume statement, we use the ↵ | 2013-09-04 | |
| | | | | alternative existential semantics. | ||
* | More refactoring towards replacing PureCollections.Sequence with List | 2013-07-22 | |
| | |||
* | Refactored labsl2absy so that it is a Dictionary<int, Absy> instead of a ↵ | 2013-07-22 | |
| | | | | plain Hashtable. | ||
* | Removed old comments about "BASEMOVE" and other constructor calls, where the ↵ | 2013-01-07 | |
| | | | | conversion from Spec# into C# moved a constructor call | ||
* | various cleanup regarding /doNotUseLabels | 2012-02-28 | |
| | |||
* | bug fixes related to using ControlFlowFunction instead of labels | 2012-02-23 | |
| | |||
* | using model instead of labels | 2012-02-23 | |
| | |||
* | Boogie: output number of proof obligations (asserts) along with timing ↵ | 2012-01-09 | |
| | | | | information when using the /trace option | ||
* | Added lazy summary computation to stratified inlining (not finished yet) | 2011-11-20 | |
| | |||
* | 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 | ||
* | 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 | ||
* | Boogie: Added boolean code expressions (sans well-formedness checks on the ↵ | 2010-08-10 | |
| | | | | input). | ||
* | Boogie: VCGeneration port part 1/3: Replacing old source files with ported ↵ | 2010-07-28 | |
| | | | | version | ||
* | Boogie\VCGeneration: Renaming sources in preparation for my addition of the ↵ | 2010-07-28 | |
ported C# version |