GNAT Dynamic Analysis Suite 25 Release Notes

We present here a few highlights of the new features in GNAT DAS 25. You can access the complete list in the GNAT DAS 25 feature file.

Code coverage reports

UX for MCDC improved in gnatcov’s HTML report

Clicking on an MC/DC violation message in the HTML report highlights the source-code excerpt of the condition.

Function and call coverage for Ada in GNATcoverage

GNATcoverage is now able to provide coverage analysis of subprograms and calls for Ada. A call is considered covered when it has been executed at least once. A subprogram is covered if it has been entered at least once. This new coverage level can be activated alongside any preexisting coverage level combination, through the use of the “fun_call” option of the “–level” switch. See section 1.5.8 of the GNAT DAS user manual for more details.

Support for restricted runtimes

Widen support for trace file dump in GNATcoverage

GNATcoverage now supports dumping coverage traces to a file on a broader range of Ada runtimes. While previously dumping traces to file also required the Ada runtime to provide a GNAT.OS_Lib unit, the only requirements now are that the runtime must provide a Ada.Text_IO unit, with capability to write to files, and that the C standard library must be available for the target.

Tool integrations

Revamped GNATtest/GNATcov integration Makefile

The Makefile generated by GNATtest for assessing the level of coverage of the generated test harness has been enhanced to offer more flexibility in cross-compilation configurations. Instead of directly attempting to invoke GNATemulator, a shell script is generated for running the test driver executables. This shell script can be modified by the user and will not be regenerated after the first creation. Additionally, intermediate build targets have been added to allow only the instrumentation and build of the test drivers, leaving the execution and consolidation up to the user in the case where the shell script is not appropriate.

Support for the CCG compiler in GNATcoverage

GNATcoverage now supports instrumentation of projects that will be compiled with the CCG compiler. Due to limitations of the CCG runtime, there are some adjustments to the overall coverage workflow compared to a regular cross-compilation scenario, which are outlined in section 1.3.10 of the GNATdas user manual.

GNATfuzz integration with GNATtest

GNATfuzz and GNATtest can now share test inputs via a common test case format in JSON. This allows GNATfuzz to utilize a GNATtest Unit test campaign to generate a starting corpus, and GNATtest can benefit from a GNATfuzz campaign to increase code coverage.

Support for preprocessing

GNATfuzz support for preprocessing

When analyzing the user project under test, GNATfuzz now preprocesses the sources according to the -gnatep and -gnateD switches defined in the project file.

Support for Ada preprocessing in GNATcoverage

GNATcoverage now correctly handles preprocessing directives when instrumenting Ada source code. Instrumentation used to ignore or misplace them.

Selective coverage analysis

Support for disabling coverage analysis

GNATcoverage now supports disabling coverage analysis by means of pragmas (for Ada) or comment markers (for C/C++) when using source instrumentation. This disables the emission of SCOs, and the instrumentation for the designated region.

Support for block instrumentation

GNATcoverage now supports instrumenting block sequences as a whole, with the –instrument-block instrument switch. The source-coverage obligations do not change in this case, only the way they are discharged. If the last statement of the sequence is covered, all the statements of the sequence are marked as covered as well.

Out-of-source annotation support in GNATcoverage

GNATcoverage now has a mechanism to generate companion files to describe annotations concerning the instrumentation process and coverage analysis. This mechanism supports the same set of annotations that can be added to source files with pragma Annotate. This feature may be particularly useful for users who do not have the possibility of modifying their source files as part of coverage-analysis activities. The annotation files can be created and augmented using the new gnatcov add-annotation command. See section 1.9 of the GNATdas user manual for more details.

Handling coverage buffers

New coverage-buffer reset API in GNATcoverage

GNATcoverage now provides an API to specify locations, in the sources, where coverage buffers will be cleared. This can be used to isolate coverage results for multiple executions of a given subprogram without needing to resort to multiple test-driver executions, to avoid incidental coverage between tests, or between setup code and test execution. The buffer reset indications take the form of Annotate pragmas in Ada code, and of specially formatted comments in C or C++ code. See the user manual for further details.

Optionally specify files with manual dump trigger

When using –dump-trigger=manual, the user can now specify the files containing the dump indications with “–dump-trigger=manual,<list_of_files>”, where list_of_files is either a comma-separated list of files or a response file. This speeds up the dump indication replacement by preventing the need to scan the entire source base in search of dump insertion points.

Test case generation from structural data

GNATtest can now automatically generate values as input to test cases based on the structure of subprogram parameters.

GNATfuzz enhancements

Add initial support for private types

GNATfuzz now supports fuzzing Ada private types. For example:

package Test is
   type P_Type is private;
   procedure Foo (P : in out P_Type);
private
   type I_Type is range 0 .. 1;
   type P_Type is array (I_Type, I_Type) of Boolean;
end Test;

Add support to subtypes

GNATfuzz now supports fuzzing Ada subtypes. For example:

package Foo is
   type Bar is private;
   subtype Baz is Bar;
   procedure Qux (F : Bar; B : Baz);
private
   type Bar is
      record
         I : Integer;
      end record;
end Foo;

Beta script for automating project campaigns

A beta script titled “fuzz-everything.py” is provided to generate harnesses and run fuzzing campaigns for all fuzzable subprograms in a GPR project. The results of the campaigns in terms of coverage achieved and test cases found are provided in an outputted JSON file. The script is located in the <install path>/share/gnatfuzz/scripts/testing folder and detailed help can be found by running fuzz-everything.py –help..

GNATfuzz supports symbolic execution

GNATfuzz now includes a symbolic execution engine called “SymCC”. SymCC generates addition test cases that solve complex branch conditions to increase coverage and allow the fuzzer to explore and test more of the user code base.

New script to decode all testcases in a folder

All test cases within a results folder (queue, crashes, hangs etc) can now be quickly decoded using the decode_folder.py script. The script is located in the <install path>/share/gnatfuzz/scripts/testing folder and detailed help can be found by running decode_folder.py –help..

Support for public and private derived types

GNATfuzz now supports the fuzzing of public and private derived types. For example:

package Test is
   type My_Record is record
      I : Integer;
   end record;
   type My_Derived_Record is new My_Record;
   procedure Foo (F : My_Derived_Record);
end Test;

Allow fuzzing of private subprograms

GNATfuzz now supports fuzzing Ada private subprograms. For example:

package System_Under_Test is
   Dummy : constant Integer := 0;
private
   procedure Subprogram_Under_Test (Input : Integer);
end System_Under_Test;

Derived record types with extensions

GNATfuzz now supports the fuzzing of derived record types with record extensions. For example:

package System_Under_Test is

   type Foo is record
      I : Integer;
   end record;

   subtype Bar is Foo;

   subtype Qux is Bar;

   procedure Subprogram_Under_Test (Input : Qux);

end System_Under_Test;

GS support for AFL modes Persist and Plain

The GNAT Studio gnatfuzz fuzz dialogue will now handle the AFL++ DEFER and DEFER_AND_PERSIST operating modes.

Optimizations

Inlining of witness subprograms

To monitor code execution, gnatcov inserts calls to “witness” subprograms before statements / decisions / conditions. Such calls can now be inlined when using optimization switches.

Improved test harness execution time

Verbose output from the generated test harness binary executable gnatfuzz-test_harness.afl_fuzz used during the fuzzing campaign has been moved to a separate executable gnatfuzz-test_harness.verbose resulting in an improved test harness execution time and an increase in the average test case executions per second. More executions per second equates to fuzzing campaigns satisfying their stopping criteria quicker.

New test harness build strategy

Compilation time of fuzzing campaigns has been significantly improved by only building the units within the closure of the subprogram under test, rather than the entire user project.

Improved gnatfuzz analyze logs

The gnatfuzz analyze command now logs all Libadalang diagnostics for the analyzed sources. Moreover, rather than terminating, it continues with the analysis using only the units that do not exhibit diagnostics.

Avoid secondary stack usage in instrumented code

The instrumentation process of gnatcov no longer introduces uses of the secondary stack for Ada source code. This means that a codebase that successfully compiles under the No_Secondary_Stack restriction will successfully compile after instrumentation for coverage under the same restriction.