Astrée release 14.04

  • The XML reports of different analyses or different versions of the same analysis can now be compared with respect to options, directives, source files, and numbers of alarms and errors, using the XML differences viewer which is available from the tools menu. The differences viewer can also be accessed from the analysis history dialog to inspect the differences between different revisions of an analysis.
  • The analyzer can now detect and warn about write accesses to variables which are possibly not read between two write accesses (write-after-write). This feature is controlled by the new option warn-on-write-after-write.
  • The GUI can now save the project configuration in a DAX file. This feature is available via “Project” → “Export” → “Project...”.
  • The new External Declarations view allows to specify types and (function) declarations that are missing, e.g. because they are part of compiler-specific extensions, or because some include files are not available to the analyzer. One use case for this feature is for generating stub functions for compiler intrinsics. When providing the analyzer with a suitable function declaration via the External Declarations view, it can automatically generate a stub function if the option auto-generate-stubs is used.
  • The new directive __ASTREE_partition_ranges((e:a1,...,an)) allows partitioning an expression e according to a list of intervals a1,...,an. The alternative syntax __ASTREE_partition_ranges((e1;min_size=e2;max_partition=n)) automatically generates partitions covering the range of the expression e1 using the minimal size specified by e2 and/or the maximum number of partitions n.

Qualification Support Kits

  • QSK test cases can now be implemented via DAX files.
  • A qualification run now logs the name of the QSK package into the message window and the report file before starting to execute its test cases.
  • Implemented support for non-ASCII characters in QSK package installation path.
  • QSK test cases are now sorted by ID.

  • The detection of shared variables has been improved so that it is now possible to have two tasks using the same entry function. This brings about a modification of the __ASTREE_asynchronous loop directive, which now requires all tasks to be listed explicitly. Hence, analysis wrappers of the following form are no longer valid:

    typedef void(*t)(void);
static t tasks[] = { t1, t2 };

unsigned int idx;
__ASTREE_known_fact(( idx < 2 ));
__ASTREE_asynchronous_loop(( tasks[idx]() ));

    The correct way for re-writing the above analysis wrapper example is:

    __ASTREE_asynchronous_loop(( t1, t2 ));

    The wrapper generator in the GUI has been modified accordingly.

  • Fixed the AAL processor so that it allows inserting __ASTREE_partition_control statements before assignments.
  • Fixed the calculation of coverage information and number of statements for analyses that use the option auto-generate-stubs=yes.

  • Improved the precision of the analyzer on barycentric computations of the following form:

    in1 = [-1.1];
in2 = [-1,1];
  while (1) {
    b = [0,1];
    out = b * in1 + (1 - b) * in2;
    if (*) in1 = out;
    if (*) in2 = out;
  }

  • Astrée now issues an alarm when an expression may write to a string literal in which case the behavior is undefined and the program may even crash. Here is an example:

    char *s = "Sky";
s[0] = 's';

    The result of Astrée:

    ALARM (A): write to constant: writing to string literal "Sky".
    Definite runtime error during assignment in this context.
    Analysis stopped for this context.
  • If an AAL annotation cannot be inserted, the analyzer no longer stops but reports an error message and continues with the analysis.
  • The precision of the domain of boolean relations has been improved. In particular, the analysis of guards in tests is now more precise.
  • The option cut-invalid-pointer has been removed.
  • The new expert option dump-hypotheses=[yes|no] controls whether the analyzer output contains additional sections that list all semantic hypotheses and further directives. It is provided so that the size of the analyzer output can be reduced when running analyses with very large numbers of directives. However, it is recommended to leave the option enabled so that the result documents the semantic hypotheses on which the correctness of the analysis result relies.
  • Improved the precision of the analyzer when analyzing conditional expressions using the bitwise OR operator.
  • Improved precision on pointers when casting them as integers.
  • Initialization of global variables to 0 can now be activated independently of the initialization option for static variables. That is, even with static-initialization=no and global-initialization=yes, the non-static global variables will now be initialized to 0.

Client

  • Modified the automatic wrapper generator for TargetLink so that the root step functions of the model can be called in arbitrary order.
  • The text search feature of the GUI can now also search the original source files, not only the preprocessed files.
  • Modified the filtering (Ctrl+F) in the Summary/C view so that filters now consider the names of the categories, not the alarm messages.
  • Modified the filtering (Ctrl+F) in the Summary/F view so that filters now consider the names of the files, not the alarm messages.
  • A new standard example demonstrates automatic detection and sound analysis of shared variables in asynchronous tasks.
  • Filtered expressions are now highlighted in the editor also when the analysis was not successful.
  • The original source files of an analysis project can now be downloaded from the server from the context menu of the original files list.
  • Re-designed the preprocessing dialog of the GUI to improve usability, performance, and flexibility.
  • Fixed sporadic crashes when deleting configurations from the Preprocessing view.
  • Improved warning message when some reports could not be generated.
  • It is now possible to reorder the entries in the Parser view using drag and drop.
  • Improved performance and reduced memory consumption when loading information about not analyzed code in the client.
  • A tooltip in the Coverage column of the Summary/F view now displays the number of statements that were not analyzed together with the total number of statements in the file.
  • The Alarm density view can now be filtered such that it displays only functions with more alarms than a given threshold.

Server

  • Fixed the automatic upload of original source files to the server after preprocessing. Instead of uploading only the C files from the list of files to preprocess, it now also uploads all included header files.
  • Locating the original source files for large analysis projects is much faster now.
  • Fixed a bug that could cause the upload of original source files to overwrite some of the preprocessed files on the server.
  • The uploading of source files to the server has been optimized to reduce transfer times.
  • Reduced server startup time on working directories with many large projects.
  • Improved the error message for client/server connection failures due to version mismatch.