| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
true but A.GetHashCode() == B.GetHashCode() return false.
The case of the bug was that Args.GetHashCode() was being used which
uses Object.GetHashCode() which uses references to compute GetHashCode().
This is wrong because we want hash codes to equal for structural equality.
To fix this I've implemented a really simple hashing method. I have not tested
how resilient this is to collisions.
|
| |/
|
|
|
|
|
|
| |
The previous implementation which called object.Equals(this.Args, other.Args)
would in turn call ``this.Args.Equals(others.Args)`` which for List<> is
reference equality. Equals() is purposely overloaded on Expr classes in Boogie
to provide structural equality so this has been fixed so a comparision of
elements in the list is performed.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
There were many calls in the code to
``` new TokenTextWriter("<buffer>", buffer, false) ```
Prior to 61a94f409975 this was a call to the following constructor
```
TokenTextWriter(string filename, TextWriter writer, bool setTokens)
```
After that commit these then became calls to
```
TokenTextWriter(string filename, TextWriter writer, bool pretty)
```
An example of where this would cause issues was if ToString() was called on an
AbsyCmd then the its token would be modified because the setTokens parameter
was effectively set to True when the original intention was for it to be set
to false!
To fix this I've
* Removed the default parameter value for pretty and fixed all
uses so that we pass false where it was implicitly being set before
* Where the intention was to set setTokens to false this has been fixed so
it is actually set to false!
Unfortunately I couldn't find a way of observing this bug from the Boogie
executable so I couldn't create a test case. I could only observe it when I was
using Boogie's APIs.
|
| | |
|
| |
|
|
| |
advanced verification result caching even for implementations with errors.
|
| |
|
|
|
|
| |
When running boogie form the command line, this should be on by default.
On the other hand, the TokenTextWriter constructors and PrintBplFile now have an
argument for this, but by default it is off.
|
| |
|
|
| |
others already present for bool, BigNum and BigDec.
|
| |
|
|
|
| |
Reduce depth of AST whenever possible (e.g., use a binary tree instead of a
linear list of terms)
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
conversion from Spec# into C# moved a constructor call
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
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)
|
| |
|
|
| |
of / and %
|
| |
|
|
|
|
|
| |
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.
|
| |
|
|
| |
operator when negating <, <=, >=, or >
|
| |\ |
|
| | | |
|
| | |
| |
| |
| | |
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}
|
| |
|
|
| |
The :forceBvZ3Native, :forceBvInt, and :bvint attributes were also eliminated.
|
| | |
|
| |
|
|
| |
pretty printing
|
| |
|
|
| |
Added a method to copy a FunctionCall.
|
| |
|
|
| |
fewer error messages when compiling with runtime checking on.
|
| | |
|
| |
|
qadeer
Dan Liew
Dan Rosén
Unknown
Unknown
Rustan Leino
Michal Moskal