a³ Release 16.10

● The Windows version now makes use of certain libraries
  it did not rely on before. Should you get a message about
  missing libraries on first startup, simply install
  the Visual C++ redistributable from Microsoft:
  In an upcoming release, the a³ installer will be updated 
  to include this package.
● A free plugin is now available for automatic integration
  of a³ in Jenkins, the leading open-source automation server:

● The alauncher executable is now used for automation of a³ and Astrée
 (running analyses in batch mode, e.g. within continuous-integration systems).
  It provides a verbose --help.

● The Safety Manual now also covers regulations for medical devices,
  in particular the FDA Principles of Software Validation.

● The Safety Manual now describes qualified tool workflows for a³ and Astrée.

● StackAnalyzer and ValueAnalyzer now available for TI MSP430(x).

● aiT for ARM now supports Infineon XMC4500 (Cortex-M4 core).

● aiT for C28x now supports TMS320F28035, ...335, and ...069.

Qualification Support Kits
● New QSKs now available for:

  ○ aiT and StackAnalyzer for ARM, THUMB2 instruction set,
    generic and compiler-specific for GCC 4.9.3
  ○ aiT and StackAnalyzer for C16x,
    compiler-specific for Tasking VX 2.4r1

● Removed test for pipeline analysis widening threshold
  as this option has been removed.

● Implemented test cases for AIS2 language constructs.

Integration with TargetLink
●"Import Result from XTC File" now puts the result
  into a new AbsIntAnalysisResults element of the function
  instead of writing to the function's properties directly.

● Improved generation of loop-bound annotations for lookup tables.

You can now save the current analysis state, any results computed so far,
and all currently open views as a so-called Workspace.

Unlike simply saving a project, this allows you to take snapshots
of your progress at any moment in time, revisit them, and build upon them.
This is especially useful for documentation and backup purposes.

In the user interface, this new feature is accessible via "Project" →
"Save as workspace".

In batch mode, you can export analysis results as a Workspace via

  --export-workspace <workspace.apx>

Then all graphs, statistics and any other output produced so far
can be immediately accessed in the GUI without having to re-run
the analyses first.

Point-and-click annotations
Annotating your project is now easier than ever before.
Whether you are looking at a graph or a statistics table,
simply right-click on a routine or loop and select "Add annotation"
from the context menu.

You will then be taken straight to the AIS file, with the selected
annotation already typed out for you. Now simply fill in the values
as desired, and you're done.

Likewise, in the AIS editor itself you can now use "Insert AIS annotation"
from the context menu to add further annotations, rather than typing
everything by hand.

Annotation hints
a³ now automatically determines any locations that might benefit
from being annotated, and marks them for you with a light bulb
in graphs and messages.

Clicking on that symbol will bring up the suggested annotation,
and another click will add it to your AIS file.

The annotation hints are also included in analysis reports
for documentation purposes.

Below are some examples of messages with annotation hints.
Placeholders enclosed in angle brackets are highlighted in the GUI
and can be double-clicked on to enter values of your choosing.

● Missing call targets:

  exec2crl: Info #1027: In "error.c", line 41:
    In routine 'os_ErrorHook', at address 0x180138c:
    Unresolved computed call in routine os_ErrorHook.
    Annotation hint:
    ais2 { instruction "os_ErrorHook" -> computed(1) { calls: <targets>; } }

● Missing loop bounds:

    Info: In routine 'main.L3', at address 0x1001b4:
    Loop 'main.L3' is unbounded.
    Annotation hint:
    ais2 { loop "main.L3" { bound: 0 .. <int>; } }

● Missing incarnation bounds:

    Warning #3097: In "fibfac.c", line 1:
    In routine 'fac', at address 0x180029c:
    For routine 'fac' the default incarnation limit of 1 is used.
    Please verify that this is correct.
    The recursion details are:
              0: main
              1: fac
        ->    2: fac
        ->    3: fac
    Annotation hint:
    ais2 { routine "fac" { incarnation limit: 1; } }

Improved statistics
● All-new Statistics view for minimum and maximum loop bounds
  for all loops globally and for each context.

● Improved WCET statistics with bar charts for self contributions
  and cumulative contributions.

● The infeasibility statistics view now shows if a routine
  is top-level infeasible, backwards infeasible or just infeasible.

● In the Graph view, loop statistics and other analysis details
  are now linked from the context menu of routines and loops.

Other GUI changes
● Message view colors and fonts have been optimized to highlight warnings,
  errors, annotations hints and locations.

● Analysis results are now always output in all available formats.
  For example, even if you haven't specified a report file, it will
  still be created in a temporary directory and can be shown on request.

● When creating analyses from an information view, a template dialog
  is now displayed that enables you to customize the generated analyses.
  In addition, you can now mass-create analyses simply by typing up
  the list of entry functions in any editor view and using the context menu.

● When visualization of recursions is enabled (selected in the combo box
  in the Graph view), any incoming edges into any recursions are now
  also highlighted in a different color.

● Register values (e.g., stack pointer) can now be specified using
  AIS2 expressions.

● You can now specify an address range where the stack pointer
  can be placed. This will usually increase analysis precision.

● Added a progress indicator for reading DWARF debug information.

● Improved Memory Usage view.

  ○ The memory usage is now broken down by category.
  ○ You can now toggle the view between overall usage
    and that of the current analysis.

● Improved configurations management and problem reporting.

● Macro information from DWARF debug information is now read
  on-the-fly to reduce memory consumption.

● Information → Sources now shows DWARF producer information,
  if available, for the individual source files. This makes it easy
  to check which compiler is used for which file. Some compilers
  include the compile options there, too.

● Improved ORTI project import:

  ○ now supporting architectures with multiple stacks
  ○ you can now specify a global AIS file
    and source file include directories
  ○ better computation of task entry function names

● Improved import of configurations with old settings.
● The option "Size limit for interval sets" has been renamed into
 "Size limit for value sets". Old settings will be imported and converted.

● The AIS1 format is now officially deprecated.
  If you need help converting AIS1 annotations to AIS2,
  contact support@absint.com.

● New annotation to directly specify call targets
  and declare that a call is a tail call:

    instruction <pp> tail calls: ...;

● The annotations "instruction calls/branches to/returns to"
  now have an implied instruction class. For example,

    instruction <pp> calls: ...;

  also changes the instruction type of <pp>
  to call, just like the annotation

    instruction <pp> type: call;

  This means that the annotation

    instruction <pp> {
      calls: ...;
      type: tail call;

  can now be simplified to:

    instruction <pp> tail calls: ...;

● Initialization values can now be collected for all structure members
  at once by specifying:

    collect initialization: ("<name>".);

  where <name> is the name of a structure variable.

● New AIS2 expression to compute the end address of an address range.
  Instead of writing:

    address(<area>) + width(<area>) - 1

  you can now simply write:


● New AIS2 functor to determine the offset of a structure field
  in a global structure variable. For example, to determine the offset
  of a structure field "data" in a global structure variable "fTable",
  the following expression can be used:


  This expression is a shorthand for

    address(("fTable"."data")) - address("fTable");

● The "collect initialization" annotation has been extended
  to enable collecting values for specific types, for example:

  ○ values written into function pointer variables

      collect initialization: type(function pointer)

  ○ values written into variables of type "void () *"

      collect initialization: type("void () *");

  ○ values written into variables that match a regular expression

      collect initialization: type("int.*");

● Improved error reporting in case a pointer dereference operation,
  e.g., in an annotation to resolve a computed call, fails to read
  data from memory. For example, consider the annotation

    instruction "main" -> computed(1) calls: *("b"[]);

  When the AIS2 resolver is unable to read data from memory,
  it previously reported:

    At address 0x1000380:
    Unable to resolve '("b"[]->)':
    - Unable to read target address from '0x40028b60'.

  Starting with this release, it will also explain why the data
  cannot be read, and even provide annotation hints when necessary:

    At address 0x1000380:
    Unable to resolve '("b"[]->)':
    - Refusing to read 4 bytes at address 0x40028b60 (variable 'b')
      from writable section '.sdata' to reconstruct the control flow.
    You may need to annotate branch/call targets in case it is.
    Additionally, you should check whether section is writable.
    Please consider writing an AIS annotation.
        ais2 { area section(".sdata") { readable: true; writable: false; } }

● Improved handling of calls via trampoline routines: "skip target check"
  can now be annotated at the original call site instead of the return
  inside the trampoline routine.

● Improved handling of interval area contains annotations.
  Either an unsigned or signed interval fitting into the destination width
  is allowed. If that constraint is not met, the decoder will issue a warning.
  Given a 32-bit wide element, feasible annotations are:

    ais2 { area 0x100C to 0x100F { contains data: 0x1 .. 0xFFFFFFFF; } }
    ais2 { area 0x100C to 0x100F { contains data: -123123 .. 1212435; } }

  Out-of-range annotations would be e.g.

  ○ ais2 { area 0x100C to 0x100F { contains data: -123123 .. 2147483648; } }

    resulting in

    Ignoring contains data annotation because signed cell value
    [-123123..2147483648] exceeds cell width of 4 byte.
    The allowed range is [-2147483648..2147483647].

  ○ ais2 { area 0x100C to 0x100F { contains data: 0x0 .. 0xFF0000000; } }

    resulting in

    Ignoring contains data annotation because unsigned cell value
    [0..68451041280] exceeds cell width of 4 byte.
    The allowed range is [0..4294967295].

● Improved performance of program point resolution for
  match(<regular expression>).

● Improved DWARF debug information extraction and usage,
  especially for C++ debug information.

● Now supporting binaries with mixed DWARF1 and DWARF2 line information.

● Extended DWARF debug information reader to show structure types
  with flexible array members.

● Support ELF files with more than 65535 program or section headers.

● Decoder now reports annotated register contents,
  such as the user stack pointer.

● Derive byte order of additional executables (e.g. HEX files
  for calibration) from main executable.

● The '.text' section is now automatically marked as read-only
  for Coff binaries.

● Better heuristic for symbol table reading in Coff binaries
  to sort out not-needed symbols.

● Improved stack pointer guessing for GCC.

● Improved handling of debug line information for binaries
  with relocations if line info points to the relocated code
  and not the original location.

● Improved handling of non-contiguous data sections in IEEE965 reader.

● Allocated sections without content are marked as writable per default.

● Empty sections are now discarded.

● ARM:

  ○ improved decoding of switch tables via thumb tbb and tbh instructions
  ○ improved decoding of computed calls and branches
  ○ improved patterns for computed calls in THUMB mode
  ○ allow more variants of VFP instructions
  ○ better TI compiler detection for Coff binaries.
  ○ improved stack pointer guessing

● C28x:

  ○ improved zero overhead loop handling
  ○ improved stack pointer guessing

● C33: improved stack pointer guessing.

● FR81: added support for FeOMF debug information.

● MPC7448 and 7448s: support for code duplication.

● PPC:

  ○ improved decoding of VLE binaries
  ○ improved call/switch table decoding

● SuperH: improved decoding of computed calls and branches.

● TriCore: improved decoding of switch tables.

● V850:

  ○ improved decoding of computed call tables
  ○ improved handling of code factorization optimization of GHS compiler
  ○ improved read/write classification of store instructions
  ○ added support for full 22-bit offsets in jarl/jr instructions

Stack and value analysis
● Improved memory usage and analysis speed.

● Improved precision for:

  ○ value analysis for computed calls with many infeasible targets
  ○ sharpening of expressions containing a + b / a - b / a ^ b
  ○ multiplication and bit extraction instructions
  ○ multiplication emulated via shift-and-add
  ○ the relational domain for shifts and multiplications
  ○ iterative decoding for guarded execution

● Improved reporting for infeasible control flow transitions.
  Symbol names for targets and annotations for the instruction
  in question are now reported, too:

    Warning #3078: In "test.c", line 42:
    In routine 'test', at address 0x110:
    In context '..., 0x020->"test"':
    In "annotations.ais", line 12:
    Detected an infeasible control flow transition.

        Edge (true) from 0x110 to possible targets:
            * [0x0200] (0x200 => 'Test_Function_0')
            * [0x0300] (0x300 => 'Test_Function_1')

        Contradicting computed targets:
            * [0x0400] => 'Test_Function_2'

● Out-of-bound array accesses detected are marked as infeasible
  if DWARF is used to restrict memory accesses. The value analyzer
  will issue a message:

    Info #3118: In "test.c", line 106:
    In routine 'test.L6', at address 0x1310:
    In context '0x1444->"test", 0x1030->"test.L1"[21]':
    The read-access is assumed to access array 'array_test'
    which conflicts with the computed address [0x003f97fc]
    (index is [21], but array has only 20 members).
    Marking this path as infeasible.

● Extended restriction of memory accesses via DWARF debug information
  to arrays which are struct members.

● Improved restriction of array accesses with DWARF debug info
  for architectures with address segmentation.

● Added support for restricting accesses to arrays with element size of 1
  using DWARF debug info.

● Sharpen the register or memory cell used as index for array access
  if DWARF is used to restrict memory accesses.

● Optimized maximum stack analysis path enumeration algorithm.

● Improved reporting for potential infinite loops, now warning
  if they have user-annotated loop bounds.

● Improved simplification for expressions like "((d3 + d4) - d4)".

● Improved collection of initializiation data if values are written
  in steps (triggered by the "collect initialization" annotation).

● Improved combination of relational information on control flow joins.

● Improved loop bound detection.

● Improved heuristic to filter out pseudo loop bounds only detected
  because of casting small loop counters to larger datatypes.

● Improve handling of complex loop exit conditions.

● Improved detection of loop bounds for shift loops.

● Improved output of computed vs. annotated memory contents clashes:

    Warning #3088: In "test.c", line 128:
    In routine 'schedule', at address 0x114c:
    In context '0x1048->"task", 0x104c->"schedule"':
    Write access to [0x00810000]:4 ('globalVariableName')
    in constant memory contradicts user annotation.

        Annotated value:
            * [0x00000000]

        Contradicting computed value:
            * [0x00000001]

● Improved performance of context mapping computation.

● ARM: improved handling of SP writeback for SRS instructions.

● C16x: restrict accesses of the form

    <base> + <index> * <factor>

  to the segment indicated by <base>.

● MCS51: improved modeling of memory-mapped registers.

● SuperH: improved stack analysis of external routines.

Cache and pipeline analysis
● Improved speed and memory consumption.

● Greatly improved performance for small max-length values.

● Improved performance and precision for additional starts.

● Now avoiding unbounded results for additional starts
  in combination with small max-length values.

● Removed the "Enable widening for cache states" option.

● Cortex-R4: improved pipeline model.

● Cortex-R5:

  ○ Improved pipeline model.
  ○ Return stack now supported in timing analysis.

● MPC5674F and 5777M(z7): improved handling of memory serialized instructions.

● PowerPC: improved stability of TimingProfiler analysis
  for variable instruction length code sequences.

● e300, MPC755, MPC755s, PPC750: improved cache-hit counter computation
  for writes into locked memory areas.

● MPC7448 and 7448s: added code-duplication support.

● Cortex-R: improved memory map and pipeline model for TimingProfiler.

● The "Reduce number of identical messages" option was removed
  in favor of dynamic filtering in the GUI. You can hide duplicates
  directly in the Messages view, but will now be able to unhide them
  without re-running the analysis.

● Suppressed messages for each analysis step are now reported via

  ○ info messages in the GUI:

      Suppressed messages: #3079 (2×), #3082 (4×)

  ○ report files:

      *** Suppressed messages: #3079 (2×), #3082 (4×)

  ○ XML report files:
      <suppressed_message number="3079" suppressions="2" />
      <suppressed_message number="3082" suppressions="4" />

● Text and XML reports now include information on completely infeasible
  contexts for a routine as an extra column/attribute.

● Potential reasons for not-computed results of timing analysis
  are now reported.

● The a³ XML Result File format has been revised. The structure
  is more consistent now. The new XML scheme definition file can be found at

● Faster initial creation of control flow graphs.

● Improved memory usage.

● Improved "Go go caller/target" context menu for calls/routines
  with many targets/callers.

Last modified on 14 October 2016 by alex@absint.com. Copyright 2016 AbsInt.
An HTML version of these release notes is available at