Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Removed AIFramework from Boogie -- use native trivial or native ↵ | boehmes | 2012-09-27 |
| | | | | | | | interval-based abstract interpretation instead. Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie. Command-line option '/logInfer' has been dropped. | ||
* | Use DateTime.UtcNow instead of DateTime.Now | stobies | 2012-01-11 |
| | | | | see http://blogs.msdn.com/b/kirillosenkov/archive/2012/01/10/datetime-utcnow-is-generally-preferable-to-datetime-now.aspx | ||
* | Dafny: implemented thresholds for the new interval domain (/infer:j) | Rustan Leino | 2011-12-12 |
| | |||
* | Dafny: corrected merge snafus | Rustan Leino | 2011-12-07 |
| | |||
* | Boogie: Added new abstract interpretation harness, which uses native Boogie ↵ | Rustan Leino | 2011-12-05 |
Expr's, not the more abstract AIExpr's. Boogie: Added Trivial Domain (/infer:t), which just detects assume/assert false. Boogie: Added new Interval Domain (/infer:j), which is stronger than the /infer:i intervals (because the also include preconditions, booleans, and more constraints) and may also be more efficient than previous intervals Boogie: Mark all inferred conditions with attribute {:inferred} |