| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
namespaces remain the same.
|
| |
|
|
|
|
| |
this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
- moved doomed and predication code into separate projects;
for doomed there is a static dependency from BoogieDriver
but for predication even that dependency has been eliminated
- deleted Provers\Simplify and Provers\Z3
- removed Provers\Z3api from the solution
- consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs
|
| |
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This predication algorithm is intended to reduce the complexity
of predicated verification conditions by reducing the amount of
predicated state and using only boolean algebra, as opposed to the
previous algorithm which also uses integers.
It assigns a unique predicate to every superblock, which is defined
per Agrawal [1] except that superblocks are further partitioned
such that either no element of the same superblock may be contained
within a natural loop or each element of the superblock has the same
innermost natural loop head. Predicates are assigned at the element
of the superblock which dominates all others, and are reset to false
at a loop head and at the start of a procedure in order to ensure
correct execution for future iterations. When exiting a loop, all
predicates corresponding to heads of exited loops are reset to false.
The algorithm requires that every successor at every divergence
point in the CFG contains assumes marked with an attribute (called
':partition') which a frontend uses to certify to the predicator
that for each block, if each successor of that block contains an
assume statement marked with :partition, exactly one of those assume
statement's predicates will hold. The frontend we use for GPUVerify
generates such attributes, and as such the new predicator is only
used there, and the old predicator has been retained for Corral etc.
[1] Hiralal Agrawal. Dominators, super blocks, and program coverage.
In POPL '94, p25-34.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration.
|
| |
|
|
| |
Select 4.0 client profile on all projects
|
| |
|
|
|
|
| |
files generated by Coco/R.
This was done to support sharing of the Coco/R .frame files with Spec#.
|
| | |
|
| |
|
|
| |
Removed references to Microsoft.Contracts.dll everywhere since that is available in .NET Framework 4.0.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
only this target has a compile time dependency on Microsoft.Z3.dll.
To compile this target, a reference to z3api must be manually added to BoogieDriver.
|
| |
|
|
| |
project in the Boogie solution references. Dafny.csproj has an internal copy of cce, so does not reference this project, because the Dafny cce uses some Dafny-defined types in its helper methods.
|
| |
|
|
| |
Z3api.csproj shouldn't get in the way this time 'round.
|
| |
|
|
| |
files, to ease between-project conflict. Will trim these back off after commit of Basetypes port in ~20 min.
|
| |
|
|
| |
Core to jive with recent changes made to the cce class.
|
| | |
|
| | |
|
| |
|
|
| |
the version information.
|
| |
|
|
| |
version
|
|
|
ported C# version
|
akashlal
Dan Liew
Ally Donaldson
pantazis
Ken McMillan
Unknown
Unknown
Peter Collingbourne