Astrée and RuleChecker Release 19.04
-----------------------------------
Spectre vulnerability detection
------------------------------
Astrée now detects and reports Spectre v1, Spectre v1.1, and SplitSpectre
vulnerabilities. The detection is disabled by default and can be enabled
via the new option "detect-spectre".
Taint analysis
--------------
Astrée can now track taint information for memory locations.
This new feature can be used for analyzing security properties.
It is disabled by default and can be enabled by setting the option
"track-taint-hues".
Additionally, the new directives "__ASTREE_taint" and "__ASTREE_taint_sink"
can be inserted into the code for expressing where variables are tainted
and which memory locations must not be reached by taints.
Closed beta: Astrée for C++
--------------------------
This is the first Astrée release to offer
static run-time error analysis of C++ code.
Evaluation licenses can now be issued on request.
Extended AUTOSAR support
-----------------------
▲ RuleChecker can now check C++ code for compliance with
AUTOSAR C++ coding rules as defined in the AUTOSAR document
“Guidelines for the use of the C++14 language in critical
and safety-related systems”.
▲ Astrée now supports AUTOSAR multi-core systems
using a multi-core aware OS model with support for spinlocks.
The OS setup can be automatically derived from ARXML.
▲ To improve the analysis performance for AUTOSAR projects,
Astrée now provides analysis stubs for the AUTOSAR modules
"NvM" (NVRAM Manager) and "Dem" (Diagnostic Event Manager).
The stubs are located in the AUTOSAR subdirectory of the installation,
and the user manual now includes a chapter dedicated to their
use and configuration.
Frontends
---------
▲ The C frontend now accepts lvalue casts, as supported
by older versions of the GCC compiler. Example:
float* fp = 0;
int* ip = 0;
(int*)fp = ip; /* lvalue cast */
Note that such code violates the diagnostic rule A.2.6 (check "lvalue-cast")
and is no longer supported by current C compilers.
▲ Source directives are now also accepted
and applied in single-line comments ("//...").
▲ The C frontend now rejects strictly invalid array index expressions
(which are also not accepted by compilers).
Options
-------
▲ New option "continue-on-definite-rte".
If Astrée encounters a definite run-time error while this option
is enabled, the analysis does not stop for the affected context
but carries on with partial statement semantics.
▲ New option "collapse-multi-dimensional-arrays"
that controls whether multi-dimensional arrays are considered as
a single type layer for naming rule checks.
▲ The type name configured via option "boolean-type"
is now equivalent to "_Bool" for naming checks.
Command-line options
-------------------
▲ The server broadcast can now be limited to the local host.
The feature is available via the server controller and the new server
command-line option "--local-broadcast".
▲ Corrected the behavior of the option "--export-preprocessed"
such that it exports the successfully preprocessed files even when
the preprocessing of other files fails.
Directives
----------
▲ Modified the syntax of the following directives to improve consistency:
New syntax Old syntax
__ASTREE_volatile_input((v; [l,h])); __ASTREE_volatile_input((v, [l,h]));
__ASTREE_global_assert((v; [l,h])); __ASTREE_global_assert((v, [l,h]));
__ASTREE_known_range((v; [l,h])); __ASTREE_known_range((v, [l;h]));
__ASTREE_partition_ranges((g; [l,h], [l,h]));
__ASTREE_partition_ranges((v: [l;h], [l;h]));
The old syntax is still accepted, but the new syntax is now preferred.
▲ For loops that contain "__ASTREE_partition_begin" directives,
the analyzer is now much faster, thanks to improved widening.
▲ Astrée can now track taint information for memory locations.
This feature can be enabled by setting the option "track-taint-hues".
Additionally, the new directives "__ASTREE_taint" and "__ASTREE_taint_sink"
can be inserted into the code for expressing where variables
are tainted and which memory locations must not be reached by taints.
▲ Fixed an issue in the evaluation of the directive
"__ASTREE_partition_control((1))". Using it in front of a loop
caused the first partition to get lost.
ABI
---
▲ Renamed the ABI option key "endianess" to "endianness".
▲ Removed the ABI option "rounding_mode_for_constants".
Floating point constant expressions evaluated at compile-time
are now always evaluated using rounding to nearest (as required
by the C standard, see ISO/IEC 9899:2011, F.8.2).
▲ The default ABI assumed by Astrée and RuleChecker now uses
bitfield_sign=signed. The default ABI is now also available
as a DAX file (default_generic_32.dax) installed with the other ABIs.
▲ The analyzer now also considers the ABI option "bits_of_byte"
when determining the size of floats and doubles. (In previous releases
it only had an effect on integer types.) Therefore with
sizeof_double=4 and bits_of_byte=16 the analyzer now considers
doubles to have 64 instead of only 32 bits.
▲ Fixed essential typing of constant expressions in case that the ABI value
bits_of_byte is set to a value other than the default of 8.
This affects most M2012.10.x checks, if the ABI is configured
in the aforementioned way.
▲ Fixed the ABI for the Diab compiler on 32-bit PowerPC by setting
the ABI option alignof_char_array to its default value of 1. The ABI
for this target as shipped with previous Astrée releases assumed
an alignment of 4, corresponding to the compiler documentation.
To the best of our knowledge, this alignment is not used by the compiler
for aligning arrays in structs, which is the only case for which the aforementioned
option is relevant for Astrée. In such cases the compiler uses a 1-byte alignment.
DAX
---
▲ Incremented the DAX version number to 1.6.
▲ File names in RuleChecker configurations are now exported
to DAX using relative paths.
▲ Improved license-token handling when importing a DAX file containing
an <id> tag. The "rulechecker" token is now released after preprocessing.
▲ DAX files are now rejected with an error message if they contain
the option <relational>no</relational> followed by
<any-relational-domain>yes</any-relational-domain>
where "any-relational-domain" is the option key of any relational domain,
e.g. "octagon". In previous releases, such specifications were accepted
but led to disparate behaviors in GUI and batch mode.
▲ Setting the DAX export option "Options=All" no longer exports
sub-options that are disabled by their parent option.
This modification ensures that exported DAX files are always
consistent with respect to the analyzer options.
Alarms, messages and warnings
----------------------------
Fixed the display and reporting of unreachable if statements
that are partitioned by an "__ASTREE_partition_control" directive.
Improved reporting
------------------
▲ HTML report files now contain a table of contents
for easier navigation in large report files.
▲ When printing analyzer options to report files,
analysis runs in batch mode now behave the same as in GUI mode,
i.e. only options that deviate from their default values are now reported.
To complement that, a new option "print-all-options=yes"
is introduced that forces the printing of all analyzer options,
including those set to their default values. It can be used in either mode.
▲ Functions that are ignored due to an "__ASTREE_ignore" directive
are now displayed as filtered in the editor view.
Server and server controller
---------------------------
▲ Improved server stability.
▲ Analyses that fail to start from the server’s analysis queue
are no longer automatically re-queued. This fixes issues with queued
analysis projects blocking the server.
▲ Fixed an issue in the installer that prevented the server from
starting automatically after reboot, even if the installer option
“Register a3 for C server as a service” was enabled.
▲ The server controller now displays its build number in the title bar.
▲ The Management view of the server controller now shows
the version information of the currently selected server.
▲ The server broadcast can now be limited to the local host.
The feature is available via the server controller and the new server
command-line option "--local-broadcast".
▲ The server port can now be configured in the server controller
if not restricted by the license file. The last configured port number
is used automatically when restarting the server.
▲ Allow the server to accept command line arguments
specified in the Windows service configuration if run as service.
Client GUI and batch mode
------------------------
▲ Improved search:
△ Faster filtering and searching in large collections of findings,
e.g. in the Findings view.
△ The identifier search no longer lists declarations of objects
for which a definition exists. For such objects only the definition
is listed. This change improves the performance of the identifier
search on very large analysis projects.
△ A search feature that can be invoked by pressing Ctrl+F
is now available in all of the following tabs of the Results view:
Findings/C, Findings/F, Rule violations, and Reachability.
▲ Improved performance when displaying source files with large numbers of alarms.
▲ Fixed the Watch view for investigating variables and lvalues in Astrée.
The feature was not working correctly in release 18.10.
▲ Jumping to another code location or switching from an editor
to another view now always enables the button for going back to
the last code location.
▲ The context menu entries "Disable", "Go to annotation" and "Edit"
in the editor now also work for AAL-inserted comment directives.
▲ Fixed the Verbosity selector of the Output view.
In release 18.04 and later, changing the verbosity in an already opened
analysis project could have undesired effects: empty cells in the 'Message'
column of the Findings view missing information (message texts and data races)
in XML and custom report files that were generated after modifying
the verbosity slider.
▲ Corrected the behavior of the option "--export-preprocessed"
such that it exports the successfully preprocessed files even when
the preprocessing of other files fails.
▲ Hovering over an AAL annotation in the Editor view
now also shows the comment for that annotation.
▲ The Annotations view now allows duplicating a set of annotations.
▲ Copying contents from the Annotations view into the clipboard
now also copies the information if an annotation was disabled.
▲ The effects of parser filters are now displayed immediately after
the frontend has finished and before starting the analysis.
▲ List edit dialogs for complex options now also allow editing the list
of parameters in a text edit field.
▲ The split view for preprocessed code now provides context menu entries
for jumping to the corresponding line in the original code editor.
The feature is available in the preprocessed code editor as well as
in the associated original code view on the right-hand side.
▲ Fixed display of the "Definite runtime error" line
in the detailed call stack information area of the Findings view
which was missing in 18.10i releases.
▲ Fixed an issue with the display of lengthy tooltips in editor views.
▲ Fixed an issue that caused coverage, data flow, and control-flow information
to be missing from the predefined report files in batch mode.
Improved precision
-----------------
▲ Precision has been improved for all of the following checks:
△ "address-of-overload"
△ "digraph-token"
△ "stdlib-use"
△ "unrelated-pointer-conversion"
△ "unary-assign-separation"
△ "virtual-call-in-constructor"
△ "return-position"
△ "inconsistent-default-argument"
△ "null-as-integer"
△ "multiple-loop-counters"
△ "mixed-virtual-base"
△ "member-function-missing-const"
▲ Improved precision of the check "plain-char-usage"
in code using the comma operator or references.
▲ Improved precision of the check "underlying-cvalue-conversion"
by ignoring irrelevant implicit conversions, like "non-const" to "const" pointers.
▲ Improved precision of the check "parameter-missing-const"
for rule CERT.DCL.0, CERT.DCL.13, M.16.7, and M2012.8.13.
▲ Improved precision of the check "controlling-invariant-expression"
used in rule M.14.1, M2012.2.1, and M2012.14.3.
▲ Improved precision of the checks "wide-narrow-string-cast"
and "wide-narrow-string-cast-implicit" used in rule CERT.STR.38.
Improved placeholders
---------------------
▲ Naming-rule configurations can now use the new placeholder
"%Module_abbreviation%". The expansion of the placeholder, e.g. "xyz",
is defined per source file using the syntax "\module_abbreviation xyz"
in an arbitrary comment.
▲ Fixed evaluation of the placeholder "%Folder#%"
which was ignored in all 18.04i and 18.10 builds.
▲ The placeholder "%bitsize%" is now also available
for objects of "struct" or "enum" type, including enumeration constants.
Other improvements
-----------------
▲ New option "collapse-multi-dimensional-arrays"
that controls whether multi-dimensional arrays are considered as
a single type layer for naming rule checks.
▲ The type name configured via option "boolean-type"
is now equivalent to "_Bool" for naming checks.
▲ Pragmas of the form
#pragma push_macro("XYZ")
#pragma pop_macro("XYZ")
are no longer rejected with an error message if "XYZ" is not defined.
▲ In case of errors during parsing, RuleChecker now always terminates with exit code "1",
after performing partial rule checking on the successfully parsed files.
New rules for C
--------------
▲ T.15.1, associated with the check "max-local-variables".
This check is violated if the specified threshold for local variables in a function is exceeded.
▲ T.16.1, associated with the check "max-size-of-statement".
This check is violated if the specified threshold for the sum of operands and operators in a statement is exceeded.
Rule sets and checks for C
-------------------------
▲ New rule check "multiple-writes-in-full-expr"
warns about full expressions in which a variable is written
more than once. This is used to warn about violations of rule M.12.2.
▲ New diagnostic rule A.1.11 warns about implicit conversion
between incompatible pointer types.
▲ Extended coverage of rule M.1.1, M.11.1, M2012.1.1, M2012.11.1,
and CERT.MSC.40.
▲ Removed false alarms for:
△ "pointer-qualifier-cast-const-implicit" when the second argument
to "__astree_memcpy" is a pointer to "const"
△ "boolean-invariant" in switch statements
△ "multiple-volatile-accesses" and "evaluation-order"
when they take the address of an array
△ "array-initialization" (rule M2012.9.3)
in case of nested arrays inside of zero-initialized structures,
such as
struct { int a[2];} s = { 0 };
▲ The check "function-pointer-cast" for rule M.11.1
and M2012.11.1 no longer warns about null pointer constants.
▲ The following checks have been split for const-qualified
and non-constant objects:
| global-object-name | ↗
↘ | global-object-name
global-object-name-const |
| static-object-name | ↗
↘ | static-object-name
static-object-name-const |
| local-object-name | ↗
↘ | local-object-name
local-object-name-const |
▲ Fixed essential typing of constant expressions in case that the ABI value
"bits_of_byte" is set to a value other than the default of "8".
This affects most M2012.10.x checks, if the ABI is configured
in the aforementioned way.
▲ Alarms concerning essential types now also mention the type, not just the category.
▲ The option "allow-signed-constant-with-unsigned"
is now also considered for the check "bitop-type"
used in rule CERT.INT.13, CERT.INT.16, M.12.7, and X.A.5.
▲ The check "integral-type-name", used in rule M.6.3, M2008.3.9.2,
M2012.D.4.6, X.A.5.6, and X.D.8.2.a, now honors the exceptions 2, 3, and 4
of MISRA-C:2012 directive 4.6. Therefore, it no longer warns about uses
of the predefined types "int" and "char" in a declaration or definition
of the main function.
▲ Diagnostics rule A.5.2 now also warns about #pragma directives
whose semantics are not taken into account by Astrée.
SEI CERT Secure C
-----------------
Added support for following SEI CERT coding rules/recommendations:
▲ CERT.EXP.5
▲ CERT.EXP.9
▲ CERT.EXP.13
▲ CERT.EXP.15
▲ CERT.EXP.16
▲ CERT.INT.16
▲ CERT.PRE.11
▲ CERT.PRE.12
▲ CERT.PRE.30
▲ CERT.STR.5
▲ CERT.STR.10
▲ CERT.API.8
▲ CERT.ARR.1
▲ CERT.ARR.39
▲ CERT.DCL.5
▲ CERT.ERR.7
▲ CERT.WIN.1
Rule sets and checks for C++
---------------------------
▲ New checks:
△ "multiple-writes-in-full-expr" warns about full expressions
in which a variable is written more than once to warn about violations of rule M2012.13.2.
△ "float-suffix" for rule M2008.2.13.4 warns about the floating literal suffix 'f'.
▲ The check "functional-cast" no longer reports constructor conversions.
▲ The checks "new-operator" and "delete-operator" no longer warn
about placement operators.
▲ The check "unary-assign-separation" is now also applied to overloaded operator calls.
▲ The checks for rule M2008.6.4.3 no longer warn about
switch statements without default clause.
▲ The checks for rule M2008.6.4.6 no longer warn about exhaustive
switch statements over values of enum type without default clause.
▲ Improved the check "functional-cast" for rule M2008.5.2.4.
▲ Sharpened the check bitop-type to warn about more cases of bit operations
on values of unfitting type.
▲ The check "cast-integer-to-pointer" now warns
about casting an integral type to any pointer type.
▲ The check "integral-type-name" now also warns
about uses of integral type names in cast operators.
▲ Rule M2008.7.3.1 can now be parameterized with a set of type names
that are allowed to be declared at file scope.
▲ Improved the check for rule M2008.8.5.2 to eliminate false alarms
for empty initializer lists initializing the whole object, e.g.
int a[2][2] = {}; // compliant
▲ The check "unused-internal-function" (rule M2008.0.1.10)
no longer warns about template functions.
▲ The check float-bits-from-pointer" (rule M2008.3.9.3)
now also covers reinterpret_cast.
▲ The check enum-usage" (rule M2008.4.5.2)
no longer warns if the unary "&" operator
is applied to an expression of type "enum".
▲ Refined checks for rule M2008.4.5.3.
▲ Improved the check "loop-control-modification" for rule M2008.6.5.5.
▲ Improved the check "inappropriate-enum" for rule M2012.10.1 to eliminate
false alarms for expressions of the form "&arr[e]" when "e" is of "enum" type.
AUTOSAR C++ support
-------------------
New rule set “AUTOSAR” with checks for AUTOSAR C++ coding rules
as defined in the AUTOSAR document “Guidelines for the use of the C++14 language
in critical and safety-related systems”.
Metrics
-------
▲ The new function metric LOCVAR counts the number of local variables
which are declared in a function.
▲ The LSCOPE metric now considers all function calls, dereferences,
array look-ups and struct-member accesses.
Stub libraries and compiler configurations
-----------------------------------------
▲ To improve the analysis performance for AUTOSAR projects,
Astrée now provides analysis stubs for the AUTOSAR modules
NvM (NVRAM Manager) and Dem (Diagnostic Event Manager).
The stubs are located in the share/source/AUTOSAR subdirectory
of the installation. The use and proper configuration of these stubs
is described in the user manual.
▲ Modified the OSEK stub generation from .oil files,
so that ISRs may now preempt tasks which hold the scheduler
resource (RES_SCHEDULER). Please note that this modification
only affects analyses which are configured to take priorities
precisely into account (precise-priorities=yes).
With the default option 'precise-priorities=no' the analyzer does not
exclude preemption based on resource priorities.
▲ The compiler configuration and stub library for CompCert PowerPC
has been extended to support the built-in functions isel64, uisel64,
and bsel, provided by recent versions of the compiler.
▲ Fixed the ABI for the Diab compiler on 32-bit PowerPC
by setting the ABI option "alignof_char_array" to its default value
of 1. The ABI for this target, as shipped with previous Astrée
releases, assumed an alignment of 4, corresponding to the compiler documentation.
To the best of our knowledge, this alignment is not used by the compiler
for aligning arrays in structs, which is the only case for which the aforementioned
option is relevant for Astrée. In such cases the compiler uses a 1-byte alignment.
Preprocessor
------------
▲ C, C++, and other stub-library "include" paths
have been moved to the end of the include-path list.
This allows to provide custom standard header replacements
if needed. For example, a "math.h" of your own
will now overwrite the stub library "math.h" shipped with the tool.
▲ The C99 macro "__TIME__" now expands to "??:??:??",
and likewise "__DATE__" now expands to "??? ?? ????".
This ensures stable results between different analysis runs.
Slicing
-------
Context proposals for program slicing no longer contain contexts
that have not been reached by the runtime error analysis.
License management
------------------
▲ Improved the ALM token handling for cases when the connection
between the analysis client and the analysis server is lost during
preprocessing. The "rulechecker" token is now immediately released
as soon as the server considers the connection definitely lost.
▲ Improved the ALM token handling in case of importing a DAX file
that contains an <id> tag. The "rulechecker" token is now released after preprocessing.
Integration with TargetLink
--------------------------
▲ Added support for the new TargetLink release 4.4.
▲ The AbsInt toolbox for TargetLink can now be configured
to run the analysis in batch mode instead of running it in GUI batch mode.
The analysis then runs without any user interaction and without opening
any windows.
▲ Improved precision of the interpolation domain.
If activated, the analyzer now reports significantly
fewer alarms in TargetLink interpolation functions.
▲ Removed unintended output (state = 'Hidden') from the Matlab command window.
▲ The AbsInt toolbox for TargetLink and the TargetLink Data Dictionary Importer
now provide an option for generating "__ASTREE_partition_control"
directives instead of "__ASTREE_unroll directives" for interpolation
routines.
Other Astrée improvements
------------------------
▲ When the second argument of a shift is too big (raising the alarm
“range of second shift argument ... not included in ...”),
the analyzer now also includes "0" in the result.
▲ Alarms about possible data races now include the name of the process
in which the alarm is detected.
▲ The analyzer no longer stops with an error if the return type of a function
is not compatible with the return type assumed by the calling expression
and the result of the function call is not used. Instead, the analysis
raises an alarm A and continues. The new behavior is consistent with
the behavior for incompatible function calls in which the result
is used by the caller.
▲ Improved the analyzer's precision on computations with bit-masks.
▲ The heuristic selection of functions for context-insensitive analysis
(option separate-function=*) now takes function substitutions into account.
This results in a better choice of separate functions in the presence
of function substitutions.
▲ Improved analyzer performance for analysis projects that enable
the option "warn-on-field-overflows".
▲ Improved the precision of location information for certain alarms.
In particular write data race and global assertion alarms in an assignment
are now reported for the left-hand side of the assignment. Please note
that comments for such alarms may need to be moved to the new location
when re-running older analyses.
▲ Fixed false alarms in "__ASTREE_modify" directives on arrays.
▲ For function calls with incompatible parameter or return types,
the analyzer now assumes that values with incompatible type are converted
according to the rules of C, if such rules are applicable.
Otherwise it assumes any value.
▲ Added a new relational domain for more precise analysis
of finite state machines. The new domain is activated
with the option "state-machine=yes". It reacts
to the new directive "__ASTREE_states_track((x))"
which indicates that "x" is used to encode
the state of a state machine. Special treatment stops
upon encountering either "__ASTREE_states_merge((x))"
or "__ASTREE_states_merge(())".
The new option "automatic-state-machine=yes" enables
automatic detection of code patterns used in state machine
implementations, for which Astrée can then insert
"__ASTREE_states_track" directives.
▲ Fixed address computation for objects that are specified
to overlap in memory by "__ASTREE_absolute_address" directives.
▲ Control flow information is now also displayed
if the reporting of data flow information was disabled
for the analysis (using the option "dump-dataflow=no").
Moreover, it now also contains call information for calls
that are only reachable via separately analyzed functions
(option "separate-function").
▲ Function calls with incompatible types now always raise an alarm of type A.
Previous releases raised an alarm of type A or C depending on the kind of incompatibility.
▲ Added new analyzer intrinsic functions for simplified process creation.
After invoking "__astree_create_process" with minimal arguments,
the following functions can be called for setting further process properties:
△ __astree_set_process_running_priority(process_id, priority)
△ __astree_set_process_non_realtime(process_id)
△ __astree_set_process_core(process_id, core)
▲ Added the new analyzer-intrinsic function
__astree_core_process(unsigned *c)
which stores in "*c" the ID of the core
that the current process is running on.
▲ Improved the performance of the static dependencies pre-analysis.
▲ Fixed an issue in the gauges abstract domain that could remove
some traces from the analysis, possibly stopping the analyzer with
an error message.
▲ Fixed an issue that caused the analyzer to abort with an error message
when using an undeclared absolute address of with an incomplete type, e.g.
struct T {}; // incomplete type ...
struct T* p = (struct T*)0x1000; // ... used with absolute address
▲ Fixed an issue that in rare circumstances could stop the analyzer
with the error message "Cannot project mismatching partition IDs".
▲ Fixed an issue that caused the analysis to abort with an error message
in a function call with incorrect type. After reporting the error,
the analyzer now proceeds, assuming that the value of the incorrectly
typed argument is undefined.
▲ Fixed an issue with missing data-race alarms in case that
a low priority process writing to a variable could be interrupted
by a higher priority process reading from the same variable
and the option precise-priorities=yes was set. Please note
that the effects of the data race were soundly taken into account
by the analyzer, so that possible run-time errors triggered
by the data race were still reported. The fix only ensures
that the analyzer reports the additional data race alarms
in this situation.
Other changes
-------------
▲ The tool now uses more descriptive names when referring
to static variables whose identifier is not unique. For example,
a static variable named "var" and declared in "file.c"
is now reported as "var@"file.c"".
▲ Multiple files with the same file name are now distinguished
by adding the minimum path information required for obtaining
a unique name. Elided prefixes are represented by a single ‘"..."’.
For example, the files
/test/share/libcxx/include/stdlib.h
/test/testcase/stubs/stdlib.h
are now represented as
.../include/stdlib.h
.../stubs/stdlib.h
The short files names are used in the analyzer output
as well as in the text and HTML report files.
▲ Analysis queuing is now fully supported for both
Astrée and RuleChecker analyses.
▲ The import of external declarations from text format (*.edf) is no longer supported.
TOR/VTP improvements
--------------------
▲ Added the sub words "REQ" and "QK" to the legend for the construction
of requirement/test case identifier names.
▲ Only the configuration recommendations relevant to the particular
core feature are now shown in the TOR.
▲ Avoiding usage of the abbreviation “QSK” without explanation.
▲ Added a section listing the covered D0-330 objectives.
Other improvements
-----------------
▲ Enhanced check for Windows’ max path limitation.
▲ Revised QSK package file names and improved installation path consistency checks.
▲ Added missing text fragments to the Verification Test Plan for RuleChecker
concerning the QSK tests "qk_check_extra_tokens" and "qk_check_non_standard_identifier".
New test cases in the Astrée QSK
-------------------------------
▲ Options:
△ qk_option_detect_spectre
△ qk_option_continue_on_definite_rte
△ qk_option_print_all_options
△ qk_option_drop_unused_statics
△ qk_option_filter_attributes
△ qk_option_state_machine
△ qk_option_automatic_state_machine
△ qk_option_report_file
△ qk_option_track_taint_hues
△ qk_option_misspelled
▲ Directives:
△ qk_directive_states_track
△ qk_directive_states_merge
△ qk_directive_taint
△ qk_directive_taint_sink
▲ Alarms:
△ qk_alarm_taint_sink
△ qk_alarm_spectre_vulnerability
▲ Intrinsics:
△ qk_intrinsic_set_process_running_priority
△ qk_intrinsic_set_process_non_realtime
△ qk_intrinsic_set_process_core
△ qk_intrinsic_core_process
▲ Checks:
△ qk_check_errno_reset
△ qk_check_incompatible_argument_type
△ qk_check_precision_shift_width
△ qk_check_int_modulo_by_zero
△ qk_check_write_to_string_literal
△ qk_check_null_dereferencing
△ qk_check_precision_shift_width_constant
△ qk_check_array_index_range_constant
△ qk_check_parameter_match
▲ Rules:
△ qk_rule_cert_flp_3
△ qk_rule_cert_msc_12
△ qk_rule_cert_dcl_30
△ qk_rule_cert_str_30
△ qk_rule_cert_mem_34
△ qk_rule_cert_arr_30, qk_rule_cert_arr_36
△ qk_rule_cert_err_30, qk_rule_cert_err_33
△ qk_rule_cert_int_8, qk_rule_cert_int_30, qk_rule_cert_int_32,
qk_rule_cert_int_33, qk_rule_cert_int_34
△ qk_rule_cert_exp_12, qk_rule_cert_exp_33, qk_rule_cert_exp_34,
qk_rule_cert_exp_37, qk_rule_cert_exp_40
△ qk_rule_iso17961_addrescape,
qk_rule_iso17961_dblfree,
qk_rule_iso17961_diverr,
qk_rule_iso17961_intoflow,
qk_rule_iso17961_inverrno,
qk_rule_iso17961_nullref,
qk_rule_iso17961_ptrobj,
qk_rule_iso17961_xfree,
qk_rule_iso17961_liberr,
qk_rule_iso17961_uninitref,
qk_rule_iso17961_invptr,
qk_rule_iso17961_strmod
The test case "qk_abi_rounding_mode_for_constants" has been removed
from the Astrée QSK.
New test cases in the RuleChecker QSK
------------------------------------
▲ Options:
△ qk_option_file_name_modifier
△ qk_option_collapse_multi_dimensional_arrays
△ qk_option_print_all_options
△ qk_option_report_file
△ qk_option_anonymous_global_structs_and_unions
△ qk_option_stop_parse_error_immediate
△ qk_option_filter_attributes
▲ Placeholders:
△ qk_placeholder_bitsize
△ qk_placeholder_filename
△ qk_placeholder_folder
△ qk_placeholder_module_abbreviation
▲ Checks:
△ qk_check_global_object_name_const
△ qk_check_local_object_name_const
△ qk_check_static_object_name_const
△ qk_check_plain_char_operator
△ qk_check_multiple_writes_in_full_expr
△ qk_check_incompatible_function_pointer_conversion
△ qk_check_incompatible_object_pointer_conversion
△ qk_check_float_comparison
△ qk_check_stdlib_use_signal
△ qk_check_multiple_atomic_accesses
△ qk_check_alignof_side_effect
△ qk_check_generic_selection_side_effect
△ qk_check_stream_argument_with_side_effects
△ qk_check_memcmp_with_float
△ qk_check_named_declaration_parameter
△ qk_check_scaled_pointer_arithmetic
△ qk_check_pointer_typedef
△ qk_check_bad_function
△ qk_check_alloc_without_sizeof
△ qk_check_chained_comparison
△ qk_check_empty_body
△ qk_check_function_name_constant_comparison
△ qk_check_pointer_cast_alignment
△ qk_check_memcmp_with_padding
△ qk_check_assignment_conditional
△ qk_check_alloc_without_cast
△ qk_check_flexible_array_member_assignment
△ qk_check_flexible_array_member_declaration
△ qk_check_malloc_size_insufficient
△ qk_check_stdlib_use_rand
△ qk_check_long_suffix
△ qk_check_macro_final_semicolon
△ qk_check_macro_parameter_multiplied
△ qk_check_macro_parameter_unused
△ qk_check_universal_character_name_concatenation
△ qk_check_signal_handler_unsafe_call
△ qk_check_signal_handler_shared_access
△ qk_check_signal_handler_signal_call
△ qk_check_encoding_mismatch
△ qk_check_char_sign_conversion
△ qk_check_wide_narrow_string_cast
△ qk_check_wide_narrow_string_cast_implicit
△ qk_check_switch_enum_default
△ qk_check_precision_shift_width_constant
△ qk_check_array_index_range_constant
△ qk_check_parameter_match
△ qk_check_max_local_variables
△ qk_check_max_size_of_statement
△ qk_check_literal_assignment_type
▲ Rules:
△ qk_rule_a_1_10, qk_rule_a_1_11
△ qk_rule_t_14_1, qk_rule_t_15_1, qk_rule_t_16_1
△ qk_rule_cert_api_8
△ qk_rule_cert_arr_1, qk_rule_cert_arr_2,
qk_rule_cert_arr_30, qk_rule_cert_arr_39
△ qk_rule_cert_con_37, qk_rule_cert_con_40
△ qk_rule_cert_dcl_0, qk_rule_cert_dcl_5, qk_rule_cert_dcl_7,
qk_rule_cert_dcl_13, qk_rule_cert_dcl_15, qk_rule_cert_dcl_16,
qk_rule_cert_dcl_18, qk_rule_cert_dcl_19, qk_rule_cert_dcl_20,
qk_rule_cert_dcl_31, qk_rule_cert_dcl_36, qk_rule_cert_dcl_37,
qk_rule_cert_dcl_40, qk_rule_cert_dcl_41
△ qk_rule_cert_env_30, qk_rule_cert_env_33
△ qk_rule_cert_err_7, qk_rule_cert_err_33
△ qk_rule_cert_exp_2, qk_rule_cert_exp_5, qk_rule_cert_exp_9,
qk_rule_cert_exp_10, qk_rule_cert_exp_12, qk_rule_cert_exp_13,
qk_rule_cert_exp_15, qk_rule_cert_exp_16, qk_rule_cert_exp_19,
qk_rule_cert_exp_30, qk_rule_cert_exp_33, qk_rule_cert_exp_36,
qk_rule_cert_exp_37, qk_rule_cert_exp_40, qk_rule_cert_exp_42,
qk_rule_cert_exp_44, qk_rule_cert_exp_45
△ qk_rule_cert_fio_38, qk_rule_cert_fio_41
△ qk_rule_cert_flp_2, qk_rule_cert_flp_30,
qk_rule_cert_flp_32, qk_rule_cert_flp_37
△ qk_rule_cert_int_9, qk_rule_cert_int_12, qk_rule_cert_int_13,
qk_rule_cert_int_16, qk_rule_cert_int_34, qk_rule_cert_int_36
△ qk_rule_cert_mem_2, qk_rule_cert_mem_33, qk_rule_cert_mem_35
△ qk_rule_cert_msc_1, qk_rule_cert_msc_4, qk_rule_cert_msc_12,
qk_rule_cert_msc_17, qk_rule_cert_msc_20, qk_rule_cert_msc_24,
qk_rule_cert_msc_30, qk_rule_cert_msc_37, qk_rule_cert_msc_40
△ qk_rule_cert_pre_0, qk_rule_cert_pre_1, qk_rule_cert_pre_6,
qk_rule_cert_pre_7, qk_rule_cert_pre_11, qk_rule_cert_pre_12,
qk_rule_cert_pre_30, qk_rule_cert_pre_32
△ qk_rule_cert_sig_30, qk_rule_cert_sig_31, qk_rule_cert_sig_34
△ qk_rule_cert_str_5, qk_rule_cert_str_10, qk_rule_cert_str_30,
qk_rule_cert_str_34, qk_rule_cert_str_37, qk_rule_cert_str_38
△ qk_rule_cert_win_1
△ qk_rule_iso17961_accsig
△ qk_rule_iso17961_alignconv
△ qk_rule_iso17961_argcomp
△ qk_rule_iso17961_asyncsig
△ qk_rule_iso17961_boolasgn
△ qk_rule_iso17961_chrsgnext
△ qk_rule_iso17961_filecpy
△ qk_rule_iso17961_funcdecl
△ qk_rule_iso17961_insufmem
△ qk_rule_iso17961_libmod
△ qk_rule_iso17961_padcomp
△ qk_rule_iso17961_resident
△ qk_rule_iso17961_sigcall
△ qk_rule_iso17961_signconv
△ qk_rule_iso17961_sizeofptr
△ qk_rule_iso17961_swtchdflt
△ qk_rule_iso17961_syscall
△ qk_rule_iso17961_liberr
△ qk_rule_iso17961_uninitref
△ qk_rule_iso17961_invptr
△ qk_rule_iso17961_strmod
------------------------------------------------------------------------------
Last updated on 18 April 2019 by alex@absint.com. Copyright 2019 AbsInt.
------------------------------------------------------------------------------
An HTML version of these release notes is available at
absint.com/releasenotes/astree/19.04