| Rule |
Req/Adv |
Comp |
Notes |
| 0-1-1 |
R |
P |
Although
the code generated by PD is generally compliant, PD generates standard
member functions (e.g. equality and comparison operators) that may be
unreachable in the project as a whole. They are not unreachable in a
unit testing environment. Unreachable code in the Perfect source is
usually (but not always) detected during verification. |
| 0-1-2 |
R |
Y |
Provided
that run-time checks are disabled. If run-time checks are enabled, the
the path corresponding to the failure of a run-time check may be
infeasible (and should be infeasible if the project has passed
verification by PD). |
| 0-1-3 |
R |
Y |
Provided that no unused variables are declared
in the Perfect source. |
| 0-1-4 |
R |
Y |
Provided that no variables used only once are
declared in the Perfect source. |
| 0-1-5 |
R |
Y |
Provided that no unused classes are declared in
the Perfect source. |
| 0-1-6 |
R |
Y |
Provided that no variables or let-declarations
whose values are not subsequently used are declared in the Perfect
source. |
| 0-1-7 |
R |
Y |
|
| 0-1-8 |
R |
Y |
Provided
that no schemas having no side effects are declared in the Perfect
source. Note that it is legitimate in object-oriented software
development to declare a set of overloaded methods that have
side-effects in some classes but not in others. |
| 0-1-9 |
R |
Y |
Provided there is no dead code or dead parts of
the specification in the Perfect source. |
| 0-1-10 |
R |
Y |
Provided that every function or schema declared
in the Perfect source is called at least once. |
| 0-1-11 |
R |
Y |
Provided there are no global or nonmember
functions or schemas with unused parameters in the Perfect source. |
| 0-1-12 |
R |
Y |
Provided there are no sets of overloaded member
functions or schemas at have parameters that are never used in the Perfect source. |
| 0-2-1 |
R |
Y |
|
| 0-3-1 |
D |
Y |
The code
generator is designed such that if full verification of the Perfect
source is achieved, there shall be no run-time failures, other than
failure to allocate memory. |
| 0-3-2 |
R |
Y |
Provided then when a function returning an error
value is called in the Perfect source, that value is tested. |
| 0-4-1 |
D |
n/a |
|
| 0-4-2 |
D |
n/a |
|
| 0-4-3 |
D |
n/a |
|
| 1-0-1 |
R |
Y |
|
| 1-0-2 |
D |
n/a |
|
| 1-0-3 |
D |
n/a |
The code generated by PD is independent of the
implementation of integer division by the chosen compiler. |
| 2-2-1 |
D |
n/a |
|
| 2-3-1 |
R |
Y |
|
| 2-5-1 |
A |
Y |
|
| 2-7-1 |
R |
Y |
|
| 2-7-2 |
R |
Y |
|
| 2-7-3 |
A |
Y |
|
| 2-10-1 |
R |
Y |
Provided they are typographically unambiguous in
the Perfect source. |
| 2-10-2 |
R |
Y |
|
| 2-10-3 |
R |
Y |
|
| 2-10-4 |
R |
Y |
|
| 2-10-5 |
A |
Y |
|
| 2-10-6 |
R |
Y |
|
| 2-13-1 |
R |
Y |
|
| 2-13-2 |
R |
Y |
|
| 2-13-3 |
R |
Y |
PD does not generate unsigned literals. |
| 2-13-4 |
R |
Y |
|
| 2-13-5 |
R |
Y |
|
| 3-1-1 |
R |
Y |
|
| 3-1-2 |
R |
Y |
|
| 3-1-3 |
R |
Y |
Arrays are used only in the run-time library. |
| 3-2-1 |
R |
Y |
|
| 3-2-2 |
R |
Y |
|
| 3-2-3 |
R |
Y |
|
| 3-2-4 |
R |
Y |
|
| 3-3-1 |
R |
Y |
|
| 3-3-2 |
R |
Y |
PD does not generate functions with internal
linkage. |
| 3-4-1 |
R |
Y |
Provided that identifiers in the Perfect source
are declared so as to minimize their visibilities. |
| 3-9-1 |
R |
Y |
|
| 3-9-2 |
A |
Y |
The generated code uses only one length of
integral type, and this is defined by a typedef. |
| 3-9-3 |
R |
Y |
|
| 4-5-1 |
R |
Y |
|
| 4-5-2 |
R |
Y |
|
| 4-5-3 |
R |
P |
Perfect
allows character operands to be compared using the
relational operators. If this is done in the Perfect source,
corresponding comparison operations will appear in the generated code. |
| 4-10-1 |
R |
Y |
|
| 4-10-2 |
R |
Y |
static_cast<T*>(0)
is used as the null pointer constant for type T*.
|
| 5-0-1 |
R |
Y |
|
| 5-0-2 |
A |
N |
The rationale given for this rule is not
relevant to generated code. |
| 5-0-3 |
R |
Y |
|
| 5-0-4 |
R |
Y |
|
| 5-0-5 |
R |
Y |
|
| 5-0-6 |
R |
Y |
|
| 5-0-7 |
R |
Y |
|
| 5-0-8 |
R |
Y |
|
| 5-0-9 |
R |
Y |
|
| 5-0-10 |
R |
Y |
|
| 5-0-11 |
R |
Y |
PD does not use plain char. |
| 5-0-12 |
R |
P |
Compliant if wide characters are being used to
represent character data in the generated code. Otherwise, PD uses signed
char
to represent character data, in order to avoid dependence on whether
the compiler used to compile the generated code treats plain char
values as signed or unsigned. PD uses unsigned char
to represent type byte. PD does not used signed
char to represent numeric data. |
| 5-0-13 |
R |
Y |
|
| 5-0-14 |
R |
Y |
|
| 5-0-15 |
R |
Y |
|
| 5-0-16 |
R |
Y |
PD does not use this construct. |
| 5-0-17 |
R |
Y |
PD does not use this construct. |
| 5-0-18 |
R |
Y |
PD does not use this construct. |
| 5-0-19 |
R |
Y |
|
| 5-0-20 |
R |
Y |
|
| 5-0-21 |
R |
Y |
|
| 5-2-1 |
R |
N |
The rationale given for this rule is not
relevant to generated code. |
| 5-2-2 |
R |
Y |
PD does not use virtual base classes. |
| 5-2-3 |
A |
Y |
Provided that the Perfect source contains no
is-casts from type from B to type D
or from type from B to type from D,
where D is derived from B. |
| 5-2-4 |
R |
Y |
|
| 5-2-5 |
R |
Y |
|
| 5-2-6 |
R |
Y |
|
| 5-2-7 |
R |
Y |
|
| 5-2-8 |
R |
Y |
Except that PD uses static_cast<Y>(0)
to express a null pointer of type T*. It is not clear whether the
MISRA rules regard literal 0 as "an object of
integral
type". |
| 5-2-9 |
A |
Y |
|
| 5-2-10 |
A |
Y |
|
| 5-2-11 |
R |
Y |
|
| 5-2-12 |
R |
Y |
|
| 5-3-1 |
R |
Y |
|
| 5-3-2 |
R |
Y |
|
| 5-3-3 |
R |
Y |
|
| 5-3-4 |
R |
Y |
|
| 5-8-1 |
R |
Y |
|
| 5-14-1 |
R |
Y |
|
| 5-17-1 |
R |
Y |
|
| 5-18-1 |
R |
Y |
Provided that run-time checks are not being
generated. |
| 5-19-1 |
A |
Y |
|
| 6-2-1 |
R |
Y |
|
| 6-2-2 |
R |
Y |
Provided that expressions of type real
are not compared for equality or inequality in the Perfect source. |
| 6-2-3 |
R |
Y |
|
| 6-3-1 |
R |
Y |
|
| 6-4-1 |
R |
Y |
|
| 6-4-2 |
R |
N |
We do not consider this rule relevant
to code generated from verified Perfect source. |
| 6-4-3 |
R |
Y |
|
| 6-4-4 |
R |
Y |
|
| 6-4-5 |
R |
Y |
|
| 6-4-6 |
R |
N |
We do not consider this rule relevant
to code generated from verified Perfect source. |
| 6-4-7 |
R |
Y |
|
| 6-4-8 |
R |
Y |
|
| 6-5-1 |
R |
Y |
|
| 6-5-2 |
R |
Y |
|
| 6-5-3 |
R |
Y |
|
| 6-5-4 |
R |
Y |
|
| 6-5-5 |
R |
Y |
|
| 6-5-6 |
R |
Y |
|
| 6-6-1 |
R |
Y |
|
| 6-6-2 |
R |
Y |
|
| 6-6-3 |
R |
Y |
|
| 6-6-4 |
R |
N |
There may sometimes be more than one break
statement in a single loop, in particular within for(;;)
loops. |
| 6-6-5 |
R |
Y |
Provided that the user does not use value
or done statements in implementations. |
| 7-1-1 |
R |
N |
This may be changed in a future version of the
code generator. |
| 7-1-2 |
R |
Y |
|
| 7-2-1 |
R |
Y |
|
| 7-3-1 |
R |
Y |
Provided that a namespace is
specified in the Code Generation settings.
|
| 7-3-2 |
R |
Y |
|
| 7-3-3 |
R |
Y |
|
| 7-3-4 |
R |
N |
The generated code will
contain a using-declaration for the current namespace.
|
| 7-3-6 |
R |
? |
|
| 7-4-1 |
D |
Y |
PD does not generate assembler.
|
| 7-4-2 |
R |
Y |
PD does not generate assembler. |
| 7-4-3 |
R |
Y |
PD does not generate assembler. |
| 7-5-1 |
R |
Y |
|
| 7-5-2 |
R |
Y |
|
| 7-5-3 |
R |
Y |
|
| 7-5-4 |
A |
Y |
Provided that the only recursive functions in the
Perfect source are functions with a recursive specification and an
explicit non-recursive refinement, and/or recursive ghost functions.
|
| 8-0-1 |
R |
Y |
|
| 8-3-1 |
R |
Y |
PD does not generate default arguments.
|
| 8-4-1 |
R |
Y |
|
| 8-4-2 |
R |
Y |
Provided that consistent identifiers
are used when overloading functions in the Perfect source
|
| 8-4-3 |
R |
Y |
|
| 8-4-4 |
R |
Y |
|
| 8-5-1 |
R |
Y |
Provided that the Perfect source has passed
verification.
|
| 8-5-2 |
R |
Y |
|
| 8-5-3 |
R |
Y |
|
| 9-3-1 |
R |
Y |
|
| 9-3-2 |
R |
Y |
|
| 9-3-3 |
R |
P |
PD will automatically declare member functions const
where possible. However, if a function or schema that does not directly
or indirectly refer to self is declared in the
Perfect source, the corresponding generated member will not
automatically be declared static.
|
| 9-5-1 |
R |
Y |
|
| 9-6-1 |
D |
Y |
PD does not use bit fields.
|
| 9-6-2 |
R |
Y |
PD does not use bit fields. |
| 9-6-3 |
R |
Y |
PD
does not use bit fields. |
| 9-6-4 |
R |
Y |
PD
does not use bit fields. |
| 10-1-1 |
A |
Y |
PD
does not use virtual base classes.
|
| 10-1-2 |
R |
Y |
PD
does not use virtual base classes. |
| 10-1-3 |
R |
Y |
PD
does not use virtual base classes. |
| 10-2-1 |
R |
Y |
|
| 10-3-1 |
R |
Y |
|
| 10-3-2 |
R |
Y |
|
| 10-3-3 |
R |
Y |
|
| 11-0-1 |
R |
N |
Member
variables that are redeclared as functions or selectors in the
confined/interface section will be declared protected/public
respectively.
|
| 12-1-1 |
R |
Y |
|
| 12-1-2 |
A |
Y |
|
| 12-1-3 |
R |
Y |
|
| 12-8-1 |
R |
Y |
Provided
that any copy constructor declared in the Perfect source only
initializes the base class and member variables of its class.
|
| 12-8-2 |
R |
Y |
PD
does not generate copy assignment operators, because the
compiler-generated ones have the correct semantics.
|
| 14-5-1 |
R |
Y |
|
| 14-5-2 |
R |
N |
This
rule is not relevant to code generated by PD because the
compiler-generated copy constructors always have the correct semantics.
|
| 14-5-3 |
R |
Y |
PD
does not generate assignment operators.
|
| 14-6-1 |
R |
Y |
|
| 14-6-2 |
R |
Y |
|
| 14-7-1 |
R |
Y |
Provided
that there are no redundant generic declarations in the Perfect source.
|
| 14-7-2 |
R |
Y |
|
| 14-7-3 |
R |
Y |
PD
does not generate template specializations.
|
| 14-8-1 |
R |
Y |
PD
does not generate template specializations. |
| 14-8-2 |
A |
Y |
PD
does not generate template specializations. |
| 15-0-1 |
D |
Y |
Provided
that the Perfect source uses exceptions only for
error handling.
|
| 15-0-2 |
A |
Y |
|
| 15-0-3 |
R |
Y |
|
| 15-1-1 |
R |
Y |
|
| 15-1-2 |
R |
Y |
|
| 15-1-3 |
R |
Y |
|
| 15-3-1 |
R |
Y |
Unless
an out-of-memory condition occurs during start-up.
|
| 15-3-2 |
A |
n/a |
This
is the responsibility of a hand-coded entry point function
that calls the PD-generated code.
|
| 15-3-3 |
R |
Y |
|
| 15-3-4 |
R |
Y |
Provided
that the Perfect source does not declare entry-point functions that
throw exceptions. |
| 15-3-5 |
R |
Y |
|
| 15-3-6 |
R |
Y |
|
| 15-3-7 |
R |
Y |
|
| 15-4-1 |
R |
Y |
|
| 15-5-1 |
R |
Y |
|
| 15-5-2 |
R |
Y |
|
| 15-5-3 |
R |
Y |
|
| 16-0-1 |
R |
Y |
|
| 16-0-2 |
R |
Y |
|
| 16-0-3 |
R |
N |
There
is one instance of #undef in one runtime library
source (not header) file.
|
| 16-0-4 |
R |
Y |
|
| 16-0-5 |
R |
Y |
|
| 16-0-6 |
R |
Y |
|
| 16-0-7 |
R |
Y |
|
| 16-0-8 |
R |
Y |
|
| 16-1-1 |
R |
Y |
|
| 16-1-2 |
R |
Y |
|
| 16-2-1 |
R |
N |
PD
uses macros to generate some types of boilerplate code.
|
| 16-2-2 |
R |
Y |
PD
uses macros to generate some types of boilerplate code. |
| 16-2-3 |
R |
Y |
|
| 16-2-4 |
R |
Y |
|
| 16-2-5 |
A |
Y |
Provided
that the PD source does not use the "\" character in filenames in import
directives.
|
| 16-2-6 |
R |
Y |
|
| 16-3-1 |
R |
Y |
|
| 16-3-2 |
A |
N |
|
| 16-6-1 |
D |
Y |
PD
does not generate #pragma directives
|
| 17-0-1 |
R |
Y |
|
| 17-0-2 |
R |
Y |
|
| 17-0-3 |
R |
Y |
|
| 17-0-4 |
D |
P |
Compliance
of the runtime library code to MISRA C++ is as indicated by this document.
|
| 17-0-5 |
R |
Y |
|
| 18-0-1 |
R |
Y |
|
| 18-0-2 |
R |
Y |
|
| 18-0-3 |
R |
N |
The
runtime library makes calls to getenv in order to implement
member getEnvironmentVar of class Environment.
|
| 18-0-4 |
R |
N |
The
runtime library makes calls to gmtime(),
timezoneadjust() and clock() in order to
implement time-related member functions of class Environment.
|
| 18-0-5 |
R |
N |
The
runtime library makes calls to some of the string functions in order to
convert string literals to Perfect form. These functions are always
used in a safe manner.
|
| 18-2-1 |
R |
Y |
|
| 18-4-1 |
R |
N |
Dynamic
object creation requires the use of dynamic memory allocation. It may
be possible to avoid dynamic memory allocation after initialization if
constructors are not called and objects are not copied, except
during initialization.
|
| 18-7-1 |
R |
Y |
|
| 19-3-1 |
R |
N |
The
file-related functions of class Environment make use
of errno.
|
| 27-0-1 |
R |
N |
The
file-related functions of class Environment make use
of cstdio.
|