summaryrefslogtreecommitdiff
path: root/Source/AbsInt/NativeLattice.cs
Commit message (Collapse)AuthorAge
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-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.
* Did some refactoring.Gravatar wuestholz2014-09-23
|
* CmdSeq: farewellGravatar Ally Donaldson2013-07-22
|
* Removed AIFramework from Boogie -- use native trivial or native ↵Gravatar boehmes2012-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.NowGravatar stobies2012-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)Gravatar Rustan Leino2011-12-12
|
* Dafny: corrected merge snafusGravatar Rustan Leino2011-12-07
|
* Boogie: Added new abstract interpretation harness, which uses native Boogie ↵Gravatar Rustan Leino2011-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}