Undecidable MISRA C:2012 Rules and Directives Supported by Polyspace Bug Finder

The MISRA C:2012 standard classifies rules and directives that cannot be statically enforced in every possible cases as Undecidable. Polyspace^® supports 44 out of 51 such rules, and 18 out of 21 such directives.

Undecidable Rules

A rule is undecidable if a static analysis tool can check compliance to it only in certain cases. Polyspace shows the subset of all possible issues. For details about which issues Polyspace detects for a particular rule, see the Polyspace Implementation section in the reference page of the rule. Polyspace supports 44 out of 51 such rules.

MISRA C:2012 Rule	Description	Polyspace Checker
MISRA C:2012 Rule 12.2	The right hand operand of a shift operator shall lie in the range zero to one less than the width in bits of the essential type of the left hand operand	`MISRA C:2012 Rule 12.2`
MISRA C:2012 Rule 13.1	Initializer lists shall not contain persistent side effects	`MISRA C:2012 Rule 13.1`
MISRA C:2012 Rule 13.2	The value of an expression and its persistent side effects shall be the same under all permitted evaluation orders and shall be independent from thread interleaving	`MISRA C:2012 Rule 13.2`
MISRA C:2012 Rule 13.5	The right hand operand of a logical && or \|\| operator shall not contain persistent side effects	`MISRA C:2012 Rule 13.5`
MISRA C:2012 Rule 14.1	A loop counter shall not have essentially floating type	`MISRA C:2012 Rule 14.1`
MISRA C:2012 Rule 14.2	A for loop shall be well-formed	`MISRA C:2012 Rule 14.2`
MISRA C:2012 Rule 14.3	Controlling expressions shall not be invariant	`MISRA C:2012 Rule 14.3`
MISRA C:2012 Rule 17.11	A function that never returns should be declared with a `_Noreturn` function specifier	`MISRA C:2012 Rule 17.11`
MISRA C:2012 Rule 17.2	Functions shall not call themselves, either directly or indirectly	`MISRA C:2012 Rule 17.2`
MISRA C:2012 Rule 17.5	The function argument corresponding to a parameter declared to have an array type shall have an appropriate number of elements	`MISRA C:2012 Rule 17.5`
MISRA C:2012 Rule 17.8	A function parameter should not be modified	`MISRA C:2012 Rule 17.8`
MISRA C:2012 Rule 17.9	A function declared with a `_Noreturn` function specifier shall not return to its caller	`MISRA C:2012 Rule 17.9`
MISRA C:2012 Rule 18.1	A pointer resulting from arithmetic on a pointer operand shall address an element of the same array as that pointer operand	`MISRA C:2012 Rule 18.1`
MISRA C:2012 Rule 18.2	Subtraction between pointers shall only be applied to pointers that address elements of the same array	`MISRA C:2012 Rule 18.2`
MISRA C:2012 Rule 18.3	The relational operators >, >=, < and <= shall not be applied to expressions of pointer type except where they point into the same object	`MISRA C:2012 Rule 18.3`
MISRA C:2012 Rule 18.6	The address of an object with automatic or thread-local storage shall not be copied to another object that persists after the first object has ceased to exist	`MISRA C:2012 Rule 18.6`
MISRA C:2012 Rule 19.1	An object shall not be assigned or copied to an overlapping object	`MISRA C:2012 Rule 19.1`
MISRA C:2012 Rule 1.2	Language extensions should not be used	`MISRA C:2012 Rule 1.2`
MISRA C:2012 Rule 1.3	There shall be no occurrence of undefined or critical unspecified behaviour	`MISRA C:2012 Rule 1.3`
MISRA C:2012 Rule 1.5	Obsolescent language features shall not be used	`MISRA C:2012 Rule 1.5`
MISRA C:2012 Rule 21.13	Any value passed to a function in `<ctype.h>` shall be representable as an `unsigned char` or be the value EOF	`MISRA C:2012 Rule 21.13`
MISRA C:2012 Rule 21.14	The Standard Library function `memcmp` shall not be used to compare null terminated strings	`MISRA C:2012 Rule 21.14`
MISRA C:2012 Rule 21.17	Use of the string handling function from `<string.h>` shall not result in accesses beyond the bounds of the objects referenced by their pointer parameters	`MISRA C:2012 Rule 21.17`
MISRA C:2012 Rule 21.18	The `size_t` argument passed to any function in `<string.h>` shall have an appropriate value	`MISRA C:2012 Rule 21.18`
MISRA C:2012 Rule 21.19	The pointers returned by the Standard Library functions `localeconv`, `getenv`, `setlocale` or `strerror` shall only be used as if they have pointer to `const`-qualified type	`MISRA C:2012 Rule 21.19`
MISRA C:2012 Rule 21.20	The pointer returned by the Standard Library functions `asctime`, `ctime`, `gmtime`, `localtime`, `localeconv`, `getenv`, `setlocale` or `strerror` shall not be used following a subsequent call to the same function	`MISRA C:2012 Rule 21.20`
MISRA C:2012 Rule 22.1	All resources obtained dynamically by means of Standard Library functions shall be explicitly released	`MISRA C:2012 Rule 22.1`
MISRA C:2012 Rule 22.10	The value of `errno` shall only be tested when the last function to be called was an `errno`-setting function	`MISRA C:2012 Rule 22.10`
MISRA C:2012 Rule 22.11	A thread that was previously either joined or detached shall not be subsequently joined nor detached	`MISRA C:2012 Rule 22.11`
MISRA C:2012 Rule 22.15	Thread synchronization objects and thread-specific storage pointers shall not be destroyed until after all threads accessing them have terminated	`MISRA C:2012 Rule 22.15`
MISRA C:2012 Rule 22.16	All mutex objects locked by a thread shall be explicitly unlocked by the same thread	`MISRA C:2012 Rule 22.16`
MISRA C:2012 Rule 22.17	No thread shall unlock a mutex or call `cnd_wait()` or `cnd_timedwait()` for a mutex it has not locked before	`MISRA C:2012 Rule 22.17`
MISRA C:2012 Rule 22.2	A block of memory shall only be freed if it was allocated by means of a Standard Library function	`MISRA C:2012 Rule 22.2`
MISRA C:2012 Rule 22.3	The same file shall not be open for read and write access at the same time on different streams	`MISRA C:2012 Rule 22.3`
MISRA C:2012 Rule 22.4	There shall be no attempt to write to a stream which has been opened as read-only	`MISRA C:2012 Rule 22.4`
MISRA C:2012 Rule 22.5	A pointer to a `FILE` object shall not be dereferenced	`MISRA C:2012 Rule 22.5`
MISRA C:2012 Rule 22.6	The value of a pointer to a `FILE` shall not be used after the associated stream has been closed	`MISRA C:2012 Rule 22.6`
MISRA C:2012 Rule 22.7	The macro `EOF` shall only be compared with the unmodified return value from any Standard Library function capable of returning `EOF`	`MISRA C:2012 Rule 22.7`
MISRA C:2012 Rule 22.8	The value of `errno` shall be set to zero prior to a call to an `errno`-setting-function	`MISRA C:2012 Rule 22.8`
MISRA C:2012 Rule 22.9	The value of `errno` shall be tested against zero after calling an `errno`-setting function	`MISRA C:2012 Rule 22.9`
MISRA C:2012 Rule 2.1	A project shall not contain unreachable code	`MISRA C:2012 Rule 2.1`
MISRA C:2012 Rule 2.2	A project shall not contain dead code	`MISRA C:2012 Rule 2.2`
MISRA C:2012 Rule 8.13	A pointer should point to a const-qualified type whenever possible	`MISRA C:2012 Rule 8.13`
MISRA C:2012 Rule 9.1	The value of an object with automatic storage duration shall not be read before it has been set	`MISRA C:2012 Rule 9.1`

Undecidable Directives

A directive is undecidable if a static analysis tool can check compliance to it only in certain cases. Polyspace shows the subset of all possible issues. For details about which issues Polyspace detects for a particular directive, see the Polyspace Implementation section in the reference page of the directive. Polyspace supports 18 out of 21 such directives.

MISRA C:2012 Directives	Description	Polyspace Checker
MISRA C:2012 Dir 1.1	Any implementation-defined behavior on which the output of the program depends shall be documented and understood	`MISRA C:2012 Dir 1.1`
MISRA C:2012 Dir 2.1	All source files shall compile without any compilation errors	`MISRA C:2012 Dir 2.1`
MISRA C:2012 Dir 4.1	Run-time failures shall be minimized	`MISRA C:2012 Dir 4.1`
MISRA C:2012 Dir 4.10	Precautions shall be taken in order to prevent the contents of a header file being included more than once	`MISRA C:2012 Dir 4.10`
MISRA C:2012 Dir 4.11	The validity of values passed to library functions shall be checked	`MISRA C:2012 Dir 4.11`
MISRA C:2012 Dir 4.12	Dynamic memory allocation shall not be used	`MISRA C:2012 Dir 4.12`
MISRA C:2012 Dir 4.13	Functions which are designed to provide operations on a resource should be called in an appropriate sequence	`MISRA C:2012 Dir 4.13`
MISRA C:2012 Dir 4.14	The validity of values received from external sources shall be checked	`MISRA C:2012 Dir 4.14`
MISRA C:2012 Dir 4.15	Evaluation of floating-point expressions shall not lead to the undetected generation of infinities and NaNs	`MISRA C:2012 Dir 4.15`
MISRA C:2012 Dir 4.3	Assembly language shall be encapsulated and isolated	`MISRA C:2012 Dir 4.3`
MISRA C:2012 Dir 4.4	Sections of code should not be "commented out"	`MISRA C:2012 Dir 4.4`
MISRA C:2012 Dir 4.5	Identifiers in the same name space with overlapping visibility should be typographically unambiguous	`MISRA C:2012 Dir 4.5`
MISRA C:2012 Dir 4.6	`typedefs` that indicate size and signedness should be used in place of the basic numerical types	`MISRA C:2012 Dir 4.6`
MISRA C:2012 Dir 4.7	If a function returns error information, then that error information shall be tested	`MISRA C:2012 Dir 4.7`
MISRA C:2012 Dir 4.8	If a pointer to a structure or union is never dereferenced within a translation unit, then the implementation of the object should be hidden	`MISRA C:2012 Dir 4.8`
MISRA C:2012 Dir 4.9	A function should be used in preference to a function-like macro where they are interchangeable	`MISRA C:2012 Dir 4.9`
MISRA C:2012 Dir 5.1	There shall be no data races between threads	`MISRA C:2012 Dir 5.1`
MISRA C:2012 Dir 5.2	There shall be no deadlocks between threads	`MISRA C:2012 Dir 5.2`