| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
|
| |
This mode also conditionalises if statements to avoid problems with
recursion.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This analysis is used to generate race checking invariants for
arbitrary (thread-level) constant offsets, in place of invariant
generators for four specific constants (thread-id, global-id, 2D
thread-id and 2D global-id) which are subsumed by the new analysis.
The main motivation is to be able to recognise offsets used by
word level accesses into byte arrays, which are formed from linear
combinations of thread IDs and constants.
This change allows us to remove the 2D and global size analyses,
resulting in a 536-line net reduction in total code size.
|
|
|
|
|
|
| |
(e.g. consider a loop within a conditional)
Pointed out by Ally.
|
|
|
|
| |
instead of a conjunction
|
|\ |
|
| |
| |
| |
| | |
for special characters in identifiers
|
|\ \ |
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |\
| | |/
| |/| |
|
| | | |
|
| |\ \
| |/ /
|/| | |
|
| | | |
|
|\| | |
|
| | |
| | |
| | |
| | | |
check the existence of a value. The previous "assume only" version is available by supplying the keyword "assume" in front of "P".
|
| |\ \ |
|
|/ / /
| | |
| | |
| | | |
(i.e. a != b is allowed when a: array<int> and b: array<T>)
|
|/ /
| |
| |
| | |
Thanks to Ally for pointing this out.
|
| | |
|
|\ \ |
|
| | | |
|
| | |
| | |
| | |
| | | |
them (for now, this is supported only in type expressions and "new" allocations, not in places where the type name is used to qualify some other type member)
|
| | | |
|
| | |
| | |
| | |
| | | |
limited)
|
| | | |
|
| | | |
|
| | |
| | |
| | |
| | | |
This allows us to retain invariant tags.
|
| | |
| | |
| | |
| | |
| | | |
This allows us to build candidate invariants in situations where we
don't have a Region, such as the block predicator.
|
| |/
| |
| |
| |
| |
| |
| | |
than in ComputeInvariant
This allows us to emit invariants in places earlier than
ComputeInvariant (such as the block predicator).
|
|\| |
|
| |
| |
| |
| | |
2. changed the block expression to be the negation of the disjunction of all outgoing edges
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| | |
intelligently
Specifically, if the input file's extension is not ".bpl", use
its name (without extension) plus ".bpl" as the output file name.
|
|/ |
|
| |
|
|
|
|
|
| |
also changing back the output path in BoogieDriver
also disabling z3api for now since it does not build
|
|\ |
|
| |
| |
| |
| | |
containing a '$'
|
| |
| |
| |
| | |
for consistency with the structured predicator
|
| |
| |
| |
| | |
This is OK now that we have assume stealing.
|
| |
| |
| |
| |
| |
| | |
Specifically, have the predicator emit backedge assumes with
a :backedge attribute, and have the dualiser recognise such assumes
and create an OR expression instead of an AND expression.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The main goal of this change is to make the candidate invariant
generation code and various analyses capable of handling both
structured and unstructured programs. This is achieved using a
high level abstraction of "regions" -- a region may either be a
"root region" representing the entire implementation, or a natural
loop within that implementation. Note that this is a subset to the
term's meaning in the context of compilers, in which regions are also
used for conditional control flow. Each region consists of a set of
commands and a set of child regions.
This change also has the side effect of eliminating a large amount of
boilerplate code -- its net effect is to reduce the number of lines
of code by 88.
|
| |\ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Should not affect function
of other provers. There is an option added in Check.cs to allow creation
of a Checker with a user-specified ProverContext. Also, some extension of
z3api prover context to support conversion of Z3 formulas back to VCExpr.
Finally, some experimental code, not enabled, to allow conversion of loops to
recursion with "head recursion" rather than "tail recursion" (i.e., recursive
call before loop body rather than after).
|
| | |
| | |
| | |
| | | |
frontend
|