Welcome to JORAL Technologies Safety Critical Tool Department.
This department is set up to support Software Engineers dealing with Safety Critical Applications. We offer free product demonstrations for all products.
Finding all Potential Run-Time Errors and Data Races in Automotive Software. The focus of the session is on system safety analysis and design of safety- critical systems employing electronic controls. Topics include: implementation of safety-relevant systems, fail-safe strategies, distributed fault tolerant systems and hazard analysis. Application areas include: automotive active safety and alternative energy systems as well as avionics and mission management. Finally, the session addresses application of new or revised safety standards such as ISO 26262 and DO-178C.
Daniel Kaestner, Absint Angewandte Informatik GmbH
When using the ABI option rounding_mode=to_nearest the analyzer may yield incorrect results when evaluating guard expressions that involve binary operations on floats.
The erroneous analysis behavior is triggered by the following code patterns:
x <cmp-op> (y1 <bin-op> y2)
<x1 <bin-op> 2> <cmp-op> y
(<x1 <bin-op> 2>) <cmp-op> (y1 <bin-op> y2)
where <cmp-op> and <bin-op> are compare or binary operators, respectively, and x, x1, x2, y, y1, y2 are floating point expressions.
Here is a minimal example:
int x = 0. > (1. - 0.005);
The analyzer may calculate locally incorrect roundings for the affected expressions. As a consequence some program behaviors may not be covered by the analysis. In most cases the analysis will stop in affected analysis contexts and produce a notification message of the form "NOTE: Direct flow changed to _|_ during test in this context".
All releases between 15.04 b240245 and 16.10 b269715.
Earlier releases do not provide the ABI option rounding_mode.
As a workaround change the ABI setting rounding_mode to its default value rounding_mode=all.
A corrected version of Astrée is available for download:
If you have not received a 'license.dat' file yet, copy the host ID from the license dialog and paste it into an email to