GNATDAS Manuals [25.1 (20250109)]

• 1. GNATcoverage User’s Guide
  • 1.1. Getting Started
    • 1.1.1. General notions
    • 1.1.2. Workflow overview
    • 1.1.3. A simple example
      • 1.1.3.1. Sample project
      • 1.1.3.2. Setup, Instrument, Build, Execute, Analyze
    • 1.1.4. Going Further
    • 1.1.5. Conventions used in the rest of this manual
  • 1.2. Specifying Units Of Interest
    • 1.2.1. Using project files (-P, --projects, --units)
      • 1.2.1.1. Conveying projects of interest
      • 1.2.1.2. Conveying units of interest within projects
      • 1.2.1.3. Conveying subprograms of interest (experimental)
      • 1.2.1.4. Other switches or attributes of importance
    • 1.2.2. Conveying source files to ignore / handling Ada subunits
    • 1.2.3. Compilation unit vs source file names
    • 1.2.4. Providing coverage obligation files (--sid)
  • 1.3. Producing source traces with gnatcov instrument
    • 1.3.1. Setting up the coverage runtime library
      • 1.3.1.1. Multiple runtimes in the same prefix
      • 1.3.1.2. Language restrictions
      • 1.3.1.3. Default source trace dump options
    • 1.3.2. Instrumenting programs
      • 1.3.2.1. gnatcov instrument command line
      • 1.3.2.2. Output strategies for main units
      • 1.3.2.3. Resetting coverage information during the execution
      • 1.3.2.4. Controlling trace file names
      • 1.3.2.5. Support for preprocessing
      • 1.3.2.6. gnatcov instrument limitations
    • 1.3.3. Building instrumented components
    • 1.3.4. Extracting a trace from standard output
    • 1.3.5. Composed instrumentation
    • 1.3.6. Instrumentation of a multi-languages project
    • 1.3.7. Instrumentation and coverage of SPARK code
      • 1.3.7.1. Inhibiting SPARK related pragmas
      • 1.3.7.2. Coverage obligations for SPARK code
    • 1.3.8. Example use cases
      • 1.3.8.1. Whole program instrumented at once, cross configuration, base64 output
      • 1.3.8.2. Library instrumented separately, native configuration, trace output
    • 1.3.9. Coverage runtime customization
      • 1.3.9.1. Basics
      • 1.3.9.2. Customize the base64-stdout dump channel
    • 1.3.10. Building instrumented programs with CCG
      • 1.3.10.1. Customizing the runtime
      • 1.3.10.2. Building an instrumented program with CCG
  • 1.4. Producing source traces with integrated instrumentation (experimental)
    • 1.4.1. Specifying instrumentation switches
    • 1.4.2. Building an instrumented executable
    • 1.4.3. A simple Makefile example
    • 1.4.4. A simple CMake example
  • 1.5. Source coverage analysis with gnatcov coverage
    • 1.5.1. gnatcov coverage command line
    • 1.5.2. Output report formats (--annotate)
      • 1.5.2.1. Cobertura report (=cobertura)
      • 1.5.2.2. Annotated sources, html (=html)
      • 1.5.2.3. SARIF report (=sarif)
      • 1.5.2.4. Violations summary, text (=report)
      • 1.5.2.5. Annotated sources, text (=xcov[+])
      • 1.5.2.6. XML report, xml (=xml)
    • 1.5.3. Statement Coverage analysis
      • 1.5.3.1. Core notions and Reporting (--level=stmt)
      • 1.5.3.2. Example program and assessments
    • 1.5.4. Decision Coverage analysis
      • 1.5.4.1. Core notions and Reporting (--level=stmt+decision)
      • 1.5.4.2. Example program and assessments
    • 1.5.5. Modified Condition/Decision Coverage analysis
      • 1.5.5.1. Core notions and Reporting (--level=stmt+mcdc)
      • 1.5.5.2. Example decisions and conditions
      • 1.5.5.3. Handling non short-circuit operators
      • 1.5.5.4. MCDC variants
      • 1.5.5.5. Example program and assessments
    • 1.5.6. Assertion True Coverage (ATC) analysis (experimental)
      • 1.5.6.1. Core notions and Reporting (--level=...+atc)
    • 1.5.7. Assertion True Condition Coverage (ATCC) analysis (experimental)
      • 1.5.7.1. Core notions and Reporting (--level=...+atcc)
    • 1.5.8. Function and Call Coverage (FUN_CALL) analysis (experimental)
      • 1.5.8.1. Core notions and Reporting (--level=...+fun_call)
    • 1.5.9. Synthetic metrics
    • 1.5.10. Handling source relocation for annotated sources output formats
    • 1.5.11. Inlining & Ada generic units
      • 1.5.11.1. Combined coverage on generics (default behavior)
      • 1.5.11.2. Separated coverage on generics
    • 1.5.12. Handling Ada assertions and contracts
    • 1.5.13. Processing of C macros
    • 1.5.14. Optimization and non-coverable items
  • 1.6. Coverage Consolidation
    • 1.6.1. Consolidation from trace files
      • 1.6.1.1. Single unit tested by different programs
      • 1.6.1.2. Disjoint units tested by different programs
      • 1.6.1.3. Multiple executions of a single program
    • 1.6.2. Consolidation from coverage checkpoints
      • 1.6.2.1. Efficient storage of test results
      • 1.6.2.2. Incremental coverage analysis
      • 1.6.2.3. Handle incidental coverage effects
      • 1.6.2.4. Compatibility considerations
  • 1.7. Coverage Exemptions
    • 1.7.1. Defining Exemption Regions
    • 1.7.2. Reporting about coverage exemptions
      • 1.7.2.1. Undetermined Coverage state and Exemptions
    • 1.7.3. Object coverage exemptions
  • 1.8. Disable coverage analysis
    • 1.8.1. Defining Disabled Coverage Regions
    • 1.8.2. Consolidating traces with varying disabled coverage regions
    • 1.8.3. Reporting about disabled coverage regions
  • 1.9. External source annotations
    • 1.9.1. Generating external annotations
      • 1.9.1.1. Semantics of buffer manipulation annotations
      • 1.9.1.2. File relocation considerations
    • 1.9.2. Deleting a pre-existing annotation
    • 1.9.3. Displaying the annotations contained in annotation files
    • 1.9.4. Annotation stability through file modifications
  • 1.10. Using project files
    • 1.10.1. General considerations
    • 1.10.2. Specifying gnatcov command Switches
    • 1.10.3. Specifying the Target and language Runtime
  • 1.11. Using GNATcoverage from GNAT Studio
    • 1.11.1. Basic scenario
    • 1.11.2. Viewing a coverage report produced outside of GNAT Studio
    • 1.11.3. GNATtest scenario
  • 1.12. Glossary of terms & concepts
  • 1.13. Appendices
    • 1.13.1. Sample html index
    • 1.13.2. Sample html annotated source
• 2. GNATtest User’s Guide
  • 2.1. Running gnattest
    • 2.1.1. Framework Generation Mode
    • 2.1.2. Test Execution Mode
  • 2.2. Switches for gnattest in framework generation mode
  • 2.3. Switches for gnattest in test execution mode
  • 2.4. Project Attributes for gnattest
  • 2.5. Simple Example
  • 2.6. Setting Up and Tearing Down the Testing Environment
  • 2.7. Regenerating Tests
  • 2.8. Default Test Behavior
  • 2.9. Testing Primitive Operations of Tagged Types
  • 2.10. Testing Inheritance
  • 2.11. Tagged Type Substitutability Testing
  • 2.12. Testing with Contracts
  • 2.13. Additional Tests
  • 2.14. Individual Test Drivers
  • 2.15. Stubbing
  • 2.16. Integration with GNATcoverage
  • 2.17. Putting Tests under Version Control
  • 2.18. Aggregate project handling
    • 2.18.1. Artifact directories and aggregate projects
  • 2.19. Current Limitations
  • 2.20. Automatically generating test cases (experimental)
    • 2.20.1. Setting up the test generation runtime
    • 2.20.2. Generating test inputs
• 3. GNATfuzz User’s Guide
  • 3.1. Introduction
    • 3.1.1. Fuzz-testing in a nutshell
    • 3.1.2. AFL++ basics
    • 3.1.3. GNATfuzz overview
  • 3.2. GNATfuzz command line interface
    • 3.2.1. GNATfuzz “analyze” mode command line interface
    • 3.2.2. GNATfuzz “generate” mode command line interface
    • 3.2.3. GNATfuzz “corpus-gen” mode command line interface
    • 3.2.4. GNATfuzz “fuzz” mode command line interface
  • 3.3. GNATfuzz by example
    • 3.3.1. Prerequisites and possible configurations
      • 3.3.1.1. AFL++ requirements
      • 3.3.1.2. GNATfuzz requirements
      • 3.3.1.3. GNATfuzz configurations
      • 3.3.1.4. Accommodating linker flags required by the user project
      • 3.3.1.5. GNATfuzz and the AFL++ execution modes
    • 3.3.2. GNATfuzz automation capabilities and limitations
      • 3.3.2.1. Fuzz-testing when corpus auto-generation is unsupported
    • 3.3.3. Fuzzing a simple Ada subprogram
      • 3.3.3.1. Using analyze mode
      • 3.3.3.2. Using generate mode
      • 3.3.3.3. Using corpus-gen mode
      • 3.3.3.4. Decoding an auto-generated test case
      • 3.3.3.5. Using fuzz mode
    • 3.3.4. Fuzzing an autogenerated test-harness with user-provided seeds
    • 3.3.5. Fuzzing instantiations of generic subprograms
    • 3.3.6. Fuzzing global and private state
    • 3.3.7. Fuzzing Access Types
    • 3.3.8. Filtering exceptions
    • 3.3.9. Fuzzing C functions through Ada bindings
    • 3.3.10. Resetting dynamically allocated memory when fuzz-testing with the AFL++ persistent mode
    • 3.3.11. CMPLOG (aka RedQueen) support
  • 3.4. The “User_Configuration” package
  • 3.5. GNATfuzz stopping criteria
  • 3.6. GNATfuzz integration in GNAT Studio
    • 3.6.1. The GNATfuzz menu
    • 3.6.2. Viewing analysis results and generating a fuzz-testing harness
    • 3.6.3. Running a fuzz session
    • 3.6.4. Viewing and debugging fuzz crashes
  • 3.7. FAQ for GNATfuzz
  • 3.8. GNATfuzz diagnostics and issue reporting
    • 3.8.1. GNATfuzz Error Codes and Exit Statuses
      • 3.8.1.1. Error_Unknown
      • 3.8.1.2. Invalid_Command_Line_Options
      • 3.8.1.3. Invalid_GNATfuzz_Configuration_Options
      • 3.8.1.4. Invalid_Fuzzable_Subprogram
      • 3.8.1.5. Error_Initializing_Fuzzing_Campaigns
      • 3.8.1.6. Error_Launching_Fuzzing_Campaigns
      • 3.8.1.7. Error_During_Fuzzing_Campaigns
      • 3.8.1.8. Error_Terminating_Campaigns
      • 3.8.1.9. Error_Initializing_Supporting_Tool
      • 3.8.1.10. Error_Executing_Supporting_Tool
      • 3.8.1.11. Error_Generating_Starting_Corpus
  • 3.9. GNATfuzz Beta feature
    • 3.9.1. Fuzzing with an arbitrary starting corpus
    • 3.9.2. GNATfuzz and Symbolic Execution
      • 3.9.2.1. Enabling SymCC
      • 3.9.2.2. Current Limitations
• 4. Using GNATtest with GNATcoverage
  • 4.1. Using the Makefile generated by GNATtest
    • 4.1.1. Special considerations for cross environment targets
    • 4.1.2. Usage example
    • 4.1.3. Instrumenting test harnesses for a SPARK project
  • 4.2. Developing a custom solution
    • 4.2.1. Single test driver
    • 4.2.2. Separate test drivers
• 5. Using GNATtest with GNATfuzz (experimental)
  • 5.1. Setting up the environment
  • 5.2. Using GNATStudio to perform the integration

• Appendix A. Using GNATcoverage Binary Traces
  • Introduction
    • Definition and main characteristics
    • Workflow overview
    • A simple example
    • Going Further
  • Producing binary traces with gnatcov run
    • Compilation prerequisites
      • General rules
      • Consolidation related rules
    • gnatcov run command line
    • Execution environment
    • Program selection and Arguments passing
    • Trace file contents
  • Object coverage analysis with gnatcov coverage
    • gnatcov coverage command line
    • Output report formats (--annotate)
      • Machine level reports (=asm)
      • Annotated sources, text (=xcov[+])
      • Annotated sources, html (=html)
    • Object Instruction Coverage analysis (--level=insn)
    • Object Branch Coverage analysis (--level=branch)
    • Focusing on subprograms of interest (--routines)
    • Inlining & Ada Generic units
    • Full object coverage considerations
  • Object/Source level metrics considerations
    • Main differences examplified
    • Full branch coverage vs MCDC
  • Using GNATcoverage from GNAT Studio
  • Importing binary traces with gnatcov convert
    • gnatcov convert command line
    • Generating Coverage Information from Nexus Traces on MPC5634M
      • Nexus Program Trace Data: the Hardware Perspective
      • Configuring the winIDEA Analyzer
      • Exporting the Trace Data
    • Generating Coverage Information from Lauterbach Trace32
      • Enabling Trace Data
      • Running the executable
      • Exporting the Trace Data
      • Automation
  • Target specific points of note with Binary traces
  • Known Limitations with Binary traces
    • Incomplete statement coverage on lines with multiple statements
    • MCDC inaccuracies with interrupts and multi-threaded applications