!=, <, >) in octagons.
- Synthetic (internal) variables are now automatically
inserted into octagon packs.
- Trace partitions created in a function call can now survive
the function return if the call is preceded by
__ASTREE_partition_control.
- Context descriptions (e.g. in alarm messages) now also contain loops
that are not unrolled. Such loops appear as
loop@XXX>=1.
- Implemented the evaluation of constant conditional expressions
(e.g.
const int i8 = 0 ? -1 : 7) when running the analyzer
with constant folding disabled (simplify=no).
- Improved the use of octagon constraints when reporting
potential runtime errors. This allows the analyzer to automatically
remove alarms for code such as
if (a - b > 0) { d = c / (a - b); }
- Improved location information in some alarms to precisely
refer to a certain operand in a comparison or arithmetic expression.
- Improved the precision of modulo computations with pointers
such that the result of evaluating expressions
like
((unsigned int) ptr % 4) is in the expected positive range
([0,3] in this example).
- The precision of notifications about potential ambiguities
due to side effects in expressions has been improved, so that
the analyzer now reports fewer false positives. The corresponding
message has been renamed from “Potential side effects in expression”
into “Potential ambiguity due to side effects in expression”.
- A new category of alarms,
ALARM(D), has been added
to represent messages about uninitialized variables. As messages
of this kind do not represent run-time errors, they do not influence
the behavior of the traffic lights. As long as there are no errors
and only alarms of class D, the traffic lights remain green.
- The identifiers “
asm” and “packed”
are no longer treated as keywords.
- The analyzer now allows the construction of pointers to undefined functions.
Such pointers are then invalid.
Options
- The analyzer now warns about incompatible combinations of options.
- New options:
fold-contiguous-fields
allows to treat
sets of contiguous structure fields of the same type as arrays
for the purpose of smashing.warn-on-undefined-remainder
enables
warnings when computing (signed INT_MIN % (-1))
which is undefined according to the 2011 revision of the C norm.export-fold
controls whether all contexts
should be joined before exporting invariants in order to reduce
memory consumption, thus enabling the use of tool tips and the
watch window for much larger projects.dump-dataflow
allows to specify whether
data flow information should be collected during the analysis run.fields-in-octagon-packs=yes
allows adding
structure fields to octagon packs.interproc-oct-packs
allows interprocedural
octagon packs.
Directives
- The
__ASTREE_absolute_address directive now accepts
absolute address specifications with standard suffixes like 0xfffff0000u.
- Added new directive
__ASTREE_check
which behaves like __ASTREE_assert,
except that it doesn't restrict the ranges of checked variables.
- The
__ASTREE_partition_begin directive has been optimized
for enum types. Instead of partitioning all possible integer values,
it partitions the possible enum values and the ranges between them.
Thus, partitioning according to variables of enum type becomes feasible
even if the analyzer must assume a large number of potential values
for these variables.
- Fixed the order in which AAL annotations
from different annotation blocks are inserted.
GUI
- A single click on a file in the Project tree opens it only if
the file has already been downloaded from the server. Downloading
a file from the server is triggered by a double click.
- The result views now use the system default for mouse clicks.
On most systems items now react on double click.
- Inline assembly statements which are not filtered but automatically
ignored by the analyzer, e.g.
__asm("addl $4, %esp");
are now also marked in the GUI as being filtered.
- The watch feature has been generalized to display not only
plain variables but also more general lvalue expressions,
e.g.
*var, var.field, var->field,
var[N], etc.
- The original source view can now display HTML formatted
source files generated by TargetLink or Embedded Coder.
Thus it becomes possible to jump from the original source
code view in Astrée directly into the Matlab model.
- The editor tab size can now be configured in the preferences dialog.
- When synchronizing files between the local machine and the server,
error messages of the GUI now state which local files are missing
and which local files are identical to the server files.
- The Preprocessing view now accepts defines that include
whitespace characters (e.g.
UINT=unsigned int).
- When setting up a new project, the list of files to analyze
can now be given as a text file. Each file must appear on a separate line.
Server
- Improved client–server communication to prevent
unexpected connection aborts.
- The server now takes additional precautions to avoid
damaging its configuration files when the hard drive is full.
- User-specific information is now attached to a certain
Astrée installation instead of a host name. Hence,
the local settings of users are now preserved even if the host name changes.
Qualification Support Kits
Fixed misspellings and inconsistencies in the VTP and TOR documents and the test reports.
Other improvements
- All defines in the example C stub library are now guarded
to prevent collisions when preprocessing source code which
sets standard defines before including standard headers.
- When running an analysis in batch mode with the option
-u,
the execution now stops with an error code (an exit code that is not equal
to 0) if some local files are missing. In addition, a detailed description
of the error is printed into the report file (specified via the option
--report-file).
Bug fixes
- Fixed assertion failures when activating dynamic smashing and uninitialized warnings.
- Fixed Boolean packing heuristic to avoid very high analysis times on certain code.
- Fixed evaluation of assignments in which one or several variables appear on both sides and a post increment operator appears on the right-hand side (e.g.
i = A[i]++).
- The list of files to exclude from the total coverage computation had not been stored on the server. This has been fixed.
- Fixed handling of local settings to avoid that they are:
- lost after upgrade to release 12.10,
- overwritten when modifying an analysis with the same user from a different machine, or
- not copied when creating a new revision of a project.
- Fixed sporadic issues with the highlighting of failed assert directives that were inserted via the AAL annotation language.
- Corrected some cases when the mapping to original sources was not working as expected.
- Fixed unjustified messages about "definite runtime errors" that could occur in rare cases when the octagon domain was enabled.
- Fixed the display of original source code in case of parse errors.
