a³ Release 13.10
----------------
Targets
-------
* aiT for MPC56xx now supports MPC5674F.
* aiT for ARM now supports Cortex-R4F.
* a³ for H8 has been discontinued.
General
-------
* Safety Manual for aiT, StackAnalyzer, and Astrée released.
The manual gives a detailed overview of DO-178B, DO-178C, and ISO-26262
with respect to runtime error checking, as well as to timing and
storage-space constraints. The verification objectives met by aiT,
StackAnalyzer, and Astrée are listed. The tool 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.
* Tool coupling between aiT, StackAnalyzer, and TargetLink from dSPACE
released. The information stored in the TargetLink Data Dictionary
is automatically exploited to provide information about interface
and environment to AbsInt’s analyzers. This improves analysis precision
and reduces manual effort.
* The new AbsInt Tool Box lets Matlab/Simulink users launch aiT, StackAnalyzer,
or Astrée analyses from TargetLink with a single mouse click.
* Implemented support for OSLC export of analysis results.
AbsInt Launcher
---------------
Added launcher option "-g" to combine suitable XTC requests
into a single call to a³.
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.
* 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.
* 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.
==============================================================================
Last modified on 7 November 2013 by alex@absint.com.
Copyright 2013 AbsInt. http://www.absint.com/
==============================================================================
An HTML version of these release notes is available at
http://www.absint.com/releasenotes/a3/13.10/