| Commit message (Collapse) | Author | Age |
... | |
| | |
|
|\ \ |
|
| | | |
|
| | | |
|
|/ / |
|
| | |
|
| | |
|
| | |
|
|\ \ |
|
| | |
| | |
| | |
| | | |
Patch by Jeroen Ketema
|
| | |
| | |
| | |
| | | |
Patch by Jeroen Ketema
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The Model parser for SMT models is broken beyond repair
and this by-passes this. The code could be moved to the
model parser, but that's a refactoring for another day.
Also, the existing version already had multiple reparses
going on and this at least removes one of those.
Patch by Jeroen Ketema.
|
| | | |
|
| | | |
|
|/ / |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
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.
|