AbsInt Astrée and RuleChecker Version 19.04

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


absint.com/releasenotes/astree/19.04



2019-06-25T04:31:21+00:00