| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Only set produce-unsat-cores in the case /explainHoudini is passed. This
allows contract inference to be used with solvers that do no support unsat
cores, as long as no explanation of the Houdini run is required.
|
| | |
|
| |
|
|
| |
condition is assumed while inlining.
|
| | |
|
| | |
|
| |
|
|
| |
changed the attribute on callee ensures to "HoudiniAssume" rather than "assume"
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
integer as a key. This allows any arbitrary "metadata" to be attached
at runtime. The implementation is lazy so the container is only created
if the SetMetadata<T>() method is called which should keep the memory
overhead very minimal.
Example usage:
var TheAssert = new AssertCmd(...);
...
TheAssert.SetMetadata(0, new List<Expr>());
TheAssert.GetMetadata<List<Expr>>(0);
foreach (var keyValue in TheAssert.NumberedMetaData)
{
// do something
}
Debug.Assert(TheAssert.NumberedMetaDataCount == 1);
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
codexpr in InjectPostConditions
|
| | | |
|
| | | |
|
| | |\
| |/
|/| |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
(vcsCores).
|
| | |
| |
| |
| | |
true but A.GetHashCode() == B.GetHashCode() return false.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
BinderExpr was doing:
object.Equals(this.TypeParameters, other.TypeParameters)
&& object.Equals(this.Dummies, other.Dummies)
Both of these are wrong because these are of type List<> and so
- object.Equals(this.TypeParamters, other.TypeParameters) will call this.TypeParameters.Equals(other.TypeParamters) (assuming they aren't references to the same list)
- object.Equals(this.Dummies, other.TypeParameters) will call this.TypeParameters.Equals(other.Dummies) (assuming they aren't references to the same list)
so this is becomes a reference comparision on Lists<>. This is wrong
because Equals() has been overloaded to implement structural equality.
This affects the classes ForallExpr, LambdaExpr and ExistsExpr.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | | |
|
| |/ / |
|
| | | |
|
| | |
| |
| |
| | |
the StdDispatch method was missing on both Classes.
|
| |/ |
|
| | |
|
| |
|
|
| |
quadratic space complexity
|
| |\ |
|
| | |
| |
| |
| | |
linear_in, linear_out
|
| |/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| | |
|
| |\ |
|
| | | |
|
| | | |
|
| |/ |
|
| |
|
|
|
| |
added another test in linear (based on bug reported by Chris)
removed the QED build configuration
|
| | |
|
| |
|
|
| |
computing statement checksums).
|
| | |
|
| | |
|
| | |
|
| | |
|
wuestholz
Dan Liew
Dan Rosén