Joral Technologies Inc.

embeddedshop-wide

Call Now: (877) 380 3366
Fax: (877) 838 7712
twitter log 32linkedin log 32

AbsInt Failure Notice: Astrée for C

In Absint
Tuesday, 22 August 2017 01:35

Problem Description:

When using the option 'separate-function', the analyzer may underestimate the possible value ranges of some local variables. As a result, it may fail to report possible run-time errors.

Scenario:

The erroneous behavior may occur under the following circumstances:

1) If the option separate-function is used and at least one of the selected functions returns a value, i.e., has a non-void return type.

or

2) If both of the options 'separate-function' and 'separate-with-caller-stack-pointers' are used, and at least one of the selected functions returns a value or writes to a local variable in the stack of one of its calling functions using a pointer.

 

Symptoms:

For functions selected for separate analysis, the analyzer underestimates the possible value ranges of return values and the effects on local variables in the stack of calling functions. As a result, it may underestimate the reachable code and fail to report possible run-time errors.

 

Affected versions:

All versions between release 14.10i b236581 and release 17.04i b277146.

 

Troubleshooting:

When using affected Astrée versions, functions with a non-void return type and the special parameter * should be removed from the argument list of the 'separate-function' option. The option 'separate-with-caller-stack-pointers' should also be disabled.

 

 

A corrected version of Astrée is available for download:

Linux 64-bit:

https://www.absint.com/dla/2017/04i/2eae4d605ef/a3_c_linux64_b277963_release.tgz

 

md5-file:

https://www.absint.com/dla/2017/04i/2eae4d605ef/a3_c_linux64_b277963_release.tgz.md5

 

md5-sum:

ae21912f77005f3abb80e15e658ed89a

 

Windows 64-bit:

https://www.absint.com/dla/2017/04i/2eae4d605ef/a3_c_win64_b277963_release.exe

 

md5-file:

https://www.absint.com/dla/2017/04i/2eae4d605ef/a3_c_win64_b277963_release.exe.md5

 

md5-sum:

47dca59b9cafce7a052d72437706da1b

 

 

RELEASE NOTES:

 

Astrée:

* The value of the option 'config-file' is not modified by the dax export anymore and the corresponding *.cfg file can be downloaded without renaming. The dax export dialog allows to select the source files which should be downloaded.

* The GUI now displays the "Comment Patterns" tab in the "Annotations" view that was added but accidentally hidden in release 17.04i b276514.

* The tool now also notifies about ambiguities due to side effects in expressions or initializers each time an object is modified multiple times between two sequence points.

 

RuleChecker:

* Improved the checks for rules MISRA-C:2004 rule 5.2 and the customer-specific rule X.A.5.14 (check identifier-hidden), MISRA-C:2012 rule 5.3 (check distinct-identifier-hidden), and MISRA-C:2004 rule 1.1 (check max-locals) w.r.t. to compound expressions (GCC extension). The improvements remove false alarms about violations of these rules.

* Improved the check distinct-identifier-hidden to remove false alarms about violations of MISRA-C:2012.rule 5.3.

* The option allow-signed-constant-with-unsigned now also suppresses alarms about the operands of <<, >> and ~.

* The option allow-boolean-constants now also suppresses alarms about equality checks (==, !=) between the essentially Boolean values and 0 or 1.

* Fixed false alarm at the last statement in a compound expression (GCC extension) for rules M.14.2 and M2012.2.2.

* Fixed false alarm for MISRA-C:2012 rule 8.3 in case of forward-declared struct tags.

* The check identifier-unique-tag for MISRA-C:2012 rule 5.7 no longer raises false alarms about forward declared tags.

* Fixed crashes that could occur on very large compilation units.

* Improved precision for pointer dereferences in the side effect analysis. This yields fewer false alarms about violations of the checks evaluation-order and expression-order and fewer false notifications about ambiguities due to side effects in expressions or initializers.

* RuleChecker now also reports violations of the checks evaluation-order and expression-order each time an object is modified multiple times between two sequence points. This affects MISRA-C:2004 rule 12.2 and MISRA-C:2012 rule 13.2.

 

Frontends:

* Fixed the parser for original source files to allow the character sequence ? inside of string literals.

* Fixed handling of source files with inconsistent line endings.

 

KNOWN ISSUE:

Invoking Astree via the AbsInt Toolbox for TargetLink fails with an error message "SWITCH expression must be a scalar or string constant.". This may happen if older AbsInt Toolbox preferences already exist for the model, i.e., a file astree_preferences.mat exists in the folder of the model.

 

WORKAROUND:

1) Open the "AbsInt->Astree->Preferences ..." dialog and close it via the "OK" button.

or

2) When invoking Astrée from an m-script, call the m-script API function SetDaxVersion('17.04'); on the AbsInt manager object before starting the analysis.

 

Home Products Absint AbsInt Failure Notice: Astrée for C

Our Location

1

Joral Technologies Inc
4322 Donnelly Rd.
Ottawa, Ontario
K0G 1J0 Canada

Tel: 877-380-3366, Mail: robert.campbell@joraltechnologies.com
2

Joral Technologies Inc
39555 Orchard Hill Place Suite 600
Novi Michigan
48375 USA

Tel: 877-380-3366, Mail: robert.campbell@joraltechnologies.com

Joomla! Debug Console

Session

Profile Information

Memory Usage

Database Queries