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.
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
CONTENT Astrée - Handling Absolute Addresses - Analysis of Concurrent Software - Improvements in the Astrée Client (GUI) - Reporting - Rule Checking - Further Improvements
CONTENT a³ - a³ Workspaces o Save complete analysis state & results (graph, statistics,…) for later review o Workspace export in alauncher (Option: --export-workspace ws.apx ) - Automatic Generation of AIS annotations from o Graph/GUI o Message View (as annotation hints) o AIS Editor - Loop Bound View in Statistics and AIS annotation generation - Project File Generator from built-in Editor and Information Views - Stack area specification in GUI - a³ Jenkins Plugin - Extended AIS2 annotations for o Initialization Value Analysis o Handling Tail Calls o New end/offset functor