| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
| |
negative numbers. I have decided that this method will floor towards
negative infinity rather than zero to match SMT-LIBv2's to_int function.
|
| |
|
|
|
|
|
|
| |
numbers correctly.
For example BigDec.FromString("-1.5") would be interpreted as
-0.5 due to the incorrect way the method handles the fractional
part of the string.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real';
Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted;
Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs);
Extended the BigDec class with additional functionality;
Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
|
| |/ |
|
| |\ |
|
| | | |
|
| | |
| |
| |
| | |
Make the set class generic
|
| |/
|
|
|
|
|
|
| |
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}
|
| | |
|
| | |
|
| |
|
|
| |
configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration.
|
| | |
|
| | |
|
| |
|
|
| |
structure instead
|
| |
|
|
| |
Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
|
| |
|
|
|
|
| |
* enhanced the printing of captured states
* addressed some warnings issued by VS 2010
* some code formatting
|
| | |
|
| |
|
|
|
| |
only this target has a compile time dependency on Microsoft.Z3.dll.
To compile this target, a reference to z3api must be manually added to BoogieDriver.
|
| |
|
|
| |
doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
|
| |
|
|
| |
project in the Boogie solution references. Dafny.csproj has an internal copy of cce, so does not reference this project, because the Dafny cce uses some Dafny-defined types in its helper methods.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
The functionality is currently broken.
* Adjust procedure summaries also after processing call returns (used only in interprocedural inference, which is currently not really supported, but this change would be needed if we ever decide to support it)
* Some other code clean-up, like removing unnecessary [Reads(...Owned)] attributes on [Pure] methods
|
| | |
|
| | |
|
| |
|
Dan Liew
Rustan Leino
pantazis
Unknown
Rustan Leino
Michal Moskal