Commercial users with current maintenance contracts will be notified
immediately whenever a 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.
| Ref. |
Class |
Category |
Description |
| 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. |
| 538 |
B |
Verification |
If a 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 uninitialised variable is redundant. |
| 585 |
B |
Runtime |
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. |
| 593 |
A |
Verification |
Within a 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 |
| 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 assigned" according to the C# or Java rules,
because Perfect requires only the weaker condition that all variables are
assigned before use. The result is an error message when the Java is
compiled. Workaround: add a dummy initialisation of the variable
concerned. |
| 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. |
| 635 |
B |
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 |
| 644 |
B |
Compiler |
The precondition of a 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. |
| 649 |
A |
Code generation
(C# and Java only) |
When generating C# or Java for a 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 |
| 666 |
B |
Compiler |
The compiler does not permit explicit use of the type 'from anything'
due to memory management issues when generating C++. |
| 687 |
C |
Runtime |
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. |
| 796 |
B |
Compiler |
The compiler does not correctly process require-parts of 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. |
| 804 |
A |
Verification |
The system does not check for illegal direct recursion. An example would
be a method precondition that contains a call to the method. |
| 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). |
| 890 |
A |
Verification |
The prover assumes that unbounded integers can be stored and
manipulated by the generated code. 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. |
| 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 orignal values before they are changed. |
| 1136 |
A |
Verification |
The verifier uses rules for idealised real numbers, but the code generator maps reals to standard floating-point types.
Therefore verification is unsound with respect to the generated code when reals are used. |
| 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 specifications that use reals. |
| 1138 |
A |
Verification |
In 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.
|
| 1139 |
A |
Code generation (C++ only) |
If a 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. |
| 1185 |
B |
Code generation |
The generated code uses the ASCII character set, therefore Unicode characters that are not also
ASCII characters cannot be used in character and string literals. |
| 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. |
| 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. |
| 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. |
TOP
