a³ Release 13.10

New Statistics views

Non-WCET cycles in XML

Customizable AIS prefix

General
GUI
Annotations and decoding
Analyses
Plain text

Targets

aiT for MPC56xx now supports MPC5674F.
aiT for ARM now supports Cortex-R4F.
a³ for H8 has been discontinued.

Safety Manual

The all-new Safety Manual for aiT, StackAnalyzer, and Astrée gives a detailed overview of DO-178B, DO-178C, and ISO 26262 with respect to checks for runtime errors, timing and storage-space constraints.

The verification objectives met by aiT, StackAnalyzer, and Astrée are listed. The qualification strategy for these tools based on QSK and QSLCD is detailed and shown to satisfy the requirements of the respective standards.

The Safety Manual is linked from the Welcome page and the Help menu.

Integration with TargetLink

Initial release of a tool coupling between aiT, StackAnalyzer, and TargetLink from dSPACE. The information stored in the TargetLink Data Dictionary is automatically exploited to provide details about interface and environment to AbsInt’s analyzers. This improves analysis precision and reduces manual effort.

The new AbsInt Toolbox lets Matlab/Simulink users launch aiT, StackAnalyzer, or Astrée analyses from TargetLink with a single mouse click.

AbsInt Launcher

Added launcher option -g to combine suitable XTC requests into a single call to a³.

OSLC support

Implemented support for OSLC export of analysis results.

GUI

The results statistics moved back from the standalone Results Viewer to the main analyzer window.
When navigating from GDL graph to source code, the GUI now correctly reports if the destination file does not exist.
Removed the option to specify a custom XML style sheet. Instead use a custom XSLT processor to apply style sheets.
Optimized generation of HTML reports, especially for larger projects.
QSK package extraction now features a progress bar.
Default installation path for QSK packages has been changed to the user’s home directory.
The Sections view now correctly displays section contents of architectures with quantas larger than one byte (e.g. C33).
Better error reporting for Results Combinator analyses.
New value analysis option “Size limit for unsharp reads”. For every read access, value analysis determines a set of possible addresses. To obtain information about the result of the read access, the value analyzer may enumerate the set of possible addresses, look up the value information of all possibly addressed memory cells, and join the results together. The new option specifies an upper limit for the application of the enumeration method.
The Functions view now displays the entry address of each function, as well as information on its return type (if known and non-void).
MPC7448(s)/E500/PPC750: Changed default bus clock ratio from 1:4.5 to 1:4.
Improved Variables and Functions views.

AIS

The AIS1 expression before is deprecated and should no longer be used.
Added the "instruction <pp> target preserves <..>" annotation that works analogously to "routine <pp> preserves <..>".
Fixed AIS switch expressions without default case, which failed to evaluate.
Fixed AIS2 parser issue where AIS2 annotation scopes (ais2 { ... }) could only have a limit size of 16KiB.
The "calls via" annotation now supports different array sizes per "calls via" level.
The prefix for AIS source-code annotations is now customizable. See screenshot.

AIS2 now supports "calls via" where entries can be skipped by means of a conditional expression. Example:

instruction "main" -> computed(1)
  calls:
    via ("FunctionTable") {
      struct:  16 byte;
      offset:   8 byte;
    }
    via {
      struct:   8 byte;
      offset:   4 byte;
      skipped:  mem(address(element), 1) != 0;
    };

Improved precision of expression evaluator.
Added support for expressions in timing annotations for loops.

Decoding

Improved iterative decoding approach by combining results of previous decoding rounds.
Improved exclusion of code snippets handling.
Hide debugging symbols like DW$L$... from symbol table in coff files.
Automatic copying of GHS .UNCOMPRESSED.<name> sections to their .<name> companions.
Improved DWARF debug information extraction.
ARM:
- Improved handling of tbb table branches for ARM Thumb.
- Improved switch table and return patterns.
- Improve support for TI compiler.
- Improved handling of mode switch via blx <constant> ARM => Thumb.
C16x: Improved switch table decoding (Tasking VX compiler).
C33: Improved switch table and return pattern detection.
MicroBlaze: Support for little endian binaries in addition to existing big endian support.
PPC: Support decoding of EFPU 2.0 Extensions instructions.
TriCore: Improved HighTec GCC support for resolving indirect computed calls via arrays of structs.
X86: Implementation of switch table support for gcc-4.4.5.
V850:
- Improved switch table patterns.
- Correct handling of the following E2/E3 ISA load/store variants (load/store now full value, not only 1-byte):
  - ld.h, 6-byte opcode
  - ld.hu, 6-byte opcode
  - ld.w, 6-byte opcode
  - st.h, 6-byte opcode
  - st.w, 6-byte opcode

Stack and value analysis

Introducing improved loop and value analyzer for C28x, FR81 and MicroBlaze. The key features are:
- Improved interval domain — sign-agnostic wrapped interval analysis.
- Improved handling of binary operations like bit-wise and/or/xor.
- Generalized symbolic relations between register-memory, register-register and memory-memory.
- Improved branch splitting.
- Generic loop analysis for all supported targets.
- Precision improvements for 64-bit integer arithmetic.
- Improved stack analysis with better handling of stack pointer spilling/reloading.
Improved value analysis performance (post-dominator/infeasibility analysis).
Improved precision on writes to unsharp addresses in value analysis.
Included annotated stack effect for external routines in report files and graphs. For example, if an external routine uses 96 bytes of stack and leaves behind 32 bytes of stack, you will get the following output:
Maximum self usage is [32..96] bytes
Now ignoring "area contains" annotations for speculative accesses.
Reduced the number of false positive warnings about unsafe loop bounds, especially for nested loops.
Improved analysis message output to use the correct target size unit, e.g. half-words/words for C28x/C33.
Improved handling of stack analysis annotations during value analysis.
Improved handling of address mirroring for user annotations.
Improved precision for bit-wise XOR.
ARC: corrected the semantics of the following bit test/set operations.
- bbit0 x,n,offset — branch if bit n in register x is zero
- bbit1 x,n,offset — branch if bit n in register x is one
ARM: Improved loop and value analysis precision.
C28x:
- Improved precision of stack analysis for instructions ASP/NASP.
- Suppress superfluous warnings about unknown PAGE0/M0M1MAP/OBJMODE.
M68k: corrected the semantics of the following bit test/set operations.
- bchg n,x — test and change a bit in register/memory cell x (test result in Z-flag)
- bclr n,x — test and clear a bit in register/memory cell x (test result in Z-flag)
- bset n,x — test and set a bit in register/memory cell x (test result in Z-flag)
- btest n,x — test a bit in register/memory cell x (test result in Z-flag)
PPC:
- Improved precision of PowerPC-branch instructions decrementing and testing the counter register in addition the standard condition.
- Improve loop analysis precision.
TriCore: Improved branch splitting.
V850:
- Improved handling of address mirroring in StackAnalyzer for Generic V850E3.
- V850 FX4 and V850 VFORREST now honor the GUI switch to assume that the analyzed program never makes any misaligned memory accesses.
- Corrected the semantics of the following bit test/set operations:
  - clr1 n,x — test and clear a bit in memory cell x (test result in Z-flag)
  - set1 n,x — test and set a bit in memory cell x (test result in Z-flag)
  - not1 n,x — test and invert a bit in memory cell x (test result in Z-flag)
  - tst1 n,x — test a bit in memory cell x (test result in Z-flag)
x86:
- Improved the stack pointer modification pattern for gcc-4.4.5.
- Corrected the semantics of the following bit test/set operations:
  - bt x,n — test a bit in register/memory cell x (test result in C-flag)
  - btc x,n — test and complement a bit in register/memory cell x (test result in C-flag)
  - btr x,n — test and reset a bit in register/memory cell x (test result in C-flag)
  - bts x,n — test and set a bit in register/memory cell x (test result in C-flag)

Cache and pipeline analysis

C28x:
- Improved pipeline model.
- Improved memory access stall handling.
- Improved handling of branches annotated to be boring.
LEON2/3: Improved valid bit tracking for caches of LEON2/3 pipelines.
MPC603e/PPC750/MPC7448s: Improved handling of the AIS annotation “timing_in_bus_cycles” for accesses to PCI.
MPC755(s)/PPC750: pipeline modifications due to results from further trace validation.
- improved fetch idle cycle for predicted taken or taken branches
- emit no prefetch, if lr/ctr-writing instruction has been recently dispatched
- dynamically stall prefetch in case of high LSU load
- emit no prefetch while dispatching a cr-modifying instruction
- improved fetch-store priority handling (755(s) only)
- improved bus access path of uncached stores (755(s) only)
- reopen page in case of tag register hit, if previous access to the same bank has opened a different page (755 only)
TriCore: faster pipeline analysis for TC1796, with reduced memory consumption.
V850: Fixed issue in interactive pipeline visualization for V850E1F.

Visualization and reporting

New option "Output non-WCET cycles" to trigger output of all timing information, including non-WCET cycles, to the XML report file. See screenshot.
Improved output of multiple worst-case stack paths.
XML report filtering issue resolved, some attributes got written to XML file even if their parent tags should have been filtered away. This led to artifacts inside the XML report files if XML filtering was active.
Update of a³ report XML schema: message_type values consolidated and documented.

a³ release 13.10