Astrée is now able to check coding rules (MISRA), compute code metrics (comment density, cyclomatic complexity, etc.), and check metric thresholds. The rule checker is highly configurable, allowing users to toggle checks for individual rules or aspects of certain rules.
The majority of the checks is performed syntactically, either on the source code or on the preprocessed code. It is possible to skip the runtime error analysis and only perform the rule checks.
A few more checks, for which a purely syntactic analysis would be too imprecise, are performed during the runtime error analysis. If a selected coding rule is violated, the analyzer reports an alarm of the new category R and reports the violated rule together with the exact code location and the check which failed.
__ASTREE_partition_controlwhich have been inserted automatically by the analyzer. Displaying such automatically inserted directives can be turned off and on in the Preferences dialog.
--stopfor stopping an analysis that is running on the server.
stop-parse-error-immediate=no) but to continue and optionally stop before starting the actual analysis (
stop-parse-error-delayed=yes). Files with parse errors are discarded after reporting the error.
bits_of_byte. It accepts the values
16, the default being
8. When the value
16is used, the additional option
bits_of_charconfigures computations on values of type
charto have either 8- or 16-bit precision.
verbose-variable-alarm, as alarm messages of the analyzer are now always verbose.
warn-in-simplify, as all run-time errors that can be found during constant propagation and simplification are also reported by the subsequent run-time error analysis.
Added new QSK test cases for validating the “External Declarations” feature.
The server data directory’s name must not contain special characters, including accented letters or umlauts.
/* Result summary */ Reached 26 of 26 statements during the analysis.
(cond ? expr1 : expr2).
#line 123” which could fail when using parser filters.
<messages>section of the XML report now feature the actual message text as one or several
<id>tag in DAX files. It now behaves exactly as documented.