Joral Technologies Inc.


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

Absint Products

AbsInt provides advanced development tools for embedded systems, and tools for validation, verification and certification of safety-critical software. For more information on AbsInt products, please visit the EmbeddedShop.

exclamationNew Releases

Astrée Datasheet

Thursday, 23 March 2017 19:12

Astrée is a parametric static analyzer designed to prove the absence of runtime errors
and data races in software programs written in C. Astrée is parameterizable and can be
specialized to the program under analysis – key features to enable high analysis precision.

SAE World Congress Tuesday, April 4.

Room 320 Time: 2:00 p.m.

Cobo Center Detroit, Michigan, USA

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


11/24/2016 Failure Notice: Astrée for C

Monday, 28 November 2016 16:40

Problem Description:

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".

 Affected versions:


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:

 Linux 64-bit:




Windows 64-bit:






- Windows: double-click on the downloaded executable

  and follow the on-screen instructions.

- Linux: unpack the downloaded archive using "tar xzvf",

  change into the newly created directory and run

the shell script "" there.

Windows Installation Note:

If you encounter the following system error during installation: The program can't start because api-ms-win-crt-runtime-l1-1-0.dll is missing.

Then please install the Visual C++ redistributable for Visual Studio 2015.

For more information refer to the following website:

License Management


Please use your existing 'license.dat' file.

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 This email address is being protected from spambots. You need JavaScript enabled to view it. .


Page 1 of 14

Home Products Absint Products

Our Location


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

Tel: 877-380-3366, Mail:

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

Tel: 877-380-3366, Mail:

Joomla! Debug Console


Profile Information

Memory Usage

Database Queries