summaryrefslogtreecommitdiff
path: root/Source/AbsInt/ExprFactories.cs
Commit message (Collapse)AuthorAge
* 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.
* Boogie: removed unreachable or unused codeGravatar Rustan Leino2011-10-27
|
* Boogie: Commented out all occurences of repeated inherited contracts - makes ↵Gravatar tabarbe2010-08-27
| | | | fewer error messages when compiling with runtime checking on.
* Boogie: I have successfully ported the AbsInt project. It passes all ↵Gravatar tabarbe2010-07-16
| | | | | | regressions, although DAFNY NEEDS TO BE REBUILT TO RECOGNIZE the changed AbsInt DLL. Address any error complaints to t-abarbe@microsoft.com
* Boogie: Renamed the AbsInt sources for use in the port I have done. ↵Gravatar tabarbe2010-07-16
Regressions with the changed code will take ~10 minutes. I hope I don't break anyone's build.