| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Drop the “basic” block predication algorithm. Block predication is only used
by GPUVerify, and then only in the “smart” version as the basic algorithm does
not perform very well. As a consequence this code is essentially dead.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
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.
|
akashlal
qadeer
Dan Liew
akashlal