| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Expose information about the predicate assigned to the immediate dominator of a CFG node.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
otherwise if either of the following happens
* if the solver hangs and we do CTRL+C
* if Boogie crashes
then some lines will be missing from the log.
|
| |
|
|
|
|
| |
where setting produce-unsat-cores to true has no effect unless the option is set last.
This makes the Test/houdini/testUnsatCore.bpl test pass under Linux using Z3 4.3.2
|
| |
|
|
|
| |
negative numbers. I have decided that this method will floor towards
negative infinity rather than zero to match SMT-LIBv2's to_int function.
|
| |
|
|
| |
DoModSetAnalysis needs to run before the linear and mover type checking.
|
| | |
|
| |
|
|
|
| |
taken from ``bv_decl_plugin::get_op_names(...)`` in
``src/ast/bv_decl_plugin.cpp`` in the Z3 4.3.2 source code.
|
| |
|
|
|
|
|
| |
taken
from `` arith_decl_plugin::get_op_names(...)`` from ``src/ast/arith_decl_plugin.cpp``
in the Z3 4.3.2 source code.
|
| |
|
|
|
| |
from ``float_decl_plugin::get_op_names(..)`` in ``src/ast/float_decl_plugin.cpp``
from the Z3 4.3.2 source code.
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
when generating the VC.
|
| | | |
|
| |/ |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
anything that implements the IAppliable interface. Type checking
should never need to change the reference of a list of arguments
(hence the removal of the ``ref`` keyword) and we need to use IList<Expr>
instead of List<Expr> to allow NAryExpr to do its type checking.
|
| |
|
|
| |
even if the types are equivalent.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Made changing the reference throw an exception if the NAryExpr was
constructed as immutable
* Changed the type of NAryExpr.Args to be IList<Expr> rather than
List<Expr> so that when the NAryExpr is immutable I can return
``_Args.AsReadOnly()`` (instead of ``_Args``) which returns a read
only wrapper around the List<Expr> so that clients cannot change the
list.
I came across two problems
* Making this change required changing types all over the place (from
List<Expr> to IList<Expr>). I feel that changes are extensive enough
that there's a good chance that out of tree clients using Boogie's
libraries might break. I've waited for a code review but this didn't
happen so I'm committing anyway.
* I came across something that looks like bad design of the IAppliable
interface which potentially breaks immutability enforcement. I've left
this as a "FIXME" in this. Here's the problematic method.
```
Type Typecheck(ref List<Expr>/*!*/ args, out
TypeParamInstantiation/*!*/ tpInstantiation, TypecheckingContext/*!*/
tc);
```
It potentially allows the instance of the args to be changed which
seems very suspect.
|
| | |
|
| |
|
|
|
|
| |
If constructing immutable Expr bottom up this would be very inefficient
because the hashcode would be recomputed unnecessarily. Now just make
ComputeHashCode() methods call GetHashCode() on Expr instead.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
<bool> == <bool>
or
<bool> != <bool>
The type checker tries rewrite the Expr when it gets type checked
which breaks immutability so disable doing this if the Expr is
immutable.
|
| |
|
|
| |
assumption variables.
|
| | |
|
| |
|
|
|
|
| |
Compilation does not depend NUnit.Runners so it should not be
a required package. Instead users should install it manually as
described in Source/UnitTests/README.md
|
| |
|
|
|
|
| |
attempt to unbreak the Jenkins build. I don't think doing this
is ideal. The package isn't required to run tests, it's only required
if you want to run them on the command line.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
out we had the repository set up in "MSBuild-Integrated package" mode[1]
(missing packages won't fetched unless the user explicitly allows it for the
solution) but what we want is "Automatic package restore" (provided NuGet is
setup correctly automatically fetch the missing packages). I've followed the
migration guide [2] and it appears that now Visual Studio will try to
automatically fetch after making this change.
[1] http://docs.nuget.org/consume/package-restore
[2] http://docs.nuget.org/Consume/Package-Restore/Migrating-to-Automatic-Package-Restore
|
| | |
|
| | |
|
| |
|
|
| |
for BvExtractExpr, BvConcatExpr and OldExpr.
|
| |
|
|
| |
for LiteralExpr, IdentifierExpr and NAryExpr.
|
| |
|
|
| |
are immutable. Add unit tests to check this.
|
| |
|
|
| |
to set them as immutable (not currently enforced for these Expr types).
|
| |
|
|
|
| |
Add a unit test for this. We need to protect the Args field too
but that is going to be much harder to enforce.
|
| |
|
|
| |
to check this is being enforced.
|
| |
|
|
|
|
|
| |
For IdentifierExpr and the Type field of Expr.
There are lots of places where it still isn't enforced but hopefully
we'll fix those in due time.
|
| |
|
|
|
|
| |
has never been type checked we allow the Type field to be set but
once it has been set it cannot be changed to refer to a different
Type.
|
| |
|
|
|
| |
immutable by raising an exception if an attempt is made to modify it
after construction.
|
| |
|
|
|
|
|
| |
for doing this is that we would like a LiteralExpr to be immutable
when constructed but because the "Val" field can point to a BvConst
which is an object it means that although the Val reference cannot
change the BvConst could be changed.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
This is currently not enforced (it really should be). So right now it
only amounts to a promise by the client that the Expr will not be modified
after it is constructed. We should actually enforce this by protecting
various fields of the Expr classes so they can't be changed if an Expr
is constructed as Immutable.
The motivation for doing this is it allows the value of GetHashCode()
to be cached. Expr classes now implement ComputeHashCode() to do the
actuall hash code computation.
|
Dan Liew
qadeer
akashlal