GNAT DAS Manuals [28.0w (20260930)]

• 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.1.4. Coverage runtime setup for configurations with no Ada runtime
    • 1.3.2. Instrumenting programs
      • 1.3.2.1. gnatcov instrument command line
      • 1.3.2.2. Output strategies for coverage information
      • 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. Optimizing the execution of instrumented programs
    • 1.3.4. Building instrumented components
    • 1.3.5. Extracting a trace from standard output
    • 1.3.6. Composed instrumentation
    • 1.3.7. Instrumentation of a multi-languages project
    • 1.3.8. Instrumentation and coverage of SPARK code
      • 1.3.8.1. Inhibiting SPARK related pragmas
      • 1.3.8.2. Coverage obligations for SPARK code
    • 1.3.9. Example use cases
      • 1.3.9.1. Whole program instrumented at once, cross configuration, base64 output
      • 1.3.9.2. Library instrumented separately, native configuration, trace output
    • 1.3.10. Coverage runtime customization
      • 1.3.10.1. Basics
      • 1.3.10.2. Customize the base64-stdout dump channel
      • 1.3.10.3. When the customized runtime needs elaboration
    • 1.3.11. Building instrumented programs with CCG
      • 1.3.11.1. Customizing the runtime
      • 1.3.11.2. Building an instrumented program with CCG
    • 1.3.12. Common instrumentation errors
      • 1.3.12.1. Linker error when building instrumented application
  • 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. Generating a coverage report
    • 1.4.4. A simple Makefile example
    • 1.4.5. 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. Guarded Expression Coverage (GEXPR) analysis (experimental)
      • 1.5.9.1. Core notions and Reporting (--level=...+gexpr)
    • 1.5.10. Synthetic metrics
    • 1.5.11. Handling source relocation for annotated sources output formats
    • 1.5.12. Inlining & Ada generic units
      • 1.5.12.1. Combined coverage on generics
    • 1.5.13. Handling Ada assertions and contracts
    • 1.5.14. Processing of C macros
    • 1.5.15. Optimization and non-coverable items
  • 1.6. Rust coverage analysis with gnatcov coverage
    • 1.6.1. Rust coverage workflow
      • 1.6.1.1. Instrument and build the project
      • 1.6.1.2. Run the executed binary
      • 1.6.1.3. Produce a coverage report
    • 1.6.2. Rust coverage limitations
      • 1.6.2.1. MC/DC false-negatives related to instrumentation level
      • 1.6.2.2. Approximative source location ranges
      • 1.6.2.3. Unsupported constructs
  • 1.7. Coverage Consolidation
    • 1.7.1. Consolidation from trace files
      • 1.7.1.1. Single unit tested by different programs
      • 1.7.1.2. Disjoint units tested by different programs
      • 1.7.1.3. Multiple executions of a single program
    • 1.7.2. Consolidation from coverage checkpoints
      • 1.7.2.1. Efficient storage of test results
      • 1.7.2.2. Incremental coverage analysis
      • 1.7.2.3. Handle incidental coverage effects
      • 1.7.2.4. Compatibility considerations
    • 1.7.3. Consolidating Coverage for Different Project Build Configurations
      • 1.7.3.1. Use SID files to use all source traces at once
      • 1.7.3.2. Use project loading options to load source traces separately
  • 1.8. Coverage Exemptions
    • 1.8.1. Defining Exemption Regions
    • 1.8.2. Defining Fine Grained Exemptions
      • 1.8.2.1. Decision Outcome Exemptions
      • 1.8.2.2. Decision Condition Exemptions
      • 1.8.2.3. Full Decision Exemptions
      • 1.8.2.4. Branch Exemptions
      • 1.8.2.5. Manual Decision Evaluations
    • 1.8.3. Reporting about coverage exemptions
      • 1.8.3.1. Exemption regions
      • 1.8.3.2. Fine grained exemptions
      • 1.8.3.3. Undetermined Coverage state and Exemptions
    • 1.8.4. Object coverage exemptions
  • 1.9. Disable coverage analysis
    • 1.9.1. Defining Disabled Coverage Regions
    • 1.9.2. Consolidating traces with varying disabled coverage regions
    • 1.9.3. Reporting about disabled coverage regions
  • 1.10. External source annotations
    • 1.10.1. Designating the annotation file from the project
    • 1.10.2. Generating external annotations
      • 1.10.2.1. Semantics of buffer manipulation annotations
      • 1.10.2.2. File relocation considerations
    • 1.10.3. Migrating in-source annotations to external annotations
      • 1.10.3.1. Removing the in-source annotations
    • 1.10.4. Deleting a pre-existing annotation
    • 1.10.5. Displaying the annotations contained in annotation files
    • 1.10.6. Annotation stability through file modifications
    • 1.10.7. Using external annotations from VS Code
      • 1.10.7.1. Displaying annotations
      • 1.10.7.2. Browsing and deleting annotations
      • 1.10.7.3. Creating annotations
  • 1.11. Using project files
    • 1.11.1. General considerations
    • 1.11.2. Specifying gnatcov command Switches
    • 1.11.3. Specifying the Target and language Runtime
  • 1.12. Using GNATcoverage from GNAT Studio
    • 1.12.1. Basic scenario
    • 1.12.2. Viewing a coverage report produced outside of GNAT Studio
    • 1.12.3. Using GNATtest’s coverage integration makefile
    • 1.12.4. GNATtest scenario
  • 1.13. Glossary of terms & concepts
  • 1.14. Appendices
    • 1.14.1. Sample html index
    • 1.14.2. Sample html annotated source
• 2. GNATtest User’s Guide
  • 2.1. Setting up the runtimes required by gnattest
  • 2.2. Running gnattest
    • 2.2.1. Framework Generation Mode
    • 2.2.2. Test Execution Mode
  • 2.3. Switches for gnattest in framework generation mode
  • 2.4. Selecting the sources to process
  • 2.5. Switches for gnattest in test execution mode
  • 2.6. Project Attributes for gnattest
  • 2.7. Simple Example
  • 2.8. Setting Up and Tearing Down the Testing Environment
  • 2.9. Regenerating Tests
  • 2.10. Default Test Behavior
  • 2.11. Selecting Tests to Run
  • 2.12. Testing Primitive Operations of Tagged Types
  • 2.13. Testing Inheritance
  • 2.14. Tagged Type Substitutability Testing
  • 2.15. Testing with Contracts
  • 2.16. Additional Tests
  • 2.17. Individual Test Drivers
  • 2.18. Stubbing
  • 2.19. Integration with GNATcoverage
  • 2.20. Structure of the Generated Harness
    • 2.20.1. Responsibilities of the harness components
    • 2.20.2. Files the user is expected to modify
  • 2.21. Putting Tests under Version Control
  • 2.22. Aggregate project handling
    • 2.22.1. Artifact directories and aggregate projects
  • 2.23. Current Limitations
  • 2.24. Automatically generating test cases (experimental)
    • 2.24.1. Setting up the test generation runtime
    • 2.24.2. Generating test inputs
      • 2.24.2.1. Supported types
      • 2.24.2.2. Test input generation strategies
    • 2.24.3. Test input generation through a proxy subprogram
• 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 “build” mode command line interface
    • 3.2.4. GNATfuzz “generate-corpus” mode command line interface
    • 3.2.5. GNATfuzz “minimize-corpus” mode command line interface
    • 3.2.6. 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.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 build mode
      • 3.3.3.4. Using generate-corpus mode
      • 3.3.3.5. Using minimize-corpus mode
      • 3.3.3.6. Decoding an auto-generated test case
      • 3.3.3.7. Using fuzz mode
    • 3.3.4. Fuzzing with non-automatically generated starting corpus
      • 3.3.4.1. Fuzzing with user-provided seeds
      • 3.3.4.2. Fuzzing with a dummy starting corpus
    • 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.8.1.12. Invalid_Stop_Criteria_Rules
  • 3.9. GNATfuzz Beta feature
    • 3.9.1. Incremental fuzzing with TGen test vectors
      • 3.9.1.1. GNATfuzz “import-tgen-vectors” mode command line interface
      • 3.9.1.2. Incremental fuzzing workflow
      • 3.9.1.3. Beta experimental TGen flags for “fuzz” mode
    • 3.9.2. GNATfuzz and Symbolic Execution
      • 3.9.2.1. Enabling SymCC
      • 3.9.2.2. Current Limitations
    • 3.9.3. GNATfuzz Adaptive - “On-target” fuzzing (experimental)
      • 3.9.3.1. What is it?
      • 3.9.3.2. How to use?
      • 3.9.3.3. Setup the development environment
      • 3.9.3.4. Configure the fuzzer
      • 3.9.3.5. Understanding the results
      • 3.9.3.6. Example usage
      • 3.9.3.7. Known limitations
    • 3.9.4. Introducing the hot-spot workflow
      • 3.9.4.1. When to use the hot-spot workflow
      • 3.9.4.2. Prerequisites
      • 3.9.4.3. Hot-spot command line interface
      • 3.9.4.4. End-to-end example
      • 3.9.4.5. Workflow steps
      • 3.9.4.6. Terminal output
      • 3.9.4.7. Crash correlation and confidence scoring
      • 3.9.4.8. Augmented SARIF output
      • 3.9.4.9. Machine-readable summary report
      • 3.9.4.10. Coverage reports
      • 3.9.4.11. TGen test vector integration
      • 3.9.4.12. Output directory layout
    • 3.9.5. Introducing the fuzz-everything workflow
      • 3.9.5.1. Accessing the fuzz-everything workflow
      • 3.9.5.2. Fuzz-everything “inspect” mode command line interface
      • 3.9.5.3. Fuzz-everything “test” mode command line interface
      • 3.9.5.4. Fuzz-everything “inspect” mode usage example
      • 3.9.5.5. Fuzz-everything “test” mode usage example
      • 3.9.5.6. Utilizing fuzz-everything-generated test cases with GNATtest
      • 3.9.5.7. Utilizing test cases generated from previous sessions
    • 3.9.6. Libfuzzer
      • 3.9.6.1. Libfuzzer basics
      • 3.9.6.2. Libfuzzer requirements
      • 3.9.6.3. GNATfuzz and the libfuzzer execution configuration
• 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 exemplified
    • 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