Known Operational Issues
Known issues concerning the installation of Escher Verification Studio are
listed separately - see here.
Issue Classification Scheme
Operational issues with Escher Verification Studio are classified as follows:
| Class |
Meaning |
| A |
The issue could give rise to a scenario whereby Perfect Developer
claims that a source file is fully validated and generates code in the
target language that is accepted by a 'reasonable' compiler, but the generated
code does not accord with the Perfect specification; or Escher C Verifier
claims that a source file is fully validated but the code could fail to behave as specified.
An issue in this
class might concern the Perfect Developer code generator producing legal but incorrect or
ambiguous code, or the theorem prover generating erroneous proofs, or verification conditions not
being generated when needed, or a serious flaw in the Perfect Developer runtime library. |
| B |
The issue does not meet the requirements of class A but does seriously
impede developer productivity. An issue in this class might concern the Perfect Developer code
generator producing code that will not compile, or either Perfect Developer
or Escher C Verifier failing to process a legal source file. |
| C |
The issue does not meet the requirements of class A, and we believe that it is rarely
encountered or easily worked around, so it does not merit classification as
class B. |
Commercial users with current maintenance contracts will be notified
immediately whenever a new category A issue is confirmed.
Generally, only category A and B issues will be listed here. Category C
issues will be listed where they potentially affect a large number of users.
Known issues with Escher Verification Studio 6.00.03 and earlier
| Ref. |
Class |
Category |
Description |
| 1322 |
A |
Verification |
Escher C Verifier fails to detect instances of out-parameters not being initialized by the called function,
or being used inside the called function before they are initialized. |
| 1288 |
A |
Verification |
Escher C Verifier does not detect instances of reading or writing through pointers that point to objects that have gone out of scope. |
| 1186 |
B |
Compiler |
The compiler assumes that the input file is ASCII and fails to interpret UTF-8, UTF-16 and UTF-32 files correctly. |
| 1185 |
B |
Code generation |
The code generated by Perfect Developer uses the ASCII character set,
therefore Unicode characters that are not also
ASCII characters cannot be used in character and string literals. |
| 1139 |
A |
Code generation (C++ only) |
If a Perfect specification uses ref types and causes circular chains of references to be created, the reference-counting garbage collection
in the generated C++ code will not collect the associated storage when such a chain becomes inaccessible, unless the chain is broken first. |
| 1138 |
A |
Verification |
In Perfect specifications that use ref types, it is possible that a heap object A of some type T may directly or indirectly hold a reference to
another object of B also of type T. When S calls members of object B via the reference, it will be assumed that the invariant of B holds.
However, if B is the same object as A (i.e. there is a circular chain of references), that may not be true.
|
| 1137 |
A |
Verification |
The verifier folds constant expressions involving reals using floating-point arithmetic.
Due to rounding errors, this may lead to incorrect verification of Perfect specifications that use reals,
or of eCv programs that use floats or doubles. |
| 1136 |
A |
Verification |
The verifier uses rules for idealized real numbers, but the Perfect Developer code generator maps reals
to standard floating-point types.
Similarly, float and double values in C/C++ code are modelled as idealized real numbers by eCv.
Therefore verification is unsound when floating-point arithmetic is used. |
| 1074 |
A |
Code generation |
If a 'forall' postcondition modifies individual elements of a sequence, and the new value depends on earlier elements of the
same sequence, the code generator fails to capture the original values before they are changed. |
| 890 |
A |
Verification |
The prover assumes that unbounded integers can be stored and
manipulated by code generated from Perfect Developer.
No allowance is currently made for the fact that the code
generator and run-time library map Perfect integers to bounded
integers in the target language. |
| 805 |
A |
Verification |
The system does not detect indirect recursion whether illegal (e.g. a
recursive precondition) or legal (in which case appropriate variants must be
declared and the corresponding proof obligations generated). |
| 804 |
A |
Verification |
The system does not check for some types of illegal direct recursion. An example would
be a method precondition that contains a call to the method. |
| 796 |
B |
Compiler |
The compiler does not correctly process require-parts of Perfect templates that
declare a requirement for a constructor of a template parameter; instead it
generates a warning that the feature is unimplemented and the requirement
will be ignored. |
| 687 |
C |
Runtime library |
If the system runs out of memory while deserializing data (e.g. because
the file is corrupt but the corruption has not been detected, or because
more memory was available when the data was serialized), instead of
returning failure from the deserialization call, the program is terminated. |
| 666 |
B |
Compiler |
The compiler does not permit explicit use of the Perfect type 'from anything'
due to memory management issues when generating C++. |
| 649 |
A |
Code generation
(C# and Java only) |
When generating C# or Java code for a Perfect schema that modifies self, it is
possible for aliasing to occur between self and a variable that has
been copied from an earlier instance of self. Example: class
A ^=
abstract
var v: int;
interface
// The following schema will result in v having a final value of 1
instead of being the same as the initial value
schema !buggy post (let temp ^= self; v! = 1
then v! = temp.v);
end |
| 644 |
B |
Compiler |
The precondition of a Perfect method declared early should not be allowed
to refer to other non-early methods of the same class. However, if the
method is declared as a define or redefine of an inherited
method and the precondition is inherited, no checks are made. |
| 635 |
B |
Runtime library |
The 'normalizeFile(..)' function sometimes produces incorrect results
for invalid arguments, as follows:
Input:
argument#1 (default path) = '\\MONSTER\!PublicReadOnly\'
argument#2 (filename) = '..\Temp\Win32InstallWorkaround.txt'
Output:
path = '\\MONSTER\!PublicReadOnly\Temp\'
file='Win32InstallWorkaround.txt'
Correct output should be:
<ERROR> because an attempt has been made to go down a level from level 0
(the UNC descriptor '\\MONSTER\!PublicReadOnly' is the root)
Input:
argument#1 (default path) = '\'
argument#2 (filename) ='..\Temp\Win32InstallWorkaround.txt'
Output:
path = 'C:\Temp\'
file = 'Win32InstallWorkaround.txt'
Correct output should be:
<ERROR> because an attempt has been made to go down a level from level 0
Input:
argument#1 (default path) = 'C:\'
argument#2 (filename) = '..\Temp\Win32InstallWorkaround.txt'
Output:
path = 'C:\Temp\'
file = 'Win32InstallWorkaround.txt'
Correct output should be:
<ERROR> because an attempt has been made to go down a level from level 0
Input:
argument #1: '::\'
argument #2: ''
Output:
path: '::\'
file: ''
Correct output should be:
<ERROR> because this is not a valid filename |
| 629 |
B |
Code generation
(C# and Java only) |
If the expression following inherits in a constructor declaration
is not a constructor call, the generated C# or Java code will not compile unless a
"copy" constructor has been declared in the parent class. Workaround:
declare a copy constructor in the parent class. |
| 625 |
C |
Code generation
(C# and Java only) |
C# or Java code generated by Perfect Developer sometimes fails to ensure that
local variables are "definitely initialized" according to the C# or Java rules,
because Perfect requires only the weaker condition that all variables are
initialized before use. The result is an error message when the Java is
compiled. Workaround: add a dummy initialisation of the variable
concerned. |
| 593 |
A |
Verification |
Within a Perfect constructor implementation, no check is made that we do not use
members of self before they are initialised. It is possible to
construct an example that will pass validation but fail at runtime. Example:
class A ^=
abstract
var v: B; // class B is assumed to have a member
called f
interface
build{x: B} post change v satisfy v'.f = x.f
via ([v.f = x.f]: pass, []: v'= x)
end;
end |
| 585 |
B |
Runtime library |
When deserializing data of an enumeration type, no check is made that
the value read is in range. This could lead to a problem if an old version
of a program is reading data written by a new version in which an
enumeration has been extended and the developer omitted to increment the
serialization version. |
| 538 |
B |
Verification |
If a Perfect loop statement declares local variables, the system fails to ensure
they their values are not used before they are initialized. However, the
implementation would normally fail to validate, unless the code that uses
the uninitialized variable is redundant. |
| 485 |
B |
Verification |
The prover will sometimes assume that an object of some class declared
by the user can be constructed (e.g. "exists x: T :- true"
will be assumed). If this is not the case (for example, if the class has an
invariant that can never be satisfied), this is not true. However, in this
case the prover should fail to validate the constructors for the
class. |
Known issues with Escher Verification Studio 5.10 and earlier that were fixed in Escher Verification Studio 6.0.03
| Ref. |
Class |
Category |
Description |
| 1338 |
A |
Verification |
Where the theorem prover had an equality between a those-expression and an empty set or bag, and this equality was inside a quantifier,
then the theorem prover could make incorrect inferences, leading to invalid proofs. |
| 1332 |
A |
Code generation (C# only) |
if a schema had an out-parameter whose type was a regular class, then of the schema assigned a value to the parameter and subsequently
called a member schema on it, the current value was not cloned. This led to incorrect modification of the value it was assigned from. |
Known issues with Escher Verification Studio 5.0 and earlier that were fixed in Escher Verification Studio 5.10
| Ref. |
Class |
Category |
Description |
| 1327 |
A |
Verification |
When a function parameter is an array for which a bound is declared (as is required for all but the first bound of a multi-dimensional array),
eCv failed to generate a verification condition or static check at the site of a call to that function that the bound of the
actual array conforms to the bound declared in the parameter. |
Known issues with Perfect Developer 4.10.02 and earlier that were fixed in Escher Verification Studio 5.0
| Ref. |
Class |
Category |
Description |
| 1294 |
A |
Verification |
If a Perfect schema was expanded multiple times by the theorem prover, and the schemas postcondition contained at least one
variable declaration, then the values of variables in the different expansions sometimes got mixed up. This could result in invalid proofs. |
| 1258 |
A |
Code generation |
If a value of a primitive type or small class type was converted into a union in a context in which a pointer was required (for example,
to pass as a function parameter), then the reference count was not set correctly. This typically resulted in a small memory leak, but
could lead to incorrect execution. |
| 1254 |
A |
Verification |
If a base class declares operator ~~ but a class derived from it does not, then the theorem prover considered that all objects of the
derived class compare same because it did not take account of the declaration of operator~~ in the base class. |
| 1249 |
A |
Verification |
The theorem prover could generate incorrect results when evaluating the % (modulus) operator between two integer operands
when the first one was negative. |
| 1245 |
A |
Verification |
A small number of prover rules that involve instantiating bound variables have incorrect quantifier depths on the right hand side,
because the mechanism used to detect inconsistencies in quantifier depths did not function for those rules.
Where a term contains nested bound variable declarations, this can lead to use of the incorrect bound variable after the rule is applied.
Typically, this leads to failed proofs or to prover termination due to type inconsistency; however it might be that
it could also lead to false proofs. |
| 1231 |
A |
Verification |
When proving that the predicate of an exists-expression over a collection is well-formed, the prover rightly assumes the current
element is in the collection, and may infer that the collection is not empty. However, this inference may get exported to the surrounding
context, which may lead the prover to incorrectly infer that the collection is not empty when trying to prove that the exists-expression
is true, leading to a false proof. |
| 1228 |
A |
Verification |
Where a specification computed "+ over" a set or bag of integers or reals, the theorem prover might make incorrect inferences in the
special case of the set or bag being empty. |
Known issues with Perfect Developer 4.0 and earlier that were fixed in 4.10.02
| Ref. |
Class |
Category |
Description |
| 1203 |
A |
Verification |
When accessing a guarded data member, a verification condition is generated that the guard is true.
However, any other verification conditions needed to ensure that the variable as a whole can be evaluated were discarded. |
| 1180 |
A |
Verification |
The verification conditions generated for the second and subsequent guarded expressions of an opaque conditional expression
incorrectly assumed that the previous guards were false, as if the conditional was not declared opaque. |
| 1160 |
A |
Verification |
When the prover applied rule "expand literal those" or rule "expand literal for..those..yield", and proof output was disabled, then it
incorrectly discarded some branch dependencies of rules used. This might lead to invalid proofs in some circumstances. |
Last updated 17 February 2013.
|
TOP
