1 Known Bugs
- Defining a message where the beginning of the message part
may contain something that looks like a formula may result in a
syntax error. For example,
%message !(E(v) pvar(v)) ® pvar + " is possibly
NULL..." results in a syntax error. A workaround for this is
inserting "" after the
implication sign. For example,
%message !(E(v) pvar(v)) ® "" + pvar + " is
possibly NULL..." solves the problem.
- Since the TVLA parser does its job in one-pass predicates need to be
declared before they are used, e.g., when
writing a nested foreach block
containing predicate declarations with associated constraints TVLA may claim
that the predicate was used but not declared. The workaround in this case is
to separate the loop into two loops - the first for the predicates
declarations and the second
for the constraints definition.
- The Focus algorithm doesn't handle embedding.
It is desired that the Focus algorithm remove structures when
there are other structures, which embed them. (This is called the
max operation in the parametric framework
article). Using the -j2 option may help to reduce this problem.
2 Bug History
- 17/11/2001 A bug that caused Focus not to terminate when an
unbound binary predicate formula is specified and the structure
contains a summary node connected with an indefinite node (of the
specified predicate). This caused Focus to continue bifurcating
nodes and discovering new indefinite nodes over and over again.
The revised Focus algorithm detects such conditions and aborts the
However, if -quiet is specified Focus recovers by not bifurcating
any given summary node more than once. This is done by considering
only the satisfying assignments of the input structure, such that,
if a node is bifurcated then the new indefinite edges are not
considered. One consequence of this is that in these situations
Focus terminates, but the specified formula will not necessarily
evaluate to a definite value.
- 1/8/2001 A bug in automatic constraint generation for instrumentation predicates.
On certain inputs, such as is[sel,other](v) = E(v1,v2)
(sel(v1,v) & other(v2,v)) the closure operator
generates constraints with a mismatch between the free variables
of the head and the free variables of the body and throws an
exception. This is only a sanity check and does not necessarily
indicates an error in the definition. This information is now
revealed to the user only in debug mode (-d).
- 14/7/2001 A bug in debug mode output.
The first coerce stage did not print its result (running TVLA with
the -d option).
- 6/5/2001 A bug when focus reaches an indefinite edge between
two summary nodes - an exception is thrown (Focus cannot continue
working on this edge, since this will result in an infinite number
After the fix, a warning message is output and if afterwards a
similar case is encountered (almost always) no more messages are
printed on this subject.
- 6/5/2001 A bug in the Focus algorithm in Single mode.
Focusing on binary function predicates with definite edges
pointing to maybe-active nodes resulted in structures without the
- 6/5/2001 Nullary predicates were not abstraction predicates by default.
- 19/4/2001 A bug in the treatment of update formulae.
In cases where variables on the left-hand side of the formula
don't appear on the right-hand side as well.
- 31/12/2000 abs/nonabs was ignored for nullary
This document was translated from LATEX by