diff --git a/.gitreview b/.gitreview
index a5d94509a..f96d59fbc 100644
--- a/.gitreview
+++ b/.gitreview
@@ -2,5 +2,5 @@
 host = git.adacore.com
 port = 29418
 project = gnatcoverage
-defaultbranch = master
+defaultbranch = 21-sustained
 defaultremote = origin
diff --git a/doc/gnatcov/target_switch_common_text.rst b/doc/gnatcov/target_switch_common_text.rst
new file mode 100644
index 000000000..607d8d5f6
--- /dev/null
+++ b/doc/gnatcov/target_switch_common_text.rst
@@ -0,0 +1,8 @@
+.. Text to be included first in all the descriptions of --target
+
+State the target toolchain configuration used to build the analyzed
+programs, as provided to ``gprbuild``. For cross or 32bit native
+configurations, this switch together with its possible ``--RTS`` companion
+is required for all commands using project files unless the root
+project provides the information with ``Target``/``Runtime``
+attributes.
diff --git a/testsuite/Qualif/Common/GprFacilities/GnatcovSwitches/CmdLinePrevails/test.py b/testsuite/Qualif/Common/GprFacilities/GnatcovSwitches/CmdLinePrevails/test.py
index 71f438b31..cf59bede7 100644
--- a/testsuite/Qualif/Common/GprFacilities/GnatcovSwitches/CmdLinePrevails/test.py
+++ b/testsuite/Qualif/Common/GprFacilities/GnatcovSwitches/CmdLinePrevails/test.py
@@ -1,7 +1,6 @@
+import os.path
 import re
 
-from e3.fs import mkdir
-
 from SCOV.minicheck import build_and_run
 from SUITE.context import thistest
 from SUITE.cutils import Wdir, contents_of
@@ -10,26 +9,32 @@
 
 
 pgm = 'test_lt0'
-wd = Wdir('wd_', clean=True)
-
-gpr = gprfor(mains=[pgm + '.adb'],
-             srcdirs=['../src'],
-             extra=gprcov_for(switches=[
-                Csw('*', ['--level=stmt']),
-                Csw('coverage', ['--annotate=report'])]))
 
 
-def run(extra_args, covlevel=None):
+def run(subdir, extra_args, covlevel=None):
     """
     Build and run the single test program, which volontarily performs stmt and
     decision coverage violations.
     """
+    dirname = f"tmp_{subdir}"
+    wd = Wdir(dirname)
+
+    gpr = gprfor(mains=[pgm + '.adb'],
+                 srcdirs=['../src'],
+                 extra=gprcov_for(switches=[
+                    Csw('*', ['--level=stmt']),
+                    Csw('coverage', ['--annotate=report'])]))
+
     xcov_args = build_and_run(
         gprsw=GPRswitches(root_project=gpr),
-        covlevel=covlevel, mains=[pgm],
-        extra_coverage_args=[])
+        covlevel=covlevel,
+        mains=[pgm],
+        extra_coverage_args=[] if covlevel is None else ['--level', covlevel])
     xcov(xcov_args + extra_args)
 
+    wd.to_homedir()
+    return dirname
+
 
 def check_report(label, filename, pattern, check_present=True):
     report = contents_of(filename)
@@ -41,37 +46,37 @@ def check_report(label, filename, pattern, check_present=True):
 # Check that we get results corresponding to the project file
 # defaults if we don't tell anything otherwise.
 
-run(['-o', 'def.rep'])
+subdir = run("default", ['-o', 'def.rep'])
+def_rep = os.path.join(subdir, "def.rep")
 
 # Check that we have the output report, that it does contain at least a stmt
 # coverage violation note, and that it doesn't contain any DC related note.
 check_report('missing expected stmt coverage failure indication',
-             'def.rep', 'statement not executed')
+             def_rep, 'statement not executed')
 check_report('unexpected decision coverage failure indication',
-             'def.rep', 'decision outcome .* never exercised',
+             def_rep, 'decision outcome .* never exercised',
              check_present=False)
 
 # Override --level up to DC. Check that we now find the DC violations we
 # expect.
 
-run(['-o', 'lev.rep'], covlevel='stmt+decision')
+subdir = run("lev", ['-o', 'lev.rep'], covlevel='stmt+decision')
+lev_rep = os.path.join(subdir, "lev.rep")
 check_report('missing expected decision coverage failure indication',
-             'lev.rep', 'decision outcome .* never exercised')
+             lev_rep, 'decision outcome .* never exercised')
 
 # Override --annotate only. Expect full coverage on the "if"
 # statement.
 
-mkdir('sc')
-run(['--annotate=xcov', '--output-dir=sc'])
+subdir = run("ann", ['--annotate=xcov'])
 check_report('missing expected full coverage indication',
-             'sc/values.adb.xcov', r'\+:.*if')
+             os.path.join(subdir, "obj", "values.adb.xcov"), r'\+:.*if')
 
 # Override --annotate and --level. Expect partial coverage on the "if"
 # statement.
 
-mkdir('dc')
-run(['--annotate=xcov', '--output-dir=dc'], covlevel='stmt+decision')
+subdir = run("lev-ann", ['--annotate=xcov'], covlevel='stmt+decision')
 check_report('missing expected partial decision coverage indication',
-             'dc/values.adb.xcov', '!:.*if')
+             os.path.join(subdir, "obj", "values.adb.xcov"), '!:.*if')
 
 thistest.result()
diff --git a/testsuite/Qualif/Common/GprFacilities/GnatcovSwitches/InSubproject/test.py b/testsuite/Qualif/Common/GprFacilities/GnatcovSwitches/InSubproject/test.py
index df9b22763..0ea9858a0 100644
--- a/testsuite/Qualif/Common/GprFacilities/GnatcovSwitches/InSubproject/test.py
+++ b/testsuite/Qualif/Common/GprFacilities/GnatcovSwitches/InSubproject/test.py
@@ -9,7 +9,7 @@
 
 
 pgm = 'test_lt0'
-wd = Wdir('wd_', clean=True)
+wd = Wdir('wd_')
 
 # Build and run the single test program, which volontarily performs stmt and
 # decision coverage violations.
diff --git a/testsuite/Qualif/Common/GprFacilities/Subdirs/BuildRunAnalyze/test.py b/testsuite/Qualif/Common/GprFacilities/Subdirs/BuildRunAnalyze/test.py
index 5190770d7..a26aaad47 100644
--- a/testsuite/Qualif/Common/GprFacilities/Subdirs/BuildRunAnalyze/test.py
+++ b/testsuite/Qualif/Common/GprFacilities/Subdirs/BuildRunAnalyze/test.py
@@ -9,7 +9,7 @@
 from SUITE.tutils import gprfor
 
 
-wd = Wdir('wd_', clean=True)
+wd = Wdir('wd_')
 
 
 gprname = 'p'
diff --git a/testsuite/Qualif/Common/UnitsOfInterest/GPR/ControlByCmdLine/ProjectsAndUnits/test.py b/testsuite/Qualif/Common/UnitsOfInterest/GPR/ControlByCmdLine/ProjectsAndUnits/test.py
index 3f8d9f3c4..4bcba93ee 100644
--- a/testsuite/Qualif/Common/UnitsOfInterest/GPR/ControlByCmdLine/ProjectsAndUnits/test.py
+++ b/testsuite/Qualif/Common/UnitsOfInterest/GPR/ControlByCmdLine/ProjectsAndUnits/test.py
@@ -9,7 +9,7 @@
 
 # Create a directory to hold temporary files, so that we do not accumulate
 # uncleaned temporary files across testsuite runs.
-temp_file_dir = Wdir('tmp_files', clean=True)
+temp_file_dir = Wdir('tmp_files')
 temp_file_dir.to_homedir()
 
 # Note that intops involves sub-units while boolops involves child-units,
diff --git a/testsuite/Qualif/Common/UnitsOfInterest/GPR/ControlByCmdLine/test_support.py b/testsuite/Qualif/Common/UnitsOfInterest/GPR/ControlByCmdLine/test_support.py
index 8527fee91..2391fd839 100644
--- a/testsuite/Qualif/Common/UnitsOfInterest/GPR/ControlByCmdLine/test_support.py
+++ b/testsuite/Qualif/Common/UnitsOfInterest/GPR/ControlByCmdLine/test_support.py
@@ -118,7 +118,7 @@ def check(root_project, recurse,
     # in requesting not to pass --no-subprojects.
     gprsw_no_subprojects = False if recurse is None else not recurse
 
-    wd = Wdir(clean=True)
+    wd = Wdir()
     wd.to_subdir(tmpdir)
 
     TestCase(category=None).run(
diff --git a/testsuite/Qualif/Common/UnitsOfInterest/GPR/ExtProjects/AttrOverride/test.py b/testsuite/Qualif/Common/UnitsOfInterest/GPR/ExtProjects/AttrOverride/test.py
index 9785be216..675277b1d 100644
--- a/testsuite/Qualif/Common/UnitsOfInterest/GPR/ExtProjects/AttrOverride/test.py
+++ b/testsuite/Qualif/Common/UnitsOfInterest/GPR/ExtProjects/AttrOverride/test.py
@@ -6,7 +6,7 @@
 from SUITE.tutils import gprfor
 
 
-wd = Wdir('wd_', clean=True)
+wd = Wdir('wd_')
 
 build_run_and_coverage(
     gprsw=GPRswitches(root_project=gprfor(mains=['test_lt0.adb'],
diff --git a/testsuite/Qualif/Common/UnitsOfInterest/GPR/ExtProjects/ExtendedHasMain/test.py b/testsuite/Qualif/Common/UnitsOfInterest/GPR/ExtProjects/ExtendedHasMain/test.py
index c8be6578e..7cfaae5d9 100644
--- a/testsuite/Qualif/Common/UnitsOfInterest/GPR/ExtProjects/ExtendedHasMain/test.py
+++ b/testsuite/Qualif/Common/UnitsOfInterest/GPR/ExtProjects/ExtendedHasMain/test.py
@@ -10,7 +10,7 @@
 from SUITE.tutils import gprfor
 
 
-wd = Wdir('wd_', clean=True)
+wd = Wdir('wd_')
 
 # Prepare the two project files
 p = gprfor(prjid='p', mains=['main1.adb'], srcdirs=['../src'],
diff --git a/testsuite/Qualif/Common/UnitsOfInterest/GPR/ExtProjects/PartialUnitOverride/test.py b/testsuite/Qualif/Common/UnitsOfInterest/GPR/ExtProjects/PartialUnitOverride/test.py
index fc8a1287e..036438b90 100644
--- a/testsuite/Qualif/Common/UnitsOfInterest/GPR/ExtProjects/PartialUnitOverride/test.py
+++ b/testsuite/Qualif/Common/UnitsOfInterest/GPR/ExtProjects/PartialUnitOverride/test.py
@@ -12,7 +12,7 @@
 from SUITE.tutils import gprfor
 
 
-tmp = Wdir('wd_', clean=True)
+tmp = Wdir('wd_')
 
 # The "orig" project contains two units: "main" and "helper". The "ext" project
 # extends "orig" and overrides only the "helper" unit.
diff --git a/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/BadUnitInAttr/test.py b/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/BadUnitInAttr/test.py
index 086aa501d..1ecc98509 100644
--- a/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/BadUnitInAttr/test.py
+++ b/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/BadUnitInAttr/test.py
@@ -9,7 +9,7 @@
 from SUITE.tutils import gprfor
 
 
-tmp = Wdir('wd_', clean=True)
+tmp = Wdir('wd_')
 
 build_run_and_coverage(
     gprsw=GPRswitches(root_project=gprfor(
diff --git a/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/BadUnitInSwitch/test.py b/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/BadUnitInSwitch/test.py
index fd908e044..c4f1eecc6 100644
--- a/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/BadUnitInSwitch/test.py
+++ b/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/BadUnitInSwitch/test.py
@@ -9,7 +9,7 @@
 from SUITE.tutils import gprfor
 
 
-tmp = Wdir('wd_', clean=True)
+tmp = Wdir('wd_')
 
 build_run_and_coverage(
     gprsw=GPRswitches(root_project=gprfor('main.adb', srcdirs='..'),
diff --git a/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/MissingLI/test.py b/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/MissingLI/test.py
index 9a38206ae..e24935c2b 100644
--- a/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/MissingLI/test.py
+++ b/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/MissingLI/test.py
@@ -22,7 +22,7 @@
 from SUITE.tutils import gprfor, xcov
 
 
-tmp = Wdir('wd_', clean=True)
+tmp = Wdir('wd_')
 
 xcov_args = build_and_run(
     gprsw=GPRswitches(root_project=gprfor('main.adb', srcdirs='..')),
diff --git a/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/NoContribPrj/test.py b/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/NoContribPrj/test.py
index 832695fec..aaf424ca8 100644
--- a/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/NoContribPrj/test.py
+++ b/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/NoContribPrj/test.py
@@ -12,7 +12,7 @@
 from SUITE.tutils import gprfor
 
 
-tmp = Wdir('wd_', clean=True)
+tmp = Wdir('wd_')
 
 
 class ProjectConfig(object):
diff --git a/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/UnitNotInProjects/test.py b/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/UnitNotInProjects/test.py
index 7d1a9bd1c..30e41e757 100644
--- a/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/UnitNotInProjects/test.py
+++ b/testsuite/Qualif/Common/UnitsOfInterest/GPR/Robustness/UnitNotInProjects/test.py
@@ -13,7 +13,7 @@
 from SUITE.tutils import gprfor
 
 
-tmp = Wdir('wd_', clean=True)
+tmp = Wdir('wd_')
 mkdir('obj-helper')
 mkdir('obj-main')
 
diff --git a/testsuite/Qualif/Common/UnitsOfInterest/SCOS/test_support.py b/testsuite/Qualif/Common/UnitsOfInterest/SCOS/test_support.py
index 691b1a58a..c5c85b477 100644
--- a/testsuite/Qualif/Common/UnitsOfInterest/SCOS/test_support.py
+++ b/testsuite/Qualif/Common/UnitsOfInterest/SCOS/test_support.py
@@ -49,7 +49,7 @@ def _tryone(sco_args, odir):
 
     # Create the output dir and execute the commands from there
 
-    wsd = Wdir(subdir=odir, clean=True)
+    wsd = Wdir(subdir=odir)
 
     _run_and_cov(pgm='../test_ab', level='stmt+mcdc', sco_args=sco_args)
 
diff --git a/testsuite/SCOV/internals/driver.py b/testsuite/SCOV/internals/driver.py
index da360acfb..ec92b03fa 100644
--- a/testsuite/SCOV/internals/driver.py
+++ b/testsuite/SCOV/internals/driver.py
@@ -23,7 +23,7 @@
 from collections import defaultdict
 import os
 
-from e3.fs import mkdir, ls
+from e3.fs import mkdir, ls, rm
 from e3.os.fs import cd
 
 from SCOV.tctl import CAT, CovControl
@@ -40,8 +40,8 @@
 from SUITE.tutils import gprbuild, gprfor, xrun, xcov, frame
 from SUITE.tutils import gprbuild_cargs_with
 from SUITE.tutils import exename_for
-from SUITE.tutils import (srctracename_for, tracename_for, ckptname_for,
-                          run_cov_program)
+from SUITE.tutils import (srctrace_pattern_for, srctracename_for,
+                          tracename_for, ckptname_for, run_cov_program)
 
 from .cnotes import r0, r0c, xBlock0, xBlock1, lx0, lx1, lFullCov, lPartCov
 from .cnotes import KnoteDict, elNoteKinds, erNoteKinds, rAntiKinds
@@ -414,6 +414,10 @@ def mode_scofiles_switch(self):
         raise NotImplementedError
 
     def mode_tracename_for(self, pgm):
+        """Name of the trace file for the given program name.
+
+        Due to specificities of the source trace files in native contexts, this
+        method should be called only once the trace file has been created."""
         raise NotImplementedError
 
     def __init__(self, testcase, drivers, xfile, xcovlevel, covctl, wdctl):
@@ -807,7 +811,7 @@ def gen_xcov_reports(self):
 
         inputs = "%s@%s" % (
             input_opt,
-            list_to_file([self.awdir_for(pgm) + input_fn(pgm)
+            list_to_file([input_fn(os.path.join(self.awdir_for(pgm), pgm))
                           for pgm in self.programs()],
                          "inputs.list")
         )
@@ -1041,6 +1045,7 @@ def to_workdir(self, wdir):
         expected to be either absolute or relative from the homedir."""
 
         self.to_homedir()
+        rm(wdir, recursive=True)
         mkdir(wdir)
         cd(wdir)
 
@@ -1325,7 +1330,11 @@ def mode_execute(self, main):
         # If the dump channel just writes text on stdout, extract traces from
         # it.
         if self.dump_channel == 'base64-stdout':
-            xcov_convert_base64(out_file, self.mode_tracename_for(main),
+            # The mode_tracename_for method works only after the trace file has
+            # been created: create a trace file that srctracename_for (called
+            # in mode_tracename_for) will pick up.
+            trace_file = srctrace_pattern_for(main).replace("*", "unique")
+            xcov_convert_base64(out_file, trace_file,
                                 register_failure=register_failure)
 
         return out_file
diff --git a/testsuite/SCOV/minicheck.py b/testsuite/SCOV/minicheck.py
index 7c786243e..2bbfadefd 100644
--- a/testsuite/SCOV/minicheck.py
+++ b/testsuite/SCOV/minicheck.py
@@ -12,12 +12,15 @@
 import os.path
 import re
 
+from e3.fs import rm
+
 from SCOV.instr import (default_dump_channel, xcov_convert_base64,
                         xcov_instrument)
 from SUITE.cutils import contents_of, indent
-from SUITE.tutils import (exepath_to, gprbuild, run_cov_program,
-                          srctracename_for, thistest, tracename_for, xcov,
-                          xrun)
+from SUITE.tutils import (
+    exepath_to, gprbuild, run_cov_program, srctrace_pattern_for,
+    srctracename_for, thistest, tracename_for, xcov, xrun
+)
 
 
 COV_RE = re.compile(r'^ *(\d+) (.):.*$')
@@ -25,12 +28,12 @@
 
 def build_and_run(gprsw, covlevel, mains, extra_coverage_args, scos=None,
                   gpr_obj_dir=None, gpr_exe_dir=None, ignored_source_files=[],
-                  separate_coverage=None, extra_args=[],
+                  separate_coverage=None, extra_args=[], extra_instr_args=None,
                   extra_gprbuild_args=[], extra_gprbuild_cargs=[],
                   absolute_paths=False, dump_trigger=None,
                   dump_channel=None, check_gprbuild_output=False,
                   trace_mode=None, gprsw_for_coverage=None, scos_for_run=True,
-                  register_failure=True):
+                  register_failure=True, program_env=None):
     """
     Prepare a project to run a coverage analysis on it.
 
@@ -66,6 +69,8 @@ def build_and_run(gprsw, covlevel, mains, extra_coverage_args, scos=None,
         to gnatcov using the -S option.
     :param list[str] extra_args: List of arguments to pass to any
         execution of gnatcov (gnatcov run|instrument|coverage).
+    :param list[str] extra_instr_args: List of arguments to pass to all
+        executions of "gnatcov instrument".
     :param list[str] extra_gprbuild_args: List of arguments to pass to
         gprbuild.
     :param list[str] extra_gprbuild_cargs: List of arguments to pass to
@@ -88,6 +93,8 @@ def build_and_run(gprsw, covlevel, mains, extra_coverage_args, scos=None,
         "gnatcov run".
     :param bool register_failure: If true and the execution of one of the mains
         exits with a non-zero status code, stop with a FatalError.
+    :param None|dict[str, str] program_env: If not none, environment variables
+        for the program to run.
 
     :rtype: list[str]
     :return: Incomplete list of arguments to pass to `xcov` in order to run
@@ -159,7 +166,7 @@ def gprbuild_wrapper(root_project, gargs):
         if scos_for_run:
             run_args.extend(scos)
         for m in mains:
-            xrun(run_args + [exepath(m)], out='run.log',
+            xrun(run_args + [exepath(m)], out='run.log', env=program_env,
                  register_failure=register_failure)
         trace_files = [abspath(tracename_for(m)) for m in mains]
 
@@ -169,7 +176,8 @@ def gprbuild_wrapper(root_project, gargs):
         dump_channel = dump_channel or default_dump_channel()
 
         # Instrument the project and build the result
-        xcov_instrument(gprsw, covlevel, extra_args=cov_or_instr_args,
+        extra_instr_args = cov_or_instr_args + list(extra_instr_args or [])
+        xcov_instrument(gprsw, covlevel, extra_args=extra_instr_args,
                         gpr_obj_dir=gpr_obj_dir, dump_trigger=dump_trigger,
                         dump_channel=dump_channel, out='instrument.log',
                         register_failure=register_failure)
@@ -179,23 +187,36 @@ def gprbuild_wrapper(root_project, gargs):
         # Then execute each main and collect trace files
         trace_files = []
         for m in mains:
+            # Remove potential existing source trace files: the name is
+            # non-deterministic by default, so we want to avoid getting
+            # multiple traces in the current directory.
+            rm(srctrace_pattern_for(m))
+
             out_file = '{}_output.txt'.format(m)
-            trace_file = abspath(srctracename_for(m))
-            run_cov_program(exepath(m), out=out_file,
+            run_cov_program(exepath(m), out=out_file, env=program_env,
                             register_failure=register_failure)
-            trace_files.append(trace_file)
 
             # Depending on the dump channel, we also may have to create the
             # trace file.
             if dump_channel == 'bin-file':
-                pass
+                trace_file = srctracename_for(m,
+                                              register_failure=register_failure)
+                if trace_file is None:
+                    continue
+
             elif dump_channel == 'base64-stdout':
+                # Create a trace name that is compatible with srctracename_for
+                trace_file = srctrace_pattern_for(m).replace("*", "unique")
+
                 xcov_convert_base64(out_file, trace_file,
                                     register_failure=register_failure)
+
             else:
                 raise ValueError('Invalid dump channel: {}'
                                  .format(dump_channel))
 
+            trace_files.append(abspath(trace_file))
+
         xcov_args.extend(extra_args)
 
     else:
diff --git a/testsuite/SUITE/context.py b/testsuite/SUITE/context.py
index 2cae2e936..5fe0fc005 100644
--- a/testsuite/SUITE/context.py
+++ b/testsuite/SUITE/context.py
@@ -138,6 +138,9 @@ def __init__(self):
         line options, reset the failures counter and precompute gprbuild
         options we'll have to pass on every call to convey config options.
         """
+        # Shortcut for SUITE.control.env
+        self.env = env
+
         self.start_time = time.time()
 
         # Compute the depth of this test wrt testsuite root. We join ROOT and
diff --git a/testsuite/SUITE/cutils.py b/testsuite/SUITE/cutils.py
index 79093cb79..556c9af99 100644
--- a/testsuite/SUITE/cutils.py
+++ b/testsuite/SUITE/cutils.py
@@ -193,23 +193,22 @@ class Wdir:
     Simple helper to handle working directories.
     """
 
-    def __init__(self, subdir=None, clean=True):
+    def __init__(self, subdir=None):
         """
         If `subdir` is passed, create a subdirectory with this name and move
-        there. If `clean`, make sure it's removed first.
+        there.
         """
         self.homedir = os.getcwd()
         if subdir:
-            self.to_subdir(subdir, clean)
+            self.to_subdir(subdir)
 
-    def to_subdir(self, dir, clean=True):
+    def to_subdir(self, dir):
         """
         Change the current directory to `dir`, relative to `self`'s home
-        directory. Create it if needed, after first removing it if requested
-        to be `clean`.
+        directory. Create it if needed, after first removing it.
         """
         self.to_homedir()
-        if clean and os.path.exists(dir):
+        if os.path.exists(dir):
             shutil.rmtree(dir)
         mkdir(dir)
         cd(dir)
diff --git a/testsuite/SUITE/tutils.py b/testsuite/SUITE/tutils.py
index 4a6ccb4ef..b10dc8b57 100644
--- a/testsuite/SUITE/tutils.py
+++ b/testsuite/SUITE/tutils.py
@@ -8,6 +8,7 @@
 
 # ***************************************************************************
 
+import glob
 import os
 import time
 
@@ -336,9 +337,40 @@ def tracename_for(pgmname):
     return exename_for(pgmname) + ".trace"
 
 
-def srctracename_for(pgmname):
-    """Name for the source trace file for the given program name"""
-    return exename_for(pgmname) + ".srctrace"
+def srctrace_pattern_for(pgmname):
+    """Glob pattern for the source trace file for the given program name"""
+    return exename_for(pgmname) + "-*.srctrace"
+
+
+def srctracename_for(pgmname, register_failure=True):
+    """
+    Name for the source trace file for the given program name.
+
+    Since source trace files is not predictible, we need to do produce the
+    source trace file first and then look for a file matching a pattern to find
+    it.
+
+    If we find zero or multiple traces and "register_failure" is True, this
+    stops the testcase. If "register_failure" is False, we just return None in
+    that case.
+    """
+    pattern = srctrace_pattern_for(pgmname)
+    trace_files = glob.glob(pattern)
+
+    if len(trace_files) == 1:
+        return trace_files[0]
+
+    elif register_failure:
+        thistest.stop(
+            FatalError(
+                "Exactly one trace expected matching:"
+                f"\n  {pattern}"
+                f"\nBut got {len(trace_files)} traces instead"
+            )
+        )
+
+    else:
+        return None
 
 
 def ckptname_for(pgmname):
@@ -476,12 +508,13 @@ def xcov_suite_args(covcmd, covargs,
     return result
 
 
-def cmdrun(cmd, inp=None, out=None, err=None, register_failure=True):
+def cmdrun(cmd, inp=None, out=None, err=None, env=None, register_failure=True):
     """
     Execute the command+args list in CMD, redirecting its input, output and
-    error streams to INP, OUT and ERR when not None, respectively. Stop with a
-    FatalError if the execution status is not zero and REGISTER_FAILURE is
-    True. Return the process descriptor otherwise.
+    error streams to INP, OUT and ERR when not None, respectively. If ENV is
+    not None, pass it as the subprocess environment. Stop with a FatalError if
+    the execution status is not zero and REGISTER_FAILURE is True. Return the
+    process descriptor otherwise.
     """
 
     # Setup a dictionary of Run input/output/error arguments for which a
@@ -489,7 +522,8 @@ def cmdrun(cmd, inp=None, out=None, err=None, register_failure=True):
 
     kwargs = {
         key: value
-        for key, value in [('input', inp), ('output', out), ('error', err)]
+        for key, value in [('input', inp), ('output', out), ('error', err),
+                           ('env', env)]
         if value
     }
 
@@ -503,7 +537,7 @@ def cmdrun(cmd, inp=None, out=None, err=None, register_failure=True):
     return p
 
 
-def xcov(args, out=None, err=None, inp=None, register_failure=True,
+def xcov(args, out=None, err=None, inp=None, env=None, register_failure=True,
          auto_config_args=True, auto_target_args=True):
     """
     Run xcov with arguments ARGS, timeout control, valgrind control if
@@ -535,7 +569,7 @@ def xcov(args, out=None, err=None, inp=None, register_failure=True,
     # The gprvar options are only needed for the "libsupport" part of our
     # projects. They are pointless wrt coverage run or analysis activities
     # so we don't include them here.
-    p = cmdrun(cmd=covpgm + covargs, inp=inp, out=out, err=err,
+    p = cmdrun(cmd=covpgm + covargs, inp=inp, out=out, err=err, env=env,
                register_failure=register_failure)
 
     if thistest.options.enable_valgrind == 'memcheck':
@@ -549,8 +583,8 @@ def xcov(args, out=None, err=None, inp=None, register_failure=True,
     return p
 
 
-def xrun(args, out=None, register_failure=True, auto_config_args=True,
-         auto_target_args=True):
+def xrun(args, out=None, env=None, register_failure=True,
+         auto_config_args=True, auto_target_args=True):
     """
     Run <xcov run> with arguments ARGS for the current target, performing
     operations only relevant to invocations intended to execute a program (for
@@ -589,13 +623,13 @@ def xrun(args, out=None, register_failure=True, auto_config_args=True,
         runargs.extend(["-exec-trace-limit",
                         thistest.options.trace_size_limit])
 
-    return xcov(['run'] + runargs, inp=nulinput, out=out,
+    return xcov(['run'] + runargs, inp=nulinput, out=out, env=env,
                 register_failure=register_failure,
                 auto_config_args=auto_config_args,
                 auto_target_args=auto_target_args)
 
 
-def run_cov_program(executable, out=None, register_failure=True):
+def run_cov_program(executable, out=None, env=None, register_failure=True):
     """
     Assuming that `executable` was instrumented, run it according to the
     current target.
@@ -605,15 +639,15 @@ def run_cov_program(executable, out=None, register_failure=True):
     # If we are in a cross configuration, run the program using GNATemulator
     if thistest.options.target:
         kernel = thistest.options.kernel
-        board = thistest.options.board or env.target.machine
-        args.append('{}-gnatemu'.format(env.target.triplet))
+        board = thistest.options.board or thistest.env.target.machine
+        args.append('{}-gnatemu'.format(thistest.env.target.triplet))
         if kernel:
             args.append('--kernel=' + kernel)
         if board:
             args.append('--board=' + board)
 
     args.append(executable)
-    return cmdrun(args, out=out, register_failure=register_failure)
+    return cmdrun(args, out=out, env=env, register_failure=register_failure)
 
 
 def do(command):
diff --git a/tools/gnatcov/Makefile b/tools/gnatcov/Makefile
index 4de1b0f97..e79190a5f 100644
--- a/tools/gnatcov/Makefile
+++ b/tools/gnatcov/Makefile
@@ -309,7 +309,7 @@ install-doc: $(foreach fmt, $(DOCFORMATS), install-doc.$(fmt))
 install-gnatcov_rts:
 	$(RM) -r $(PREFIX)/share/$(DIRNAME)/gnatcov_rts
 	$(MKDIR) $(PREFIX)/share/$(DIRNAME)/gnatcov_rts
-	$(CP) -r rts/*.gpr rts/*.ad* $(PREFIX)/share/$(DIRNAME)/gnatcov_rts
+	$(CP) -r rts/*.gpr rts/*.ad* rts/*.c rts/*.h $(PREFIX)/share/$(DIRNAME)/gnatcov_rts
 
 install-lib:
 	$(MKDIR) $(PREFIX)/lib/gnatcoverage
diff --git a/tools/gnatcov/argparse.adb b/tools/gnatcov/argparse.adb
index 8ab79327c..c92e04a0e 100644
--- a/tools/gnatcov/argparse.adb
+++ b/tools/gnatcov/argparse.adb
@@ -178,6 +178,19 @@ package body Argparse is
       return +Result;
    end Option_Name;
 
+   -------------------
+   -- Value_Or_Null --
+   -------------------
+
+   function Value_Or_Null (Opt : String_Option) return Unbounded_String is
+   begin
+      if Opt.Present then
+         return Opt.Value;
+      else
+         return Null_Unbounded_String;
+      end if;
+   end Value_Or_Null;
+
    ----------------
    -- Is_Present --
    ----------------
diff --git a/tools/gnatcov/argparse.ads b/tools/gnatcov/argparse.ads
index 517ecee69..1ae97e519 100644
--- a/tools/gnatcov/argparse.ads
+++ b/tools/gnatcov/argparse.ads
@@ -2,7 +2,7 @@
 --                                                                          --
 --                               GNATcoverage                               --
 --                                                                          --
---                        Copyright (C) 2015, AdaCore                       --
+--                     Copyright (C) 2015-2020, AdaCore                     --
 --                                                                          --
 -- GNATcoverage is free software; you can redistribute it and/or modify it  --
 -- under terms of the GNU General Public License as published by the  Free  --
@@ -168,7 +168,8 @@ package Argparse is
      with Pre => Long_Name'Length > 0 or else Short_Name'Length > 0;
    --  Create a single string option description. Long_Name and Short_Name are
    --  |-separated lists of options names. If At_Most_Once is true, the command
-   --  cannot appear multiple times on the command-line.
+   --  cannot appear multiple times on the command-line; otherwise, the
+   --  retained value is the one from the last occurence on the command line.
 
    function Create
      (Long_Name, Short_Name, Help : String := "";
@@ -284,6 +285,9 @@ package Argparse is
    --  not appear on the command-line and the case when the option specified an
    --  empty value. This is specified thanks to the Present distriminant.
 
+   function Value_Or_Null (Opt : String_Option) return Unbounded_String;
+   --  If Opt is present, return its value. Return the empty string otherwise.
+
    type Bool_Array is array (Bool_Options) of Boolean;
    type String_Array is array (String_Options) of String_Option;
    type String_List_Array is
diff --git a/tools/gnatcov/command_line.ads b/tools/gnatcov/command_line.ads
index 71e9ffc08..b86ecc9c1 100644
--- a/tools/gnatcov/command_line.ads
+++ b/tools/gnatcov/command_line.ads
@@ -2,7 +2,7 @@
 --                                                                          --
 --                               GNATcoverage                               --
 --                                                                          --
---                     Copyright (C) 2015-2020, AdaCore                     --
+--                     Copyright (C) 2015-2021, AdaCore                     --
 --                                                                          --
 -- GNATcoverage is free software; you can redistribute it and/or modify it  --
 -- under terms of the GNU General Public License as published by the  Free  --
@@ -19,7 +19,6 @@
 with Argparse;
 with Coverage;
 with Coverage.Tags;
-with Rundrv.Config;
 with Switches;
 
 package Command_Line is
@@ -77,7 +76,9 @@ package Command_Line is
       Opt_Pretty_Print,
       Opt_Keep_Reading_Traces,
       Opt_Externally_Built_Projects,
-      Opt_GNAT_Pragmas);
+      Opt_GNAT_Pragmas,
+      Opt_Dump_Filename_Simple);
+
    --  Set of boolean options we support. More complete descriptions below.
 
    type String_Options is
@@ -104,6 +105,8 @@ package Command_Line is
       Opt_Report_Title,
       Opt_Dump_Trigger,
       Opt_Dump_Channel,
+      Opt_Dump_Filename_Env_Var,
+      Opt_Dump_Filename_Prefix,
       Opt_Ada,
       Opt_Dump_Units_To);
    --  Set of string options we support. More complete descriptions below.
@@ -420,7 +423,15 @@ package Command_Line is
         (Long_Name => "--gnat-pragmas",
          Help      => "Dump the list of GNAT pragmas, from gnat_util.",
          Commands  => (Cmd_Dump_Pragmas => True, others => False),
-         Internal  => True));
+         Internal  => True),
+
+      Opt_Dump_Filename_Simple => Create
+        (Long_Name => "--dump-filename-simple",
+         Help      => "Valid only when --dump-channel=bin-file. Create simple"
+                      & " filenames for source trace files (no PID/timestamp"
+                      & " variations).",
+         Commands  => (Cmd_Instrument => True, others => False),
+         Internal  => False));
 
    String_Infos : constant String_Option_Info_Array :=
      (Opt_Project => Create
@@ -442,18 +453,16 @@ package Command_Line is
         (Long_Name    => "--target",
          Short_Name   => "-t",
          Pattern      => "[TARGET]",
-         Help         => ("When using projects files, state the target"
-                          & " toolchain prefix used to build the analyzed"
-                          & " programs. If project files don't already set the"
-                          & " target, this is required for correct project"
-                          & " files processing and correct execution target"
-                          & " selection with cross targets."
-                          & ASCII.LF & ASCII.LF
-                          & "Target must either match one of:" & ASCII.LF
-                          & "  " & Rundrv.Config.Available_Targets
-                          & ASCII.LF
-                          & "or there must be a TARGET-gnatemu program"
-                          & " available."),
+         Help         => ("State the target toolchain configuration used"
+                          & " to build the analyzed programs, as provided"
+                          & " to gprbuild. For cross or 32bit native"
+                          & " configurations, this switch, together with"
+                          & " its possible --RTS companion, is required for"
+                          & " all commands using project files unless the"
+                          & " root project provides the information with"
+                          & " ""Target""/""Runtime"" attributes. It is also"
+                          & " needed for ""run"" commands without a project"
+                          & " file."),
          At_Most_Once => True,
          Internal     => False),
       Opt_Runtime => Create
@@ -663,6 +672,21 @@ package Command_Line is
          At_Most_Once => False,
          Internal     => False,
          Pattern      => "bin-file|base64-stdout"),
+      Opt_Dump_Filename_Env_Var => Create
+        (Long_Name    => "--dump-filename-env-var",
+         Help         => "Valid only when --dump-channel=bin-file. Name of the"
+                         & " environment variable which, if set, contains the"
+                         & " filename for created source traces.",
+         Commands     => (Cmd_Instrument => True, others => False),
+         At_Most_Once => False,
+         Internal     => False),
+      Opt_Dump_Filename_Prefix => Create
+        (Long_Name    => "--dump-filename-prefix",
+         Help         => "Valid only when --dump-channel=bin-file. Select a"
+                         & " filename prefix for created source traces.",
+         Commands     => (Cmd_Instrument => True, others => False),
+         At_Most_Once => False,
+         Internal     => False),
 
       Opt_Ada => Create
         (Long_Name    => "--ada",
diff --git a/tools/gnatcov/coverage-source.adb b/tools/gnatcov/coverage-source.adb
index 896a760db..cec985658 100644
--- a/tools/gnatcov/coverage-source.adb
+++ b/tools/gnatcov/coverage-source.adb
@@ -1451,13 +1451,6 @@ package body Coverage.Source is
 
       for J in Stmt_Buffer'Range loop
 
-         --  TODO??? Currently we hard-code No_SC_Tag.
-         --  Need to add support for per-instance coverage
-
-         --  Mark SCO as coverable (there is a bit referencing it)
-
-         Set_Basic_Block_Has_Code (BM.Statement_Bits (J), No_SC_Tag);
-
          --  If bit is set, statement has been executed
 
          if Stmt_Buffer (J) then
@@ -1716,6 +1709,42 @@ package body Coverage.Source is
       end if;
    end Initialize_SCI;
 
+   ----------------------------------------
+   -- Initialize_SCI_For_Instrumented_CU --
+   ----------------------------------------
+
+   procedure Initialize_SCI_For_Instrumented_CU (CU : CU_Id) is
+
+      procedure Process_SCI (SCI : in out Source_Coverage_Info);
+      --  Callback for Update_SCI. Set SCI (assumed to be a statement SCI) as
+      --  having code.
+
+      -----------------
+      -- Process_SCI --
+      -----------------
+
+      procedure Process_SCI (SCI : in out Source_Coverage_Info) is
+      begin
+         SCI.Basic_Block_Has_Code := True;
+      end Process_SCI;
+
+      Stmt_Bit_Map : Statement_Bit_Map renames
+        Bit_Maps (CU).Statement_Bits.all;
+
+   --  Start of processing for Initialize_SCI_For_Instrumented_CU
+
+   begin
+      --  Only create tag-less SCIs (No_SC_Tag) as per-instance coverage of
+      --  generics is not supported (see S628-011).
+
+      Initialize_SCI;
+      for Bit in Stmt_Bit_Map'Range loop
+         Update_SCI (SCO     => Stmt_Bit_Map (Bit),
+                     Tag     => No_SC_Tag,
+                     Process => Process_SCI'Access);
+      end loop;
+   end Initialize_SCI_For_Instrumented_CU;
+
    --------------------------
    -- Merge_Checkpoint_SCI --
    --------------------------
diff --git a/tools/gnatcov/coverage-source.ads b/tools/gnatcov/coverage-source.ads
index 22d93fc60..dadd7621c 100644
--- a/tools/gnatcov/coverage-source.ads
+++ b/tools/gnatcov/coverage-source.ads
@@ -33,6 +33,14 @@ package Coverage.Source is
    --  This can be called multiple times if SCO information is loaded in chunks
    --  (case of loading checkpointed coverage information).
 
+   procedure Initialize_SCI_For_Instrumented_CU (CU : CU_Id);
+   --  Initialize source coverage information vectors for obligations in CU,
+   --  assumed to come from source instrumentation.
+   --
+   --  A particularity here is that we automatically consider CU's statements
+   --  which have an allocated bit in trace buffers (see
+   --  SC_Obligations.Statement_Bit_Map) as having code.
+
    procedure Compute_Source_Coverage
      (Subp_Key  : Subprogram_Key;
       Subp_Info : Subprogram_Info;
diff --git a/tools/gnatcov/doc/umanual/cov_source.rst b/tools/gnatcov/doc/umanual/cov_source.rst
index 73ef301c9..bd67ed6a8 100644
--- a/tools/gnatcov/doc/umanual/cov_source.rst
+++ b/tools/gnatcov/doc/umanual/cov_source.rst
@@ -63,13 +63,7 @@ The available options are as follows:
 .. include:: cov_common_switches.rst
 
 :option:`-t`, :option:`--target` :
-  State the target architecture/board/ABI for which the analyzed program was
-  built.  This corresponds to the target prefix of your compilation toolchain,
-  for example ``powerpc-elf`` or ``leon-elf``, and can also be specified as a
-  ``Target`` attribute within the project file designated by :option:`-P`, if
-  any. By default, |gcv| assumes that this target is the same as the host
-  environment. Stating the correct target is required for correct processing
-  of project files.
+   .. include:: target_switch_common_text.rst
 
 :option:`--non-coverable`:
    Report about language statements for which no object code could be found in
diff --git a/tools/gnatcov/doc/umanual/getting_started.rst b/tools/gnatcov/doc/umanual/getting_started.rst
index 7ff452575..609c7499d 100644
--- a/tools/gnatcov/doc/umanual/getting_started.rst
+++ b/tools/gnatcov/doc/umanual/getting_started.rst
@@ -273,37 +273,21 @@ with a |gcvins| command like::
   gnatcov instrument --level=<> <units-of-interest>
     [--dump-trigger=<>] [--dump-channel=<>]
 
-- :option:`--dump-trigger` selects the execution point at which the output of
-  coverage data should be injected, if any. This is ``manual`` by default,
-  leaving to users the responsibility to emit the coverage data as they see
-  fit. ``atexit`` is a typically good choice for native environments.
-
-- When the triggering mechanism isn't ``manual``, :option:`--dump-channel`
-  selects the coverage data output medium. This is ``bin-file`` by default,
-  which requests the production of a trace file.  For runtime environments
-  that wouldn't support this, ``base64-stdout`` is a possible alternative where
-  the trace is emitted as base64 text on standard output through ``Ada.Text_IO``.
-  A trace file can be produced from a capture of the complete output in this case,
-  thanks to a ``gnatcov extract-base64-trace`` command.
-
-- The :option:`<units-of-interest>` options may only resort to project file
-  facilities, with at least a :option:`-P<project>` option designating the
-  project file name you would pass to :command:`gprbuild` for building the
-  program.
-
-Note that the instrumentation performed to honor a :option:`dump-trigger`
-option other than ``manual``, intended to output the coverage data, is of a
-different kind than the instrumentation performed on units of interest,
-intended to collect the coverage data in the first place. Main units which are
-not also declared of interest are instrumented only to enable the output of
-coverage data gathered by the units of interest.
+
+:option:`--dump-trigger` and :option:`--dump-channel` select the execution
+point at which the output of coverage data should be injected and the output
+medium, respectively, with a variety of possibilities to select depending on
+the runtime environment capabilities.  This might involve two kinds of
+instrumentation: one on main units to output the coverage data after it has
+been gathered, and one on the units of interest to collect the coverage data
+in the first place.
 
 After instrumentation, building the program using instrumented source is
 achieved with a :command:`gprbuild` command like::
 
   gprbuild -P<project> --src-subdirs=gnatcov-instr --implicit-with=gnatcov_rts_full.gpr
 
-after having set ``GPR_PROJECT_PATH`` to designate the directory where the
+``GPR_PROJECT_PATH`` should be set to designate the directory where the
 coverage runtime has been installed if that is not a place where
 :command:`gprbuild` would search by default (such that the GNAT installation
 prefix).
@@ -311,17 +295,7 @@ prefix).
 The production of coverage data is then simply achieved by executing the
 program.
 
-When the output takes the form of a trace file, the default behavior is to
-produce a file named ``<executable-name>.srctrace`` in the current
-directory. An alternative name/location can be selected by setting the
-``GNATCOV_TRACE_FILE`` environment variable. For cross configurations, one
-would more likely use a ``base64-stdout`` kind of output and rely on a
-restricted coverage runtime, not including the support for the production of
-trace files (``gnatcov_rts.gpr`` instead of ``gnatcov_rts_full.gpr``). A trace file
-can be produced offline by extracting the base64 coverage data from the
-execution output, thanks to a ``gnatcov extract-base64-trace`` command.
-
-Regardless, a general property of note here is that instrumentation works
+A general property of note here is that instrumentation works
 within the context of an existing project structure, just adding alternate
 versions of the sources in strategically chosen places. We do not replicate
 the entire project tree, not even project files. Instead, the
diff --git a/tools/gnatcov/doc/umanual/run_commandline.rst b/tools/gnatcov/doc/umanual/run_commandline.rst
index 4b08aff4d..bdaff3fd2 100644
--- a/tools/gnatcov/doc/umanual/run_commandline.rst
+++ b/tools/gnatcov/doc/umanual/run_commandline.rst
@@ -43,14 +43,14 @@ Then the available :option:`[OPTIONS]` are:
   options, as described in :ref:`sunits`.
 
 :option:`-t`, :option:`--target` :
-  State the target architecture/board/abi for which the analyzed program was
-  built.  This corresponds to the target prefix of your compilation toolchain,
-  for example ``powerpc-elf`` or ``leon-elf``, and can also be specified as a
-  ``Target`` attribute within the project file designated by -P, if any. This
-  is used to control the underlying execution engine used to run the program,
-  assumed to be the host environment by default. On the command line, a
-  possible ``,<board-name>`` extension is allowed as well. See the
-  :ref:`execution-control` section of this chapter for additional details.
+   .. include:: target_switch_common_text.rst
+
+   This is used to control the underlying execution engine used to run
+   the program, assumed to be the host environment by default. On the
+   command line, a possible ``,<board-name>`` extension is allowed as
+   well. See the :ref:`execution-control` section of this chapter for
+   additional details.
+
 
 :option:`--kernel` :
   Tell the underlying emulator that the executable program actually
diff --git a/tools/gnatcov/doc/umanual/src_traces.rst b/tools/gnatcov/doc/umanual/src_traces.rst
index 097397302..af6ad986d 100644
--- a/tools/gnatcov/doc/umanual/src_traces.rst
+++ b/tools/gnatcov/doc/umanual/src_traces.rst
@@ -6,18 +6,18 @@ Producing source traces with |gcvins|
 
 The production of :term:`source traces` is performed by an instrumented
 version of the original program running in its regular execution
-environment. Alternative sources are generated for units of interest, with additional
-data structures and code statements solely aimed at tracking coverage related
-information. Coverage data is output in accordance with a user selectable
-policy, for example upon exit of the program, for which the program main unit
-gets instrumented as well.
+environment. A |gcvins| command produces alternative sources for units of
+interest, with additional data structures and code statements solely aimed at
+tracking coverage related information. Coverage data is output in accordance
+with a user selectable policy, for example upon exit of the program, for which
+the program main unit gets instrumented as well.
 
 To gather coverage data while the program is running and to output this data
 in the form of a source trace file eventually, the instrumented code relies on
 common data types and subprograms provided by a :term:`coverage runtime`
 library.  The first thing to do for a given project is then to build and
 install the coverage runtime so it becomes available to the instrumented
-sources afterwards, as we will describe in the :ref:`instr-setup-rts` section
+sources afterwards, as we will describe in the :ref:`instr-rts` section
 of this chapter.
 
 Once the coverage runtime is setup, the simplest possible use of the
@@ -117,7 +117,7 @@ involve two distinct kinds of operations:
 - Modify the code in units-of-interest so the program records, while it is
   running, facts of relevance to the coverage metrics to be assessed,
 
-- Possibly modify the main unit(s) to output the so gathered coverage data to
+- Modify the main unit(s) to output the so gathered coverage data to
   an externally readable channel, typically either a source trace file or some
   communication port.
 
@@ -134,28 +134,35 @@ will allow assessing afterwards and the :option:`<units-of-interest>` switches
 specify the set of units for which such assessment will be possible. The
 latter may only resort to project file facilities, as described in the
 :ref:`passing_gpr` section of this manual. Projects marked ``Externally_Built``
-In the closure are not instrumented or otherwise modified.
+in the closure are not instrumented or otherwise modified.
 
-The :option:`[OPTIONS]` of particular interest to this manual are those
-controlling the instrumentation of main units, if any are designated by the
-root project:
+A few :option:`[OPTIONS]` allow controlling the instrumentation of main units,
+if any are designated by the root project:
 
-- :option:`--dump-trigger` selects the execution point at which the output of
-  coverage data should be injected in main units. This is ``manual`` by
-  default, leaving to users the responsibility to emit the coverage data as
-  they see fit. Other possible choices are ``atexit``, ``main-end`` and
-  ``ravenscar-task-termination``.
+:option:`--dump-trigger`
+   selects the execution point at which the output of
+   coverage data should be injected in main units. This is ``manual`` by
+   default, leaving to users the responsibility to emit the coverage data as
+   they see fit. Other possible choices are ``atexit``, ``main-end`` and
+   ``ravenscar-task-termination``.
 
-- :option:`--dump-channel` selects the mechanism used to output coverage data
-  at the selected triggering point, if any. The possible choices are
-  ``bin-file``, to create a source trace file, or ``base64-stdout`` to emit a
-  base64 encoded version of the data through ``Ada.Text_IO``. ``bin-file`` is the
-  default.
+:option:`--dump-channel`
+   selects the mechanism used to output coverage data
+   at the selected triggering point, if any. The possible choices are
+   ``bin-file``, to create a source trace file, or ``base64-stdout`` to emit a
+   base64 encoded version of the data through ``Ada.Text_IO``. ``bin-file`` is
+   the default.
+
+:option:`--externally-built-projects`
+   instructs the instrumenter to look into projects marked as externally built
+   when computing the list of units of interest (they are ignored by default),
+   for the sole purpose of instrumenting mains.
+
+In addtion, for trace files produced automatically from a ``bin-file``
+dump-channel, the ``--dump-filename-<>`` family of switches provides control
+over the name of trace files. See :ref:`instr-tracename` for more details on
+the default behavior and possibilities to alter it.
 
-- :option:`--externally-built-projects` instructs the instrumenter to look
-  into projects marked as externally built when computing the list of units of
-  interest (they are ignored by default), for the sole purpose of
-  instrumenting mains.
 
 Output strategies for main units
 --------------------------------
@@ -186,38 +193,63 @@ data. You will have to emit this data somehow to allow analysing coverage
 afterwards, still, and can of course experiment with other possibilities just
 to get examples of possible ways to proceed.
 
-.. _instr-compose:
+.. _instr-tracename:
 
-Composed instrumentation
-------------------------
+Controlling trace file names
+----------------------------
 
-To prevent unnecessary re-instrumentation and re-build of components which
-don't change, |gcp| allows partial instrumentations to be combined together. A
-common use case would be the testing of library components, where the library
-doesn't change and its coverage needs to be assessed incrementally as new
-tests get developed.
+When an instrumented program produces a trace file through a ``bin-file``
+dump-channel, the file is by default created in the current working directory
+at the data output point (for example, at exit time for an ``atexit``
+dump-trigger), and named as ``<ename>-<istamp>-<pid>-<estamp>.srctrace``,
+where:
 
-In such situations, the process would become something like:
+- ``<ename>`` is the executable name,
 
-#. Setup or reuse a separate project file for the library, which normally
-   wouldn't have any main unit;
-#. Instrument the library using this project as the root project;
-#. Build the instrumented library;
+- ``<istamp>`` is the instrumentation time stamp, representing the time at
+  which the instrumentation took place,
 
-Then for each new test:
+- ``<pid>`` is the execution process identifier,
 
-#. Setup or reuse a separate project file for the test, designating the main
-   unit if you wish to leverage the instrumenter's ability to insert the
-   coverage coverage data output code. Setup a dependency from this project on
-   the library project, with an ``Externally_Built`` attribute set to ``"True"``;
-#. Instrument the testing code main unit alone;
-#. Build a program combining the library (instrumented for coverage
-   measurement) and the testing code (instrumented to output the gathered
-   coverage data);
-#. Execute the program to produce a trace.
+- ``<estamp>`` is an execution time stamp, representing the time at which
+  coverage data was written out to the file.
+
+The ``<estamp>`` and ``<pid>`` components are intented to ensure that parallel
+executions of the program from the same working directory write out to
+different files. The ``<istamp>`` component allows distinguishing traces
+issued from different versions of the program. These three components are
+expressed as hexadecimal integers to limit the growth of file name lengths.
+
+This default behavior can be influenced in several manners. First:
+
+* The :option:`--dump-filename-prefix` switch to |gcvins| requests replacing
+  the ``<ename>`` component by the switch argument;
+
+* The :option:`--dump-filename-simple` switch requests the removal of the
+  variable components (stamps and pid), so only the ``<ename>`` component
+  remains or the replacement provided by :option:`--dump-filename-prefix` if
+  that switch is also used.
 
-The following sections provide details on the build and execution steps, then
-a couple of illustrated use cases.
+
+The use of a specific location for the file, or of a specific file name can be
+requested at run time by setting the ``GNATCOV_TRACE_FILE`` variable in the
+program's environment.
+
+If the variable value ends with a ``/`` or ``\`` character, this value is
+interpreted as the name of a directory where the trace file is to be produced,
+following the rules we have just described for the file base name. The
+directory reference may be a full or a relative path, resolved at the trace
+file creation point and expected to exist at that time.
+
+If the variable value does *not* end with a ``/`` or ``\`` character, the
+value is used directly as the name of the file to create. This name may hold a
+path specification, full or relative, also resolved at the trace file creation
+point and the directories involved are expected to exist at that time.
+
+For specific needs of programs wishing to output to different places from
+within the same environment, the variable name for a program can actually be
+tailored by passing a :option:`--dump-filename-env-var` switch to |gcvins|,
+providing the variable name to use.
 
 
 .. _instr-build:
@@ -256,49 +288,60 @@ where :option:`<gnatcov_rts_gpr>` would be the coverage runtime project file
 setup beforehand for the project, as described previously in this
 chapter. This project file could be refered to with a full path specification,
 or with a simple basename if the ``GPR_PROJECT_PATH`` environment variable is
-updated to designate the directory where the coverage runtime has been
-installed.
+updated to designate the directory where the project file is located, which
+would be the ``share/gpr`` subdirectory of the runtime installation tree.
 
 While the scheme relies on the use of GNAT project files, it does not
 absolutely require :command:`gprbuild` to build the instrumented programs,
 even though we have augmented that builder with a few features to make that
 process very efficient and straightforward.
 
-Obtaining traces from instrumented programs
-===========================================
+Extracting a trace from standard output
+=======================================
 
-As a general principle, instrumented programs output coverage data to the
-requested channel when reaching an execution point where instrumentation
-arranged for it to do so, automatically or with user assistance, per the
-:option:`--dump-channel` and :option:`--dump-trigger` switches.
+With the :option:`base64-stdout` channel, coverage data is emitted
+with ``Ada.Text_IO`` on the program's standard output stream. The actual
+base64 encoded data is framed by start/end-of-coverage-data markers and |gcp|
+provides the |gcvxtr| command to extract this data from a captured output and
+create a trace file offline (outside of the program's execution context). The
+extraction command line simply is::
 
-Some procedural details are of interest, depending on the output channel.
+  gnatcov extract-base64-trace <captured-output> <output-trace-file>
+
+The captured output may be used directly, there is no need to first extract
+the trace data section.
+
+.. _instr-compose:
 
-When coverage data is written as a trace file
----------------------------------------------
+Composed instrumentation
+========================
 
-When an instrumented program produces a trace file directly, the output file
-is by default named ``<executable-name>.srctrace`` and placed in the current
-directory.
+To prevent unnecessary re-instrumentation and re-build of components which
+don't change, |gcp| allows partial instrumentations to be combined together. A
+common use case would be the testing of library components, where the library
+doesn't change and its coverage needs to be assessed incrementally as new
+tests get developed.
 
-This behavior can be influenced by setting the ``GNATCOV_TRACE_FILE`` variable
-in the program's environment, in which case the variable value is used as the
-file name to produce. This value may hold a full path specification and the
-designated directory is expected to exist when the program reaches the file
-creation point.
+In such situations, the process would become something like:
 
-When coverage data goes to standard output
-------------------------------------------
+#. Setup or reuse a separate project file for the library, which normally
+   wouldn't have any main unit;
+#. Instrument the library using this project as the root project;
+#. Build the instrumented library;
 
-With the :option:`base64-stdout` channel, coverage data is normally emitted
-with ``Ada.Text_IO`` on the program's standard output stream.
+Then for each new test:
 
-The actual base64 encoded data is framed by start/end-of-coverage-data markers
-and |gcp| provides the |gcvxtr| command to extract this data from a captured
-output and create a trace file offline (outside of the program's execution
-context). The extraction command line simply is::
+#. Setup or reuse a separate project file for the test, designating the main
+   unit if you wish to leverage the instrumenter's ability to insert the
+   coverage coverage data output code. Setup a dependency from this project on
+   the library project, with an ``Externally_Built`` attribute set to ``"True"``;
+#. Instrument the testing code main unit alone;
+#. Build a program combining the library (instrumented for coverage
+   measurement) and the testing code (instrumented to output the gathered
+   coverage data);
+#. Execute the program to produce a trace.
 
-  gnatcov extract-base64-trace <input-base64-file> <output-trace-file>
+The following section illustrates such a use case.
 
 Example use cases
 =================
@@ -358,7 +401,7 @@ For our intended target environment, this would be something like::
     -p --prefix=<gnatcov_rts-ppc-install-dir>
 
   # Allow references to the coverage runtime project from other project files:
-  export GPR_PROJECT_PATH=<gnatcov_rts-ppc-install-dir>
+  export GPR_PROJECT_PATH=<gnatcov_rts-ppc-install-dir>/share/gpr
 
 Instrument and build
 ********************
@@ -462,7 +505,7 @@ the default full Ada runtime (no specific :option:`--RTS` option)::
   gprinstall -Pgnatcov_rts_full.gpr -p --prefix=<gnatcov_rts-install-dir>
 
   # Allow references to the coverage runtime project from other project files:
-  export GPR_PROJECT_PATH=<gnatcov_rts-install-dir>
+  export GPR_PROJECT_PATH=<gnatcov_rts-install-dir>/share/gpr
 
 Project file architecture
 *************************
diff --git a/tools/gnatcov/gnatcov.adb b/tools/gnatcov/gnatcov.adb
index a5a46d004..8102e3229 100644
--- a/tools/gnatcov/gnatcov.adb
+++ b/tools/gnatcov/gnatcov.adb
@@ -2,7 +2,7 @@
 --                                                                          --
 --                               GNATcoverage                               --
 --                                                                          --
---                     Copyright (C) 2008-2020, AdaCore                     --
+--                     Copyright (C) 2008-2021, AdaCore                     --
 --                                                                          --
 -- GNATcoverage is free software; you can redistribute it and/or modify it  --
 -- under terms of the GNU General Public License as published by the  Free  --
@@ -1442,63 +1442,70 @@ begin
 
             Dump_Trigger_Opt : String_Option renames
                Args.String_Args (Opt_Dump_Trigger);
-            Dump_Trigger     : Any_Dump_Trigger := Manual;
-
             Dump_Channel_Opt : String_Option renames
                Args.String_Args (Opt_Dump_Channel);
-            Dump_Channel     : Any_Dump_Channel := Binary_File;
+
+            Dump_Filename_Simple      : Boolean renames
+               Args.Bool_Args (Opt_Dump_Filename_Simple);
+            Dump_Filename_Env_Var_Opt : String_Option renames
+               Args.String_Args (Opt_Dump_Filename_Env_Var);
+            Dump_Filename_Prefix_Opt  : String_Option renames
+               Args.String_Args (Opt_Dump_Filename_Prefix);
 
             Language_Version_Opt : String_Option renames
                Args.String_Args (Opt_Ada);
+
+            Dump_Config      : Any_Dump_Config := (others => <>);
             Language_Version : Any_Language_Version := Ada_2012;
          begin
             Create_Ignored_Source_Files_Matcher (Matcher, Has_Matcher);
 
+            --  Create the appropritae dump configuration depending on
+            --  command-line options. Unless --dump-channel is passed, the dump
+            --  channel is "bin-file".
+
+            declare
+               Value : constant String :=
+                 (if Dump_Channel_Opt.Present
+                  then +Dump_Channel_Opt.Value
+                  else "bin-file");
+            begin
+               if Value = "bin-file" then
+                  Dump_Config :=
+                    (Channel          => Binary_File,
+                     Trigger          => <>,
+                     Filename_Simple  => Dump_Filename_Simple,
+                     Filename_Env_Var =>
+                        Value_Or_Null (Dump_Filename_Env_Var_Opt),
+                     Filename_Prefix  =>
+                        Value_Or_Null (Dump_Filename_Prefix_Opt));
+               elsif Value = "base64-stdout" then
+                  Dump_Config :=
+                    (Channel => Base64_Standard_Output,
+                     Trigger => <>);
+               else
+                  Fatal_Error ("Bad buffers dump channel: " & Value);
+               end if;
+            end;
+
             if Dump_Trigger_Opt.Present then
                declare
                   Value : constant String := +Dump_Trigger_Opt.Value;
                begin
                   if Value = "manual" then
-                     Dump_Trigger := Manual;
+                     Dump_Config.Trigger := Manual;
                   elsif Value = "atexit" then
-                     Dump_Trigger := At_Exit;
+                     Dump_Config.Trigger := At_Exit;
                   elsif Value = "ravenscar-task-termination" then
-                     Dump_Trigger := Ravenscar_Task_Termination;
+                     Dump_Config.Trigger := Ravenscar_Task_Termination;
                   elsif Value = "main-end" then
-                     Dump_Trigger := Main_End;
+                     Dump_Config.Trigger := Main_End;
                   else
                      Fatal_Error ("Bad buffers dump trigger: " & Value);
                   end if;
                end;
             end if;
 
-            if Dump_Channel_Opt.Present then
-               declare
-                  Value : constant String := +Dump_Channel_Opt.Value;
-               begin
-                  if Value = "bin-file" then
-                     Dump_Channel := Binary_File;
-                  elsif Value = "base64-stdout" then
-                     Dump_Channel := Base64_Standard_Output;
-                  else
-                     Fatal_Error ("Bad buffers dump channel: " & Value);
-                  end if;
-               end;
-            end if;
-
-            --  Reject invalid combinations of --dump-trigger and
-            --  --dump-channel.
-
-            if Dump_Trigger = At_Exit
-               and then Dump_Channel = Base64_Standard_Output
-            then
-               --  When atexit handlers are triggered, the runtime finalized
-               --  Ada.Text_IO, so Standard_Output is closed.
-
-               Fatal_Error ("--dump-trigger=atexit is not compatible with"
-                            & " --dump-channel=base64-stdout");
-            end if;
-
             if Language_Version_Opt.Present then
                declare
                   Value : constant String := +Language_Version_Opt.Value;
@@ -1515,9 +1522,24 @@ begin
                end;
             end if;
 
+            if Dump_Config.Channel /= Binary_File then
+               if Dump_Filename_Simple then
+                  Fatal_Error
+                    ("--dump-filename-simple requires"
+                     & " --dump-channel=bin-file");
+               elsif Dump_Filename_Env_Var_Opt.Present then
+                  Fatal_Error
+                    ("--dump-filename-env-var requires"
+                     & " --dump-channel=bin-file");
+               elsif Dump_Filename_Env_Var_Opt.Present then
+                  Fatal_Error
+                    ("--dump-filename-prefix requires"
+                     & " --dump-channel=bin-file");
+               end if;
+            end if;
+
             Instrument.Instrument_Units_Of_Interest
-              (Dump_Trigger         => Dump_Trigger,
-               Dump_Channel         => Dump_Channel,
+              (Dump_Config          => Dump_Config,
                Language_Version     => Language_Version,
                Ignored_Source_Files =>
                  (if Has_Matcher then Matcher'Access else null));
diff --git a/tools/gnatcov/instrument-common.adb b/tools/gnatcov/instrument-common.adb
index eb8d68346..264faf78c 100644
--- a/tools/gnatcov/instrument-common.adb
+++ b/tools/gnatcov/instrument-common.adb
@@ -23,11 +23,15 @@ pragma Warnings (Off, "* is an internal GNAT unit");
 with Ada.Strings.Wide_Wide_Unbounded.Aux;
 pragma Warnings (On, "* is an internal GNAT unit");
 with Ada.Unchecked_Deallocation;
+with Interfaces;
+
+with GNAT.OS_Lib;
 
 with Langkit_Support.Text;
 with Libadalang.Common;
 with Libadalang.Sources;
 
+with Hex_Images;
 with Outputs; use Outputs;
 with Project;
 
@@ -657,8 +661,7 @@ package body Instrument.Common is
 
    function Create_Context
      (Provider             : Libadalang.Analysis.Unit_Provider_Reference;
-      Dump_Trigger         : Any_Dump_Trigger;
-      Dump_Channel         : Any_Dump_Channel;
+      Dump_Config          : Any_Dump_Config;
       Language_Version     : Any_Language_Version;
       Ignored_Source_Files : access GNAT.Regexp.Regexp) return Inst_Context is
    begin
@@ -667,13 +670,27 @@ package body Instrument.Common is
            (Project.Root_Project_Filename);
          --  TODO??? Get the original casing for the project name
 
+         --  Compute the tag for default source trace filenames. Use the
+         --  current time as a mostly unique identifier. Put it in hexadecimal
+         --  form without leading zeros to avoid too long names.
+
+         declare
+            use Interfaces;
+
+            Time : constant Unsigned_64 :=
+              Unsigned_64 (GNAT.OS_Lib.To_C (GNAT.OS_Lib.Current_Time));
+            Tag  : constant String :=
+               Hex_Images.Strip_Zero_Padding (Hex_Images.Hex_Image (Time));
+         begin
+            IC.Tag := +Tag;
+         end;
+
          IC.Provider := Provider;
          IC.Context := Libadalang.Analysis.Create_Context
            (Unit_Provider => Provider);
          IC.Get_From_File_Count := 0;
 
-         IC.Dump_Trigger := Dump_Trigger;
-         IC.Dump_Channel := Dump_Channel;
+         IC.Dump_Config := Dump_Config;
          IC.Language_Version := Language_Version;
 
          IC.Ignored_Source_Files_Present := Ignored_Source_Files /= null;
diff --git a/tools/gnatcov/instrument-common.ads b/tools/gnatcov/instrument-common.ads
index 9d660790c..f9c90d42d 100644
--- a/tools/gnatcov/instrument-common.ads
+++ b/tools/gnatcov/instrument-common.ads
@@ -311,6 +311,18 @@ package Instrument.Common is
       Project_Name : Ada.Strings.Unbounded.Unbounded_String;
       --  Name of the root project. It is also used to name the list of buffers
 
+      Tag : Ada.Strings.Unbounded.Unbounded_String;
+      --  String which allows differentiating trace files produced by a
+      --  specific program instrumentation from the ones produced by other
+      --  instrumentations.
+      --
+      --  To achieve this, Tag is based on the date/time at which the
+      --  instrumentation takes place. Automatic coverage buffer dumps (in
+      --  instrumented mains) will pass this string to
+      --  GNATcov_RTS.Traces.Output.Files.Default_Trace_Name (unless the
+      --  --dump-trace-filename-simple option is passed to "gnatcov
+      --  instrument").
+
       Provider : Libadalang.Analysis.Unit_Provider_Reference;
       --  Unit provider to create an analysis context (Context member below)
 
@@ -321,8 +333,7 @@ package Instrument.Common is
       --  Count how many times we called Context.Get_From_File. See the
       --  Max_Get_From_File_Count constant.
 
-      Dump_Trigger     : Any_Dump_Trigger;
-      Dump_Channel     : Any_Dump_Channel;
+      Dump_Config      : Any_Dump_Config;
       Language_Version : Any_Language_Version;
       --  See the eponym arguments in Instrument.Intrument_Units_Of_Interest
 
@@ -342,8 +353,7 @@ package Instrument.Common is
 
    function Create_Context
      (Provider             : Libadalang.Analysis.Unit_Provider_Reference;
-      Dump_Trigger         : Any_Dump_Trigger;
-      Dump_Channel         : Any_Dump_Channel;
+      Dump_Config          : Any_Dump_Config;
       Language_Version     : Any_Language_Version;
       Ignored_Source_Files : access GNAT.Regexp.Regexp) return Inst_Context;
    --  Create an instrumentation context for the currently loaded project
@@ -378,7 +388,7 @@ package Instrument.Common is
       Mains   : in out Main_To_Instrument_Vectors.Vector;
       File    : GNATCOLL.VFS.Virtual_File;
       Project : Project_Type)
-      with Pre => Context.Dump_Trigger /= Manual;
+      with Pre => Context.Dump_Config.Trigger /= Manual;
    --  Register in Mains a main to be instrumented so that it dumps coverage
    --  buffers. File is the source file for this main, and Project is the
    --  project that owns this main. If File is actually a unit of interest in
diff --git a/tools/gnatcov/instrument-find_units.adb b/tools/gnatcov/instrument-find_units.adb
index 919615210..edcf96bbf 100644
--- a/tools/gnatcov/instrument-find_units.adb
+++ b/tools/gnatcov/instrument-find_units.adb
@@ -91,9 +91,16 @@ begin
       raise Xcov_Exit_Exc;
    end if;
 
-   --  Abort if we have several compilation units per file
+   --  We cannot instrument files that contain only pragmas, but they are still
+   --  valid sources in the context of the GNAT runtime (for instance
+   --  g-os_lib.adb), so just ignore them.
 
-   if Unit.Root.Kind = Ada_Compilation_Unit_List then
+   if Unit.Root.Kind = Ada_Pragma_Node_List then
+      return;
+
+   --  Abort if a source file does not contain exactly one compilation unit
+
+   elsif Unit.Root.Kind = Ada_Compilation_Unit_List then
       Error ("instrumentation failed for " & Input_Filename);
       Error ("source files containing multiple compilation units are not"
              & " supported");
diff --git a/tools/gnatcov/instrument-sources.adb b/tools/gnatcov/instrument-sources.adb
index 3432a9135..1a51f0007 100644
--- a/tools/gnatcov/instrument-sources.adb
+++ b/tools/gnatcov/instrument-sources.adb
@@ -17,12 +17,12 @@
 ------------------------------------------------------------------------------
 
 with Ada.Characters.Conversions; use Ada.Characters.Conversions;
+with Ada.Containers;
 with Ada.Exceptions;
+with Ada.Strings;
 
 with GNATCOLL.Projects; use GNATCOLL.Projects;
 
-with Libadalang.Common; use Libadalang.Common;
-
 with SCOs;
 
 with Coverage;        use Coverage;
@@ -79,6 +79,13 @@ package body Instrument.Sources is
    --  Wrapper around E.P_Expression_Type, logging a warning and returning
    --  Standard.Boolean if unable to determine the type.
 
+   function Referenced_Defining_Name
+     (Main_Name : Ada_Qualified_Name;
+      N         : LAL.Name) return Defining_Name;
+   --  Wrapper around Name.P_Referenced_Defining_Name, logging a warning and
+   --  returning No_Defining_Name if unable to determine the referenced
+   --  defining name.
+
    -------------------------------------
    -- Generation of witness fragments --
    -------------------------------------
@@ -384,7 +391,7 @@ package body Instrument.Sources is
       --  Qualified names for the unit that contains the buffer output
       --  procedure, and for the procedure itself.
 
-      Dump_Trigger : constant Auto_Dump_Trigger := IC.Dump_Trigger;
+      Dump_Trigger : constant Auto_Dump_Trigger := IC.Dump_Config.Trigger;
       --  Shortcut to avoid repeatedly restricting the dump trigger to the
       --  Auto_Dump_Trigger subtype.
 
@@ -402,7 +409,7 @@ package body Instrument.Sources is
 
       declare
          use type Ada_Qualified_Name;
-         Unit : constant String := (case IC.Dump_Channel is
+         Unit : constant String := (case IC.Dump_Config.Channel is
                                     when Binary_File            => "Files",
                                     when Base64_Standard_Output => "Base64");
       begin
@@ -499,10 +506,36 @@ package body Instrument.Sources is
             end;
          end loop;
 
-         case IC.Dump_Channel is
+         case IC.Dump_Config.Channel is
          when Binary_File =>
-            File.Put ("         Filename => "
-                      & To_Ada (Output_Unit) & ".Default_Trace_Filename");
+            declare
+               U       : constant String := To_Ada (Output_Unit);
+               Indent1 : constant String := "         ";
+               Indent2 : constant String := Indent1 & "  ";
+
+               Env_Var : constant String :=
+                 (if Length (IC.Dump_Config.Filename_Env_Var) = 0
+                  then U & ".Default_Trace_Filename_Env_Var"
+                  else """" & To_String (IC.Dump_Config.Filename_Env_Var)
+                       & """");
+               Prefix  : constant String :=
+                 (if Length (IC.Dump_Config.Filename_Prefix) = 0
+                  then U & ".Default_Trace_Filename_Prefix"
+                  else """" & To_String (IC.Dump_Config.Filename_Prefix)
+                       & """");
+               Tag     : constant String := """" & To_String (IC.Tag) & """";
+               Simple  : constant String :=
+                 (if IC.Dump_Config.Filename_Simple
+                  then "True"
+                  else "False");
+            begin
+               File.Put_Line
+                 (Indent1 & "Filename => " & U & ".Default_Trace_Filename");
+               File.Put_Line (Indent2 & "(Env_Var => " & Env_Var & ",");
+               File.Put_Line (Indent2 & " Prefix => " & Prefix & ",");
+               File.Put_Line (Indent2 & " Tag => " & Tag & ",");
+               File.Put (Indent2 & " Simple => " & Simple & ")");
+            end;
 
          when Base64_Standard_Output =>
 
@@ -622,6 +655,78 @@ package body Instrument.Sources is
       end if;
    end Expression_Type;
 
+   ------------------------------
+   -- Referenced_Defining_Name --
+   ------------------------------
+
+   function Referenced_Defining_Name
+     (Main_Name : Ada_Qualified_Name;
+      N         : LAL.Name) return Defining_Name
+   is
+      DF : Defining_Name;
+   begin
+      begin
+         DF := N.P_Referenced_Defining_Name;
+
+         if DF.Is_Null then
+            Report
+              (Kind => Warning,
+               Msg  => "Failed to determine referenced defining name while "
+               & "processing the main " & To_Ada (Main_Name) & " (got null "
+               & "defining name)");
+         end if;
+
+      exception
+         when Exc : Property_Error =>
+            Report
+              (Kind => Warning,
+               Msg  => "Failed to determine referenced defining name while "
+               & "processing the main " & To_Ada (Main_Name) & ": "
+               & Ada.Exceptions.Exception_Information (Exc));
+      end;
+      if not DF.Is_Null then
+         return DF;
+      else
+         return No_Defining_Name;
+      end if;
+   end Referenced_Defining_Name;
+
+   -----------------------------
+   -- Index_In_Rewriting_Tree --
+   -----------------------------
+
+   function Index_In_Rewriting_Tree (N : Ada_Node'Class) return Positive is
+      RH : constant Node_Rewriting_Handle := Handle (N);
+      P  : constant Node_Rewriting_Handle := Parent (RH);
+   begin
+      pragma Assert (P /= No_Node_Rewriting_Handle);
+      for I in 1 .. Children_Count (P) loop
+         if Child (P, I) = RH then
+            return I;
+         end if;
+      end loop;
+
+      --  If we reach this point, this means the rewriting tree is corrupted (a
+      --  node does not belong to its parent's children).
+
+      return (raise Program_Error with "corrupted rewriting tree");
+   end Index_In_Rewriting_Tree;
+
+   ------------
+   -- Detach --
+   ------------
+
+   function Detach (N : Ada_Node'Class) return Node_Rewriting_Handle is
+   begin
+      if N.Is_Null then
+         return No_Node_Rewriting_Handle;
+      end if;
+
+      return H : constant Node_Rewriting_Handle := Handle (N) do
+         Replace (H, No_Node_Rewriting_Handle);
+      end return;
+   end Detach;
+
    ---------------------------
    -- Add_Auto_Dump_Buffers --
    ---------------------------
@@ -696,8 +801,24 @@ package body Instrument.Sources is
                Arguments => (1 => To_Nodes (RH, Helper_Unit)),
                Rule      => With_Clause_Rule);
 
+         With_RTS_Clause : constant Node_Rewriting_Handle :=
+            Create_From_Template
+               (RH,
+                Template  => "with GNATcov_RTS;",
+                Arguments => (1 .. 0 => No_Node_Rewriting_Handle),
+                Rule      => With_Clause_Rule);
+
+         Runtime_Version_Check_Node : constant Node_Rewriting_Handle :=
+            Create_From_Template
+               (RH,
+                Template  => To_Wide_Wide_String (Runtime_Version_Check),
+                Arguments => (1 .. 0 => No_Node_Rewriting_Handle),
+                Rule      => Pragma_Rule);
+
       begin
          Append_Child (Prelude, With_Clause);
+         Append_Child (Prelude, With_RTS_Clause);
+         Append_Child (Prelude, Runtime_Version_Check_Node);
       end;
 
       --  Wrap the previous subprogram body content (declarations, handled
@@ -711,6 +832,51 @@ package body Instrument.Sources is
          Nested_Block : Node_Rewriting_Handle;
          Nested_Decls : Node_Rewriting_Handle;
 
+         Main_Name  : constant LAL.Defining_Name :=
+           Subp_Body.F_Subp_Spec.F_Subp_Name;
+         Block_Name : constant Node_Rewriting_Handle :=
+           Create_Identifier (RH, "GNATcov_Original_Main");
+
+         function Replace_FQNs
+           (Node : LAL.Ada_Node'Class) return Visit_Status;
+         --  Callback for Libadalang's Traverse. If Node is a dotted name whose
+         --  prefix refers to Main, rewrite the prefix to refer to the named
+         --  block we create here.
+
+         -----------------
+         -- Replace_FQN --
+         -----------------
+
+         function Replace_FQNs
+           (Node : LAL.Ada_Node'Class) return Visit_Status
+         is
+            Name : Dotted_Name;
+         begin
+            if Node.Kind /= Ada_Dotted_Name then
+               return Into;
+            end if;
+            Name := Node.As_Dotted_Name;
+            if Referenced_Defining_Name (Main, Name.F_Prefix) = Main_Name then
+               declare
+                  Old_Prefix : constant Node_Rewriting_Handle :=
+                    Handle (Name.F_Prefix);
+                  New_Node   : constant Node_Rewriting_Handle :=
+                    Create_Regular_Node
+                      (RH,
+                       Ada_Dotted_Name,
+                       (No_Node_Rewriting_Handle,
+                        Clone (Block_Name)));
+               begin
+                  Replace (Old_Prefix, New_Node);
+                  Set_Child (Handle => New_Node,
+                             Index  => 1,
+                             Child  => Old_Prefix);
+                  return Over;
+               end;
+            end if;
+            return Into;
+         end Replace_FQNs;
+
       begin
          --  Extract the original statements (Old_Stmts) and replace it in the
          --  subprogram body with the new statements.
@@ -721,10 +887,10 @@ package body Instrument.Sources is
          Replace (Old_Stmts, New_Stmts);
 
          --  If the original subprogram has declarations or exception handlers,
-         --  wrap the original statements in a declare block to hold them.
+         --  wrap the original statements in a named block to hold them.
 
          if Subp_Body.F_Decls.F_Decls.Children_Count = 0
-            and then Subp_Body.F_Stmts.F_Exceptions.Children_Count = 0
+           and then Subp_Body.F_Stmts.F_Exceptions.Children_Count = 0
          then
             Nested_Block := Old_Stmts;
          else
@@ -735,20 +901,32 @@ package body Instrument.Sources is
                  (RH, Ada_Declarative_Part,
                   (1 => Create_Node (RH, Ada_Ada_Node_List))));
 
-            Nested_Block := Create_Regular_Node
-              (RH, Ada_Decl_Block,
-               (Nested_Decls, --  F_Decls
-                Old_Stmts,    --  F_Stmts
-                No_Node));    --  F_End_Name
-         end if;
+            Nested_Block := Create_Named_Stmt
+              (RH,
+               Named_Stmt_F_Decl => Create_Named_Stmt_Decl
+                 (RH,
+                  Create_Defining_Name
+                    (RH, Clone (Block_Name)),
+                  No_Node),
+               Named_Stmt_F_Stmt => Create_Regular_Node
+                 (RH, Ada_Decl_Block,
+                  (Nested_Decls,
+                   Old_Stmts,
+                   Clone (Block_Name))));
+
+            --  Change the Qualified names in the Main's declarations and
+            --  statements to be compatible ith the new nested block.
+            Subp_Body.F_Stmts.Traverse (Replace_FQNs'Access);
+            Subp_Body.F_Decls.Traverse (Replace_FQNs'Access);
 
+         end if;
          Append_Child (New_Stmt_List, Nested_Block);
       end;
 
       --  Depending on the chosen coverage buffers dump trigger, insert the
       --  appropriate code.
 
-      case Auto_Dump_Trigger (IC.Dump_Trigger) is
+      case Auto_Dump_Trigger (IC.Dump_Config.Trigger) is
 
       when At_Exit | Ravenscar_Task_Termination =>
 
@@ -1060,7 +1238,7 @@ package body Instrument.Sources is
 
       --  Insert automatic buffer dump calls, if requested
 
-      if IC.Dump_Trigger /= Manual and then Unit_Info.Is_Main then
+      if IC.Dump_Config.Trigger /= Manual and then Unit_Info.Is_Main then
          Add_Auto_Dump_Buffers
            (IC   => IC,
             Info => Prj_Info,
diff --git a/tools/gnatcov/instrument-sources.ads b/tools/gnatcov/instrument-sources.ads
index 862137788..213a7d4f7 100644
--- a/tools/gnatcov/instrument-sources.ads
+++ b/tools/gnatcov/instrument-sources.ads
@@ -2,7 +2,7 @@
 --                                                                          --
 --                               GNATcoverage                               --
 --                                                                          --
---                     Copyright (C) 2008-2019, AdaCore                     --
+--                     Copyright (C) 2008-2020, AdaCore                     --
 --                                                                          --
 -- GNATcoverage is free software; you can redistribute it and/or modify it  --
 -- under terms of the GNU General Public License as published by the  Free  --
@@ -26,10 +26,12 @@ with Ada.Strings.Wide_Wide_Hash;
 
 with Langkit_Support.Text; use Langkit_Support.Text;
 with Libadalang.Analysis;  use Libadalang.Analysis;
+with Libadalang.Common;     use Libadalang.Common;
 with Libadalang.Rewriting; use Libadalang.Rewriting;
 
-with SC_Obligations;    use SC_Obligations;
+with GNATcov_RTS;
 with Instrument.Common; use Instrument.Common;
+with SC_Obligations;    use SC_Obligations;
 with Strings;
 with Types;             use Types;
 
@@ -55,7 +57,6 @@ private package Instrument.Sources is
       MCDC_Buffer : Node_Rewriting_Handle := No_Node_Rewriting_Handle;
       --  Qualified name for the buffer corresponding to paths in decision
       --  BDDs.
-
    end record;
 
    -----------------------------
@@ -156,31 +157,56 @@ private package Instrument.Sources is
    type Insertion_Info;
    type Insertion_Info_Access is access all Insertion_Info;
 
-   type Insertion_Info is record
-      Witness_Use_Statement : Boolean := False;
-      --  Set False when traversing a list of declarations,
-      --  True when traversing a list of statements.
+   type Insertion_Method is
+     (None, Statement, Declaration, Expression_Function);
+   --  Describe how to insert a call to a witness subprogram:
+   --
+   --  * None: no insertion method yet.
+   --
+   --  * Statement: insert a witness call statement.
+   --
+   --  * Declaration: insert a dummy declaration whose initialization
+   --    expression is a witness call.
+   --
+   --  * Expression_Function: wrap the expression in an expression function
+   --    in a case expression whose controlling expr is a witness call.
+
+   type Insertion_Info (Method : Insertion_Method := None) is record
+
+      case Method is
+         when Statement | Declaration =>
+            RH_List : Node_Rewriting_Handle := No_Node_Rewriting_Handle;
+            --  Rewriting handle for the statement/declaration list
 
-      Preelab : Boolean := False;
-      --  Whether we are traversing a list of top-level declarations in a
-      --  preelaborate package. In this context, we cannot insert witness
-      --  calls, precisely because of the preelaborate restriction.
+            Index : Natural := 0;
+            --  Index of the element in RH_List being traversed
 
-      RH_List : Node_Rewriting_Handle := No_Node_Rewriting_Handle;
-      --  If traversing a list, rewriting handle for the list
+            Rewriting_Offset : Integer := 0;
+            --  Count of nodes inserted/removed in current list so far
 
-      RH_Private_List : Node_Rewriting_Handle := No_Node_Rewriting_Handle;
-      --  If RH_List is the declarations of a public part, and there is
-      --  a corresponding private part, declarations list of the private part.
+            Preelab : Boolean := False;
+            --  Whether we are traversing a list of top-level declarations in a
+            --  preelaborate package. In this context, we cannot insert witness
+            --  calls, precisely because of the preelaborate restriction.
 
-      Index : Natural := 0;
-      --  Index of the element in RH_List being traversed
+            Parent : Insertion_Info_Access;
+            --  Insertion_Info for the upper enclosing list
 
-      Rewriting_Offset : Integer := 0;
-      --  Count of nodes inserted/removed in current list so far
+            case Method is
+               when Declaration =>
+                  RH_Private_List : Node_Rewriting_Handle :=
+                     No_Node_Rewriting_Handle;
+                  --  If RH_List is the declarations of a public part, and
+                  --  there is a corresponding private part, declarations
+                  --  list of the private part.
 
-      Parent : Insertion_Info_Access;
-      --  Insertion_Info for the upper enclosing list
+               when others =>
+                  null;
+            end case;
+
+         when others =>
+            null;
+      end case;
    end record;
 
    type Root_MCDC_State_Inserter is abstract tagged null record;
@@ -284,7 +310,7 @@ private package Instrument.Sources is
       Info : in out Project_Info;
       Main : Ada_Qualified_Name;
       URH  : Unit_Rewriting_Handle)
-      with Pre => IC.Dump_Trigger /= Manual;
+      with Pre => IC.Dump_Config.Trigger /= Manual;
    --  Try to insert in the sources of Main (a main subprogram) a call to dump
    --  the list of coverage buffers for all units of interest in Main's
    --  closure. Return without doing anything if unsuccessful.
@@ -292,6 +318,15 @@ private package Instrument.Sources is
    --  Info must be the project that owns the Main unit, and URH must be a
    --  rewriting handle for the body unit that contains Main's sources.
 
+   Runtime_Version_Check : constant String :=
+     "pragma Compile_Time_Error (GNATcov_RTS.Version /="
+     & GNATcov_RTS.Version'Image
+     & ",""Incompatible GNATcov_RTS version, please use"
+     & " the GNATcov_RTS project provided with your"
+     & " GNATcoverage distribution."");";
+   --  Check to be inserted in instrumented units to verify that they are
+   --  built with the version of GNATcov_RTS the instrumenter expects.
+
    function Img (Bit : Any_Bit_Id) return String is
      (Strings.Img (Integer (Bit)));
 
@@ -300,4 +335,44 @@ private package Instrument.Sources is
    --  Unit, which must be specified in the normalized form expected for
    --  FQN_Sets (lower case, period separated, fully qualified).
 
+   function Index_In_Rewriting_Tree (N : Ada_Node'Class) return Positive;
+   --  Assuming that the rewriting node for N has a parent, return its index in
+   --  that parent's list of children.
+
+   ---------------------------------
+   -- Helpers to synthetize nodes --
+   ---------------------------------
+
+   function Clone (N : Ada_Node'Class) return Node_Rewriting_Handle is
+     (if N.Is_Null then No_Node_Rewriting_Handle else Clone (Handle (N)));
+   --  Simple wrapper around Libadalang's Clone, except that it works on parse
+   --  nodes, and accepts null nodes.
+
+   function Detach (N : Ada_Node'Class) return Node_Rewriting_Handle;
+   --  Replace N with No_Node_Rewriting_Handle, and return its previous
+   --  handle for possible reuse elsewhere in the tree.
+
+   No_Children : constant Node_Rewriting_Handle_Array :=
+     (1 .. 0 => No_Node_Rewriting_Handle);
+
+   function Make
+     (UIC : Unit_Inst_Context;
+      K   : Ada_Node_Kind_Type) return Node_Rewriting_Handle
+   is (Create_Node (UIC.Rewriting_Context, K));
+   --  Shortcut to create a node of the given kind
+
+   function Make_Identifier
+     (UIC : Unit_Inst_Context;
+      Id  : Wide_Wide_String) return Node_Rewriting_Handle
+   is (Create_Token_Node
+         (UIC.Rewriting_Context, Libadalang.Common.Ada_Identifier, Id));
+   --  Shortcut to create an identifier node
+
+   function Make_Defining_Name
+     (UIC    : Unit_Inst_Context;
+      D_Name : Wide_Wide_String) return Node_Rewriting_Handle
+   is (Create_Defining_Name (UIC.Rewriting_Context,
+                             Make_Identifier (UIC, D_Name)));
+   --  Shortcut to create a defining identifier tree
+
 end Instrument.Sources;
diff --git a/tools/gnatcov/instrument-tree.adb b/tools/gnatcov/instrument-tree.adb
index b57f9e2b2..8fa28e280 100644
--- a/tools/gnatcov/instrument-tree.adb
+++ b/tools/gnatcov/instrument-tree.adb
@@ -2,7 +2,7 @@
 --                                                                          --
 --                               GNATcoverage                               --
 --                                                                          --
---                     Copyright (C) 2008-2020, AdaCore                     --
+--                     Copyright (C) 2008-2021, AdaCore                     --
 --                                                                          --
 -- GNATcoverage is free software; you can redistribute it and/or modify it  --
 -- under terms of the GNU General Public License as published by the  Free  --
@@ -16,11 +16,12 @@
 -- of the license.                                                          --
 ------------------------------------------------------------------------------
 
-with Ada.Wide_Wide_Characters.Handling; use Ada.Wide_Wide_Characters.Handling;
 with Ada.Characters.Conversions;        use Ada.Characters.Conversions;
+with Ada.Exceptions;
 with Ada.Strings.Unbounded;             use Ada.Strings.Unbounded;
 with Ada.Strings.Wide_Wide_Fixed;
 with Ada.Strings.Wide_Wide_Unbounded;   use Ada.Strings.Wide_Wide_Unbounded;
+with Ada.Wide_Wide_Characters.Handling; use Ada.Wide_Wide_Characters.Handling;
 
 with GNATCOLL.Projects; use GNATCOLL.Projects;
 
@@ -143,14 +144,10 @@ package body Instrument.Tree is
 
    I_Accept_Stmt_With_Stmts_F_Stmts : constant Integer :=
      Index (Ada_Accept_Stmt_With_Stmts, Accept_Stmt_With_Stmts_F_Stmts);
-   I_Defining_Name_F_Name : constant Integer :=
-     Index (Ada_Defining_Name, Defining_Name_F_Name);
    I_Handled_Stmts_F_Stmts : constant Integer :=
      Index (Ada_Handled_Stmts, Handled_Stmts_F_Stmts);
    I_Subp_Spec_F_Subp_Params : constant Integer :=
      Index (Ada_Subp_Spec, Subp_Spec_F_Subp_Params);
-   I_Params_F_Params : constant Integer :=
-     Index (Ada_Params, Params_F_Params);
 
    -------------------------------------
    -- Generation of witness fragments --
@@ -182,6 +179,297 @@ package body Instrument.Tree is
       UIC      : in out Unit_Inst_Context;
       Name     : String) return String;
 
+   ------------------------------------------------
+   -- Degenerate subprograms                     --
+   -- (null procedures and expression functions) --
+   ------------------------------------------------
+   --  Degenerate subprograms require special handling because we need a place
+   --  to insert witness calls for statement coverage, and in the case of
+   --  expression functions, a place to declare temporary local variables for
+   --  the MC/DC state buffer for any decision in the expression.
+   --
+   --  We provide these locations by generating a generic subprogram in the
+   --  pure buffers unit, and replacing the degenerate subprogram with an
+   --  instantiation of that generic subprogram. The statement witness and
+   --  MC/DC state variable declarations are inserted in the generic body.
+   --
+   --  For expression functions, we then create a new, augmented expression
+   --  function that takes the addresses of the MC/DC states as additional
+   --  formal parameters, and we pass this new function as a generic parameter
+   --  in the instantiation.
+   --
+   --  Also note that we wrap both the augmented expression function and the
+   --  generic instantiation in a nested package, so that they do not introduce
+   --  unwanted additional primitive operations. We use a renaming-as-body of
+   --  the instantiation to associate it with the original subprogram name,
+   --  while preserving all aspects and default parameters.
+   --
+   --  The following examples both provide a compact summary of the
+   --  transformations, and associate names (used in the implementation) to the
+   --  various constructs involved.
+   --
+   --  Null subprogram example
+   --  =======================
+   --
+   --  For the following null procedure:
+   --
+   --     --  See Degenerate_Subp_Common_Nodes.N
+   --     procedure Foo
+   --       (Arg1 : Arg1_Type;
+   --        Arg2 : in out Arg2_Type) is null;
+   --
+   --  We generate the following declaration in the pure buffer unit:
+   --
+   --     --  See Null_Proc_Nodes.Subp_Decl
+   --     generic
+   --        --  See Null_Proc_Nodes.Formals
+   --        type Par1 (<>) is limited private;
+   --        type Par2 (<>) is limited private;
+   --     procedure Null_Proc_[Subprogram_Index](S|B|U)_Gen
+   --       --  See Null_Proc_Nodes.Subp_Spec and .Param_Specs
+   --       (Arg1 : Par2;
+   --        Arg2 : in out Par2);
+   --
+   --  the following body (also in the pure buffer unit):
+   --
+   --     --  See Complete_Null_Proc_Decls.Subp_Body
+   --     procedure Null_Proc_[Subprogram_Index](S|B|U)_Gen
+   --       (Arg1 : Par2;
+   --        Arg2 : in out Par2) is
+   --     begin
+   --        --  See Null_Proc_Nodes.Stmt_List
+   --        [Witness call];
+   --        null;  --  See Null_Proc_Nodes.Null_Stmt
+   --     end;
+   --
+   --  and finally the following (in the instrumented unit, replacing the
+   --  original declaration):
+   --
+   --     procedure Foo
+   --       (Arg1 : Arg1_Type;
+   --        Arg2 : in out Arg2_Type);
+   --
+   --     --  See Degenerate_Subp_Common_Nodes.Wrapper_Pkg
+   --     package Null_Proc_[Subprogram_Index](S|B|U) is
+   --        --  See Complete_Null_Proc_Decls.Instance
+   --        procedure Foo is new
+   --          [Pure_Unit].Null_Proc_[Subprogram_Index](S|B|U)
+   --            --  See Null_Proc_NOdes.Inst_Params
+   --            (Arg1_Type, Arg2_Type);
+   --     end Null_Proc_[Subprogram_Index](S|B|U);
+   --
+   --     --  See Complete_Null_Proc_Decls.Renaming_Decl
+   --     procedure Foo
+   --       (Arg1 : Arg1_Type;
+   --        Arg2 : in out Arg2_Type)
+   --     renames Null_Proc_[Subprogram_Index](S|B|U).Foo;
+   --
+   --  Expression function example (MC/DC)
+   --  ===================================
+   --
+   --  For the following expression function:
+   --
+   --     --  See Degenerate_Subp_Common_Nodes.N
+   --     function Foo (Arg1 : Arg1_Type; Arg2 : Arg2_Type) return Boolean
+   --     is (Arg1.X and then Arg2.Y);
+   --
+   --  We generate the following declarations in the instrumented unit,
+   --  replacing the original declaration:
+   --
+   --     --  Sometimes we don't emit this forward declaration (see
+   --     --  Traverse_Degenerate_Subprogram).
+   --     function Foo (Arg1 : Arg1_Type; Arg2 : Arg2_Type) return Boolean;
+   --
+   --     --  See Degenerate_Subp_Common_Nodes.Wrapper_Pkg
+   --     package Func_Expr_[Subprogram_Index](S|B|U) is
+   --        --  See Create_Augmented_Expr_Function.Augmented_Expr_Function
+   --        function Foo_With_State
+   --          (Arg1         : Arg1_Type;
+   --           Arg2         : Arg2_Type;
+   --           MCDC_State_2 : GNATcov_RTS.Buffers.MCDC_State_Holder)
+   --           return Boolean
+   --        is (case [Witness call] is
+   --            when others =>
+   --            [decision with Witness calls using MCDC_State_2]);
+   --     end Func_Expr_[Subprogram_Index](S|B|U);
+   --
+   --     --  See Create_Augmented_Expr_Function.New_Expr_Function
+   --     function Foo (Arg1 : Arg1_Type; Arg2 : Arg2_Type) return Boolean
+   --     is (Func_Expr_[Subprogram_Index](S|B|U).Foo_With_State
+   --           (Arg1,
+   --            Arg2,
+   --            GNATcov_RTS.Buffers.MCDC_State_Holder'(others => <>)));
+   --
+   --  Without MC/DC, we just insert the case expression+Witness call inside
+   --  the expression function.
+
+   --  The following record tracks several parse and rewriting nodes that are
+   --  useful for both the instrumentation of null subprograms and expression
+   --  functions (see Traverse_Degenerate_Subprogram).
+
+   type Degenerate_Subp_Common_Nodes is record
+      N : Basic_Decl;
+      --  Parse node for the subprogram to instrument
+
+      N_Spec : Subp_Spec;
+      --  Shortcut for its subprogram specification
+
+      N_Overriding : Overriding_Node;
+      --  Shortcut for the subprogram "overriding" node (if any)
+
+      N_Name : Libadalang.Analysis.Name;
+      --  Shortcut for its name
+
+      N_Params : Param_Spec_List;
+      --  List of arguments for the subprogram, or No_Param_Spec_List if there
+      --  is no argument list.
+
+      Ctrl_Type : Base_Type_Decl;
+      --  If the subprogram is a primitive of a tagged type, Ctrl_Type is the
+      --  tagged type (No_Base_Type_Decl otherwise).
+
+      Append_List : Node_Rewriting_Handle;
+      --  Declaration list for the current context. Note that this is always
+      --  "private" one if this is a package that has a private part.
+
+      --  The augmented expression function, taking supplementary parameters
+      --  for state buffers, and the generic instantiation, must be wrapped in
+      --  a package so that they do not create additional primitive operations
+      --  for argument/return types. The following Wrapper_Pkg* components
+      --  implement this package.
+
+      Wrapper_Pkg_Name : Node_Rewriting_Handle;
+      --  Name for this wrapper package
+
+      Wrapper_Pkg_Decls : Node_Rewriting_Handle;
+      --  List of public declarations for this wrapper package
+
+      Wrapper_Pkg : Node_Rewriting_Handle;
+      --  Declaration for this wrapper package
+   end record;
+
+   function Create_Degenerate_Subp_Common_Nodes
+     (UIC              : Unit_Inst_Context;
+      N                : Basic_Decl;
+      N_Spec           : Subp_Spec;
+      Gen_Names_Prefix : Wide_Wide_String) return Degenerate_Subp_Common_Nodes;
+   --  Create all the required nodes in Degenerate_Subp_Common_Nodes from the
+   --  given arguments.
+
+   --  The expression function MC/DC state inserter inserts MC/DC state buffers
+   --  as variable declarations in the generic body, and ensures that
+   --  references to these variables are passed to the instrumented expression
+   --  function.
+
+   --  Holder for the various nodes used in the instrumentation of null
+   --  procedures. They all relate to the generic procedure we generate in pure
+   --  buffer units.
+
+   type Null_Proc_Nodes is record
+      Name : Node_Rewriting_Handle;
+      --  Name of the generic procedure (raw identifier node, not the defining
+      --  identifier tree).
+
+      Formals : Node_Rewriting_Handle;
+      --  List of formals for the generic procedure (i.e. what comes next
+      --  right after the "generic" keyword).
+
+      Param_Specs : Node_Rewriting_Handle;
+      --  List of parameters for the generic procedure (null if the original
+      --  procedure takes no argument).
+
+      Null_Stmt : Node_Rewriting_Handle;
+      --  "null" statement in the generic procedure body. We create this
+      --  statement so that statement handling machinery inserts a witness call
+      --  next to it later on.
+
+      Stmt_List : Node_Rewriting_Handle;
+      --  List of statements for the generic procedure body. Only contains the
+      --  "null" statement intially, then is completed to also contain the
+      --  witness call later.
+
+      Subp_Spec : Node_Rewriting_Handle;
+      --  Spec for the generic procedure. Note that although this rewriting
+      --  node is used in the generic procedure declaration, it is cloned in
+      --  order to generate the corresponding body.
+
+      Subp_Decl : Node_Rewriting_Handle;
+      --  Declaration for the generic procedure
+
+      Inst_Params : Node_Rewriting_Handle;
+      --  List of parameters for the generic procedure instantiation
+   end record;
+
+   procedure Create_Null_Proc_Nodes
+     (Nodes            : out Null_Proc_Nodes;
+      UIC              : Unit_Inst_Context;
+      N_Spec           : Subp_Spec;
+      Gen_Names_Prefix : Wide_Wide_String);
+   --  Fill in Nodes to instrument a null procedure. N_Spec is its
+   --  subprogram spec.
+   --
+   --  Gen_Names_Prefix is used to generate the name of the generic procedure.
+
+   procedure Collect_Null_Proc_Formals
+     (Common_Nodes : Degenerate_Subp_Common_Nodes;
+      NP_Nodes     : Null_Proc_Nodes;
+      UIC          : Unit_Inst_Context);
+   --  Go through all arguments in Common_Nodes.N_Spec and create:
+   --
+   --  * the corresponding formal types in NP_Nodes.Formal;
+   --  * the corresponding arguments in NP_Nodes.Param_Specs;
+   --  * the corresponding instantiation arguments in NP_Nodes.Inst_Params.
+
+   procedure Complete_Null_Proc_Decls
+     (UIC           : Unit_Inst_Context;
+      Common_Nodes  : Degenerate_Subp_Common_Nodes;
+      NP_Nodes      : Null_Proc_Nodes;
+      Subp_Body     : out Node_Rewriting_Handle;
+      Instance      : out Node_Rewriting_Handle;
+      Renaming_Decl : out Node_Rewriting_Handle);
+   --  Create the body for the generic subprogram (Subp_Body), its
+   --  instantiation declaration (Instance) and the renaming for this instance
+   --  (Renaming_Decl).
+
+   type Expr_Func_MCDC_State_Inserter is new Root_MCDC_State_Inserter with
+      record
+         N_Spec : Subp_Spec;
+         --  Subprogram spec for the original expression function
+
+         Call_Params : Node_Rewriting_Handle;
+         --  Assoc_List node for the call to the augmented expression function
+
+         Formal_Params : Node_Rewriting_Handle;
+         --  Formal parameter list where new parameters are added to hold MC/DC
+         --  temporary buffers. This is set lazily from N_Spec. This can
+         --  therefore be tested for No_Node_Rewriting_Handle to determine if
+         --  any parameter was inserted.
+      end record;
+
+   overriding function Insert_MCDC_State
+     (Inserter : in out Expr_Func_MCDC_State_Inserter;
+      UIC      : in out Unit_Inst_Context;
+      Name     : String) return String;
+
+   procedure Create_Augmented_Expr_Function
+     (UIC                     : Unit_Inst_Context;
+      Common_Nodes            : Degenerate_Subp_Common_Nodes;
+      Formal_Params           : Node_Rewriting_Handle;
+      Call_Params             : Node_Rewriting_Handle;
+      Augmented_Expr_Function : out Node_Rewriting_Handle;
+      New_Expr_Function       : out Node_Rewriting_Handle);
+   --  Create the augmented expression function from the original one
+   --  (Augmented_Expr_Function) and create the expression function
+   --  (New_Expr_Function) that will serve as a replacement to the original
+   --  one.
+
+   function Is_Self_Referencing
+     (UIC : Unit_Inst_Context;
+      EF  : Expr_Function) return Boolean;
+   --  Return if EF is a self-referencing expression function, i.e. if its
+   --  expression has a reference to itself (for instance: it's a recursive
+   --  function).
+
    ------------
    -- Report --
    ------------
@@ -282,6 +570,712 @@ package body Instrument.Tree is
       return Name;
    end Insert_MCDC_State;
 
+   -----------------------------------------
+   -- Create_Degenerate_Subp_Common_Nodes --
+   -----------------------------------------
+
+   function Create_Degenerate_Subp_Common_Nodes
+     (UIC              : Unit_Inst_Context;
+      N                : Basic_Decl;
+      N_Spec           : Subp_Spec;
+      Gen_Names_Prefix : Wide_Wide_String) return Degenerate_Subp_Common_Nodes
+   is
+      RC          : Rewriting_Handle renames UIC.Rewriting_Context;
+      Insert_Info : Insertion_Info renames UIC.Current_Insertion_Info.all;
+   begin
+      return Result : Degenerate_Subp_Common_Nodes do
+         Result.N := N;
+         Result.N_Spec := N_Spec;
+         Result.N_Overriding := N.As_Base_Subp_Body.F_Overriding;
+         Result.N_Name := N_Spec.F_Subp_Name.F_Name;
+         Result.N_Params :=
+           (if N_Spec.F_Subp_Params.Is_Null
+            then No_Param_Spec_List
+            else N_Spec.F_Subp_Params.F_Params);
+         Result.Ctrl_Type := N_Spec.P_Primitive_Subp_Tagged_Type;
+
+         Result.Append_List :=
+           (if Insert_Info.RH_Private_List /= No_Node_Rewriting_Handle
+            then Insert_Info.RH_Private_List
+            else Insert_Info.RH_List);
+
+         Result.Wrapper_Pkg_Name :=
+           Make_Identifier (UIC, Gen_Names_Prefix & "Pkg");
+
+         Result.Wrapper_Pkg_Decls :=
+           Create_Regular_Node (RC, Ada_Ada_Node_List, No_Children);
+
+         Result.Wrapper_Pkg :=
+           Create_Package_Decl
+             (RC,
+              Base_Package_Decl_F_Package_Name => Result.Wrapper_Pkg_Name,
+              Base_Package_Decl_F_Aspects      =>
+                No_Node_Rewriting_Handle,
+              Base_Package_Decl_F_Public_Part  =>
+                Create_Public_Part
+                  (RC,
+                   Declarative_Part_F_Decls => Result.Wrapper_Pkg_Decls),
+              Base_Package_Decl_F_Private_Part =>
+                No_Node_Rewriting_Handle,
+              Base_Package_Decl_F_End_Name     =>
+                No_Node_Rewriting_Handle);
+      end return;
+   end Create_Degenerate_Subp_Common_Nodes;
+
+   ----------------------------
+   -- Create_Null_Proc_Nodes --
+   ----------------------------
+
+   procedure Create_Null_Proc_Nodes
+     (Nodes            : out Null_Proc_Nodes;
+      UIC              : Unit_Inst_Context;
+      N_Spec           : Subp_Spec;
+      Gen_Names_Prefix : Wide_Wide_String)
+   is
+      RC : Rewriting_Handle renames UIC.Rewriting_Context;
+
+      No_Param : constant Boolean := N_Spec.F_Subp_Params.Is_Null;
+   begin
+      Nodes.Name := Make_Identifier (UIC, Gen_Names_Prefix & "Gen");
+
+      Nodes.Formals := Make (UIC, Ada_Ada_Node_List);
+
+      Nodes.Param_Specs :=
+        (if No_Param
+         then No_Node_Rewriting_Handle
+         else Make (UIC, Ada_Param_Spec_List));
+
+      Nodes.Null_Stmt := Make (UIC, Ada_Null_Stmt);
+
+      Nodes.Stmt_List :=
+         Create_Regular_Node (RC, Ada_Stmt_List, (1 => Nodes.Null_Stmt));
+
+      Nodes.Subp_Spec :=
+         Create_Subp_Spec
+           (RC,
+            Subp_Spec_F_Subp_Kind => Make (UIC, Ada_Subp_Kind_Procedure),
+            Subp_Spec_F_Subp_Name => Create_Defining_Name (RC, Nodes.Name),
+
+            Subp_Spec_F_Subp_Params =>
+              (if No_Param
+               then No_Node_Rewriting_Handle
+               else Create_Params (RC, Params_F_Params => Nodes.Param_Specs)),
+
+            Subp_Spec_F_Subp_Returns => No_Node_Rewriting_Handle);
+
+      Nodes.Subp_Decl :=
+         Create_Generic_Subp_Decl
+           (RC,
+            Generic_Decl_F_Formal_Part =>
+               Create_Generic_Formal_Part
+                 (RC, Generic_Formal_Part_F_Decls => Nodes.Formals),
+
+            Generic_Subp_Decl_F_Subp_Decl =>
+               Create_Generic_Subp_Internal
+                 (RC,
+                  Generic_Subp_Internal_F_Subp_Spec => Nodes.Subp_Spec,
+                  Generic_Subp_Internal_F_Aspects   =>
+                     No_Node_Rewriting_Handle),
+
+            Generic_Subp_Decl_F_Aspects => No_Node_Rewriting_Handle);
+
+      Nodes.Inst_Params := Make (UIC, Ada_Assoc_List);
+   end Create_Null_Proc_Nodes;
+
+   -------------------------------
+   -- Collect_Null_Proc_Formals --
+   -------------------------------
+
+   procedure Collect_Null_Proc_Formals
+     (Common_Nodes : Degenerate_Subp_Common_Nodes;
+      NP_Nodes     : Null_Proc_Nodes;
+      UIC          : Unit_Inst_Context)
+   is
+      RC : Rewriting_Handle renames UIC.Rewriting_Context;
+
+      function Gen_Type_Expr (TE : Type_Expr) return Node_Rewriting_Handle;
+      --  Return the type expression to use in the generic procedure spec for a
+      --  parameter of the given type.
+
+      function Gen_Proc_Param_For
+        (Spec : Param_Spec) return Node_Rewriting_Handle
+      is (Create_Param_Spec
+            (RC,
+             Param_Spec_F_Ids          => Clone (Spec.F_Ids),
+             Param_Spec_F_Has_Aliased  => Clone (Spec.F_Has_Aliased),
+             Param_Spec_F_Mode         => Clone (Spec.F_Mode),
+             Param_Spec_F_Type_Expr    => Gen_Type_Expr (Spec.F_Type_Expr),
+             Param_Spec_F_Default_Expr => No_Node_Rewriting_Handle,
+             Param_Spec_F_Aspects      => No_Node_Rewriting_Handle));
+      --  Create and return the param spec to be used in the generic procedure
+      --  parameters for Spec (a parameter spec for the null procedure to
+      --  instrument).
+
+      function Gen_Type_Expr_For_Simple_Access_Type
+        (Access_Def : Type_Access_Def) return Node_Rewriting_Handle;
+      --  Helper for Gen_Type_Expr, specifically for simple access types. For
+      --  instance, given:
+      --     access Integer
+      --  This will return:
+      --     access ParN
+      --  See Make_Formal_Type for the meaning of ParN.
+
+      function Gen_Type_Expr_For_Access_To_Subp
+        (Access_Def : Access_To_Subp_Def) return Node_Rewriting_Handle;
+      --  Helper for Gen_Type_Expr, specifically for access to subprogram
+      --  types. For instance, given:
+      --     access function (S : String) return Natural
+      --  This will return:
+      --     access function (S : ParN) return ParM
+      --  See Make_Formal_Type for the meaning of Par*.
+
+      Next_Formal_Index : Positive := 1;
+      --  Unique index for each generic procedure formal type we generate (thus
+      --  increased each time we add a formal type). Index unicity allows us to
+      --  generate unique formal type names. This is used exclusively in
+      --  Make_Formal_Type.
+
+      function Make_Formal_Type
+        (TE : Type_Expr'Class) return Node_Rewriting_Handle;
+      --  Create a formal type for the given type expression and return a
+      --  reference to it. This function takes care of adding the formal type
+      --  declaration to NP_Nodes.Formals and the actual type (TE) to
+      --  NP_Nodes.Inst_Params.
+      --
+      --  For instance, given:
+      --     Integer
+      --  This inserts the following to NP_Nodes.Formals:
+      --     type ParN (<>) is limited private;
+      --  plus the following to NP_Nodes.Param_Specs:
+      --     Integer
+      --  and finally returns:
+      --     ParN
+
+      function Make_Anonymous_Type_Decl
+        (Type_Def : Node_Rewriting_Handle) return Node_Rewriting_Handle
+      is (Create_Anonymous_Type_Decl
+            (RC,
+             Base_Type_Decl_F_Name     => No_Node_Rewriting_Handle,
+             Type_Decl_F_Discriminants => No_Node_Rewriting_Handle,
+             Type_Decl_F_Type_Def      => Type_Def,
+             Type_Decl_F_Aspects       => No_Node_Rewriting_Handle));
+      --  Shortcut for Gen_Type_Expr_For_* subprograms. Create and return an
+      --  anonymous type declaration for the given type definition.
+
+      -------------------
+      -- Gen_Type_Expr --
+      -------------------
+
+      function Gen_Type_Expr (TE : Type_Expr) return Node_Rewriting_Handle is
+      begin
+         --  Compute the type for the returned param spec. In the case of
+         --  anonymous access types, we must deconstruct type accessed type.
+         --  For instance, we must turn the following type expression:
+         --
+         --     not null access procedure (Line : in out String := "")
+         --
+         --  into the following:
+         --
+         --     not null access function
+         --       (Line : in out [formalX])
+         --        return [formalY];
+
+         if TE.Kind = Ada_Anonymous_Type then
+            declare
+               TD : constant Type_Def :=
+                 TE.As_Anonymous_Type.F_Type_Decl.F_Type_Def;
+            begin
+               --  There are two kinds of anonymous types: "simple" access
+               --  types, and access to subprogram types.
+
+               case TD.Kind is
+               when Ada_Type_Access_Def =>
+                  return Gen_Type_Expr_For_Simple_Access_Type
+                    (TD.As_Type_Access_Def);
+
+               when Ada_Access_To_Subp_Def =>
+                  return Gen_Type_Expr_For_Access_To_Subp
+                    (TD.As_Access_To_Subp_Def);
+
+               when others =>
+                  raise Program_Error with
+                    "unexpected anonymous type definition: " & TD.Kind'Image;
+               end case;
+            end;
+
+         else
+            return Make_Formal_Type (TE);
+         end if;
+      end Gen_Type_Expr;
+
+      ------------------------------------------
+      -- Gen_Type_Expr_For_Simple_Access_Type --
+      ------------------------------------------
+
+      function Gen_Type_Expr_For_Simple_Access_Type
+        (Access_Def : Type_Access_Def) return Node_Rewriting_Handle
+      is
+         Formal_Subtype_Indication : constant Subtype_Indication :=
+           Access_Def.F_Subtype_Indication;
+         --  Accessed type
+
+         --  Determine if this is a controlling access parameter, in which case
+         --  the corresponding formal in the generic subprogram must be
+         --  explicitly null excluding.
+
+         Formal_Subt_Decl : constant Base_Type_Decl :=
+           Formal_Subtype_Indication.P_Designated_Type_Decl;
+         Ctrl_Type        : Base_Type_Decl renames
+           Common_Nodes.Ctrl_Type;
+         Is_Controlling   : constant Boolean :=
+           (if Ctrl_Type.Is_Null
+            then False
+            else Formal_Subt_Decl = Ctrl_Type
+                 or else Formal_Subt_Decl = Ctrl_Type.P_Full_View);
+         Has_Not_Null : constant Node_Rewriting_Handle :=
+           (if Is_Controlling
+            then Make (UIC, Ada_Not_Null_Present)
+            else Clone (Access_Def.F_Has_Not_Null));
+      begin
+         return Make_Anonymous_Type_Decl
+           (Create_Type_Access_Def
+              (RC,
+               Access_Def_F_Has_Not_Null            => Has_Not_Null,
+               Type_Access_Def_F_Has_All            =>
+                 No_Node_Rewriting_Handle,
+               Type_Access_Def_F_Has_Constant       =>
+                 Clone (Access_Def.F_Has_Constant),
+               Type_Access_Def_F_Subtype_Indication =>
+                 Make_Formal_Type (Formal_Subtype_Indication)));
+      end Gen_Type_Expr_For_Simple_Access_Type;
+
+      --------------------------------------
+      -- Gen_Type_Expr_For_Access_To_Subp --
+      --------------------------------------
+
+      function Gen_Type_Expr_For_Access_To_Subp
+        (Access_Def : Access_To_Subp_Def) return Node_Rewriting_Handle
+      is
+         Orig_Spec : constant Subp_Spec := Access_Def.F_Subp_Spec;
+         Subp_Kind : constant Ada_Node_Kind_Type := Orig_Spec.F_Subp_Kind.Kind;
+
+         Orig_Params      : constant Param_Spec_List :=
+           (if Orig_Spec.F_Subp_Params.Is_Null
+            then No_Param_Spec_List
+            else Orig_Spec.F_Subp_Params.F_Params);
+         Param_Spec_Count : constant Natural :=
+           (if Orig_Params.Is_Null
+            then 0
+            else Orig_Params.Children_Count);
+
+         New_Params : Node_Rewriting_Handle_Array (1 .. Param_Spec_Count);
+         --  List of param spec for the returned access to subprogram type
+
+         New_Return_Type : Node_Rewriting_Handle;
+         --  Return type for the returned access to subprogram type, or
+         --  No_Node_Rewriting_Handle if this is a procedure.
+
+         New_F_Subp_Params : Node_Rewriting_Handle;
+         Subp_Spec         : Node_Rewriting_Handle;
+         --  Intermediate nodes to create the access to subprogram type
+         --  definition.
+      begin
+         --  Create param specs for the returned access to subprogram type
+
+         for J in 1 .. Param_Spec_Count loop
+            New_Params (J) := Gen_Proc_Param_For
+              (Orig_Params.Child (J).As_Param_Spec);
+         end loop;
+
+         New_F_Subp_Params :=
+           (if Param_Spec_Count > 0
+            then Create_Params
+                   (RC,
+                    Create_Regular_Node (RC, Ada_Param_Spec_List, New_Params))
+            else No_Node_Rewriting_Handle);
+
+         --  Create its return type (if it is a function)
+
+         New_Return_Type :=
+           (if Subp_Kind = Ada_Subp_Kind_Function
+            then Gen_Type_Expr (Orig_Spec.F_Subp_Returns)
+            else No_Node_Rewriting_Handle);
+
+         --  We can now create the whole subprogram spec, and then the
+         --  anonymous type.
+
+         Subp_Spec := Create_Subp_Spec
+           (RC,
+            Subp_Spec_F_Subp_Kind    => Create_Node (RC, Subp_Kind),
+            Subp_Spec_F_Subp_Name    => No_Node_Rewriting_Handle,
+            Subp_Spec_F_Subp_Params  => New_F_Subp_Params,
+            Subp_Spec_F_Subp_Returns => New_Return_Type);
+
+         return Make_Anonymous_Type_Decl
+           (Create_Access_To_Subp_Def
+              (RC,
+               Access_Def_F_Has_Not_Null          =>
+                 Clone (Access_Def.F_Has_Not_Null),
+               Access_To_Subp_Def_F_Has_Protected =>
+                 Clone (Access_Def.F_Has_Protected),
+               Access_To_Subp_Def_F_Subp_Spec     => Subp_Spec));
+      end Gen_Type_Expr_For_Access_To_Subp;
+
+      ----------------------
+      -- Make_Formal_Type --
+      ----------------------
+
+      function Make_Formal_Type
+        (TE : Type_Expr'Class) return Node_Rewriting_Handle
+      is
+         Formal_Type_Name : constant Wide_Wide_String :=
+           "Par" & To_Wide_Wide_String (Img (Next_Formal_Index));
+         --  We are going to add a formal type in the generic procedure for the
+         --  type of this argument: this is the name of this formal.
+
+         Is_Tagged : constant Boolean :=
+           TE.P_Designated_Type_Decl.P_Is_Tagged_Type;
+      begin
+         Next_Formal_Index := Next_Formal_Index + 1;
+
+         --  Create the generic formal type node and add it to the list of
+         --  generic formals.
+
+         Append_Child
+           (NP_Nodes.Formals,
+            Create_Generic_Formal_Type_Decl
+              (RC,
+               Generic_Formal_F_Decl    =>
+                 Create_Type_Decl
+                   (RC,
+                    Base_Type_Decl_F_Name     =>
+                      Make_Defining_Name (UIC, Formal_Type_Name),
+
+                    Type_Decl_F_Discriminants =>
+                      Make (UIC, Ada_Unknown_Discriminant_Part),
+
+                    Type_Decl_F_Type_Def      =>
+                      Create_Private_Type_Def
+                        (RC,
+                         Private_Type_Def_F_Has_Abstract =>
+                           (if Is_Tagged
+                            then Make (UIC, Ada_Abstract_Present)
+                            else No_Node_Rewriting_Handle),
+
+                         Private_Type_Def_F_Has_Tagged   =>
+                           (if Is_Tagged
+                            then Make (UIC, Ada_Tagged_Present)
+                            else No_Node_Rewriting_Handle),
+
+                         Private_Type_Def_F_Has_Limited  =>
+                           Make (UIC, Ada_Limited_Present)),
+
+                    Type_Decl_F_Aspects       =>
+                      No_Node_Rewriting_Handle),
+
+               Generic_Formal_F_Aspects => No_Node_Rewriting_Handle));
+
+         --  Add the actual type to the instantiation
+
+         Append_Child (NP_Nodes.Inst_Params, Clone (TE));
+
+         --  Return a reference to this formal
+
+         return Make_Identifier (UIC, Formal_Type_Name);
+      end Make_Formal_Type;
+
+   --  Start of processing for Collect_Null_Proc_Formals
+
+   begin
+      --  Process all formals (there is nothing to do if there is none)
+
+      if Common_Nodes.N_Params.Is_Null then
+         return;
+      end if;
+      for J in 1 .. Common_Nodes.N_Params.Children_Count loop
+         Append_Child
+           (NP_Nodes.Param_Specs,
+            Gen_Proc_Param_For
+              (Common_Nodes.N_Params.Child (J).As_Param_Spec));
+      end loop;
+   end Collect_Null_Proc_Formals;
+
+   ------------------------------
+   -- Complete_Null_Proc_Decls --
+   ------------------------------
+
+   procedure Complete_Null_Proc_Decls
+     (UIC           : Unit_Inst_Context;
+      Common_Nodes  : Degenerate_Subp_Common_Nodes;
+      NP_Nodes      : Null_Proc_Nodes;
+      Subp_Body     : out Node_Rewriting_Handle;
+      Instance      : out Node_Rewriting_Handle;
+      Renaming_Decl : out Node_Rewriting_Handle)
+   is
+      RC : Rewriting_Handle renames UIC.Rewriting_Context;
+      E  : Instrumentation_Entities renames UIC.Entities;
+   begin
+      --  Create the generic subprogram body
+
+      Subp_Body := Create_Subp_Body
+        (RC,
+         Base_Subp_Body_F_Overriding => No_Node_Rewriting_Handle,
+         Base_Subp_Body_F_Subp_Spec  => Clone (NP_Nodes.Subp_Spec),
+         Subp_Body_F_Aspects         => No_Node_Rewriting_Handle,
+
+         Subp_Body_F_Decls =>
+           Create_Declarative_Part
+             (RC,
+              Declarative_Part_F_Decls => Make (UIC, Ada_Ada_Node_List)),
+
+         Subp_Body_F_Stmts =>
+           Create_Handled_Stmts
+             (RC,
+              Handled_Stmts_F_Stmts      => NP_Nodes.Stmt_List,
+              Handled_Stmts_F_Exceptions => No_Node_Rewriting_Handle),
+         Subp_Body_F_End_Name => No_Node_Rewriting_Handle);
+
+      --  Create an instantiation for this generic subprogram
+
+      Instance := Create_Generic_Subp_Instantiation
+        (RC,
+         Generic_Subp_Instantiation_F_Overriding => No_Node_Rewriting_Handle,
+
+         Generic_Subp_Instantiation_F_Kind =>
+           Make (UIC, Ada_Subp_Kind_Procedure),
+
+         Generic_Subp_Instantiation_F_Subp_Name =>
+           Make_Defining_Name (UIC, Text (Common_Nodes.N_Name)),
+
+         Generic_Subp_Instantiation_F_Generic_Subp_Name => Create_Dotted_Name
+           (RC,
+            Dotted_Name_F_Prefix => Clone (E.Unit_Buffers),
+            Dotted_Name_F_Suffix => Clone (NP_Nodes.Name)),
+
+         Generic_Subp_Instantiation_F_Params  => NP_Nodes.Inst_Params,
+         Generic_Subp_Instantiation_F_Aspects => No_Node_Rewriting_Handle);
+
+      --  Finally, create the declaration that renames the instantiated generic
+      --  subprogram.
+
+      Renaming_Decl := Create_Subp_Renaming_Decl
+        (RC,
+         Base_Subp_Body_F_Subp_Spec  => Clone (Common_Nodes.N_Spec),
+         Base_Subp_Body_F_Overriding => Clone (Common_Nodes.N_Overriding),
+
+         Subp_Renaming_Decl_F_Renames => Create_Renaming_Clause
+           (RC,
+            Renaming_Clause_F_Renamed_Object => Create_Dotted_Name
+              (RC,
+               Dotted_Name_F_Prefix => Clone (Common_Nodes.Wrapper_Pkg_Name),
+               Dotted_Name_F_Suffix => Clone (Common_Nodes.N_Name))),
+
+         Subp_Renaming_Decl_F_Aspects => No_Node_Rewriting_Handle);
+   end Complete_Null_Proc_Decls;
+
+   -----------------------
+   -- Insert_MCDC_State --
+   -----------------------
+
+   overriding function Insert_MCDC_State
+     (Inserter : in out Expr_Func_MCDC_State_Inserter;
+      UIC      : in out Unit_Inst_Context;
+      Name     : String) return String
+   is
+      RC : Rewriting_Handle renames UIC.Rewriting_Context;
+
+      Holder_Type : constant Wide_Wide_String :=
+        "GNATcov_RTS.Buffers.MCDC_State_Holder";
+
+      State_Identifier : constant Node_Rewriting_Handle :=
+        Make_Identifier (UIC, To_Wide_Wide_String (Name));
+
+      State_Formal : constant Node_Rewriting_Handle :=
+        Create_Defining_Name (RC, State_Identifier);
+
+      State_Param_Spec : constant Node_Rewriting_Handle :=
+        Create_Param_Spec
+          (RC,
+           Param_Spec_F_Ids          =>
+             Create_Regular_Node
+               (RC,
+                Ada_Defining_Name_List,
+                Children => (1 => State_Formal)),
+           Param_Spec_F_Has_Aliased  =>
+             No_Node_Rewriting_Handle,
+           Param_Spec_F_Mode         =>
+             No_Node_Rewriting_Handle,
+           Param_Spec_F_Type_Expr    =>
+             Make_Identifier (UIC, Holder_Type),
+           Param_Spec_F_Default_Expr =>
+             No_Node_Rewriting_Handle,
+           Param_Spec_F_Aspects      =>
+             No_Node_Rewriting_Handle);
+
+      State_Actual : constant Node_Rewriting_Handle :=
+        Create_Qual_Expr
+          (RC,
+           Qual_Expr_F_Prefix =>
+             Make_Identifier (UIC, Holder_Type),
+           Qual_Expr_F_Suffix =>
+             Create_Aggregate
+               (RC,
+                Base_Aggregate_F_Ancestor_Expr => No_Node_Rewriting_Handle,
+                Base_Aggregate_F_Assocs        =>
+                  Create_Regular_Node
+                    (RC,
+                     Kind     => Ada_Assoc_List,
+                     Children =>
+                       (1 => Create_Aggregate_Assoc
+                          (RC,
+                           Aggregate_Assoc_F_Designators =>
+                             Create_Regular_Node
+                               (RC, Ada_Alternatives_List,
+                                (1 => Create_Regular_Node
+                                        (RC, Ada_Others_Designator,
+                                         No_Children))),
+                           Aggregate_Assoc_F_R_Expr =>
+                             Create_Regular_Node
+                               (RC, Ada_Box_Expr, No_Children))))));
+
+   begin
+      if Inserter.Formal_Params = No_Node_Rewriting_Handle then
+
+         --  This is the first MC/DC state argument we need to add for this
+         --  expression function. Create a non-null copy of the formal
+         --  parameter list for the augmented function.
+
+         declare
+            P : constant Params := Inserter.N_Spec.F_Subp_Params;
+         begin
+            Inserter.Formal_Params :=
+              (if P.Is_Null
+               then Make (UIC, Ada_Param_Spec_List)
+               else Clone (P.F_Params));
+         end;
+      end if;
+
+      Append_Child (Inserter.Formal_Params, State_Param_Spec);
+      Append_Child (Inserter.Call_Params, State_Actual);
+
+      return Name & ".State'Address";
+   end Insert_MCDC_State;
+
+   ------------------------------------
+   -- Create_Augmented_Expr_Function --
+   ------------------------------------
+
+   procedure Create_Augmented_Expr_Function
+     (UIC                     : Unit_Inst_Context;
+      Common_Nodes            : Degenerate_Subp_Common_Nodes;
+      Formal_Params           : Node_Rewriting_Handle;
+      Call_Params             : Node_Rewriting_Handle;
+      Augmented_Expr_Function : out Node_Rewriting_Handle;
+      New_Expr_Function       : out Node_Rewriting_Handle)
+   is
+      RC : Rewriting_Handle renames UIC.Rewriting_Context;
+
+      --  Compute the name of the augmented expression function (it will go in
+      --  the wrapper package).
+
+      Orig_Name_Text : constant Wide_Wide_String :=
+        Text (Common_Nodes.N_Name);
+      Is_Op_Symbol : constant Boolean :=
+        Orig_Name_Text (Orig_Name_Text'First) = '"';
+
+      Augmented_Expr_Func_Name : constant Wide_Wide_String :=
+        (if Is_Op_Symbol
+         then Op_Symbol_To_Name (Common_Nodes.N_Name) & "_Op"
+         else Orig_Name_Text) & "_With_State";
+
+      --  Create the expression for New_Expr_Function that will call that
+      --  augmented expression function.
+
+      Call_Expr : constant Node_Rewriting_Handle :=
+        Create_Call_Expr
+          (RC,
+           Call_Expr_F_Name   =>
+             Create_Dotted_Name
+               (RC,
+                Dotted_Name_F_Prefix =>
+                  Clone (Common_Nodes.Wrapper_Pkg_Name),
+                Dotted_Name_F_Suffix =>
+                  Make_Identifier (UIC, Augmented_Expr_Func_Name)),
+           Call_Expr_F_Suffix => Call_Params);
+
+   begin
+      --  Now create New_Expr_Function, which will go right after the wrapper
+      --  package. Move all aspecs from the original function to the new one.
+
+      New_Expr_Function :=
+        Create_Expr_Function
+          (RC,
+           Base_Subp_Body_F_Overriding => Clone (Common_Nodes.N_Overriding),
+           Base_Subp_Body_F_Subp_Spec  => Clone (Common_Nodes.N_Spec),
+           Expr_Function_F_Expr        => Create_Paren_Expr (RC, Call_Expr),
+           Expr_Function_F_Aspects     => Detach (Common_Nodes.N.F_Aspects));
+
+      --  The original expression function becomes the augmented one. Replace
+      --  its name and formal parameter list it a new name.
+
+      Augmented_Expr_Function := Handle (Common_Nodes.N);
+      Replace
+        (Handle (Common_Nodes.N_Name),
+         Make_Identifier (UIC, Augmented_Expr_Func_Name));
+      Set_Child
+        (Handle (Common_Nodes.N_Spec),
+         I_Subp_Spec_F_Subp_Params,
+         Create_Params (RC, Formal_Params));
+   end Create_Augmented_Expr_Function;
+
+   -------------------------
+   -- Is_Self_Referencing --
+   -------------------------
+
+   function Is_Self_Referencing
+     (UIC : Unit_Inst_Context;
+      EF  : Expr_Function) return Boolean
+   is
+      EF_Decl : constant Basic_Decl := EF.As_Basic_Decl;
+
+      function Process_Node (N : Ada_Node'Class) return Visit_Status;
+      --  If N is a reference to EF_Decl, return Stop
+
+      ------------------
+      -- Process_Node --
+      ------------------
+
+      function Process_Node (N : Ada_Node'Class) return Visit_Status is
+         Is_Self_Reference : constant Boolean :=
+           (N.Kind in Ada_Single_Tok_Node
+            and then N.Parent.Kind not in Ada_Defining_Name
+            and then N.As_Single_Tok_Node.P_Referenced_Decl = EF_Decl);
+      begin
+         return (if Is_Self_Reference then Stop else Into);
+      exception
+         when Exc : Property_Error =>
+
+            --  If Libadalang cannot determine what N is a reference to, emit a
+            --  warning and consider it's not a self-reference.
+
+            Report
+              (UIC,
+               EF,
+               "failed to determine referenced declaration: "
+               & Ada.Exceptions.Exception_Information (Exc),
+               Warning);
+            return Into;
+      end Process_Node;
+
+   --  Start of processing for Is_Self_Referencing
+
+   begin
+      --  Return whether we can find at least on enode in EF's expression that
+      --  is a referenc to EF itself.
+
+      return EF.F_Expr.Traverse (Process_Node'Access) = Stop;
+   end Is_Self_Referencing;
+
    ----------------
    -- Append_SCO --
    ----------------
@@ -563,9 +1557,7 @@ package body Instrument.Tree is
       SD_First : constant Nat := SD.Last + 1;
       --  Record first entries used in SC/SD at this recursive level
 
-      Current_Insertion_Info : aliased Insertion_Info :=
-        (Parent => UIC.Current_Insertion_Info,
-         others => <>);
+      Current_Insertion_Info : aliased Insertion_Info := (Method => None);
 
       procedure Extend_Statement_Sequence
         (N           : Ada_Node'Class;
@@ -617,98 +1609,8 @@ package body Instrument.Tree is
       -- Utility functions for node synthesis --
       ------------------------------------------
 
-      No_Children : constant Node_Rewriting_Handle_Array :=
-        (1 .. 0 => No_Node_Rewriting_Handle);
-
       RC : Rewriting_Handle renames UIC.Rewriting_Context;
 
-      function Make (K : Ada_Node_Kind_Type) return Node_Rewriting_Handle is
-        (Create_Node (RC, K));
-
-      function Make_Identifier
-        (Id : Wide_Wide_String) return Node_Rewriting_Handle
-      is
-         (Create_Token_Node (RC, Libadalang.Common.Ada_Identifier, Id));
-
-      function Make_Defining_Name
-        (D_Name : Wide_Wide_String) return Node_Rewriting_Handle
-      is
-         (Create_Defining_Name (RC, Make_Identifier (D_Name)));
-
-      function Make_Formal_Type
-        (FT_Name : Wide_Wide_String;
-         TE      : Type_Expr) return Node_Rewriting_Handle;
-      --  Create a formal type with the given name, suitable for
-      --  instantiation with TE as the actual type.
-
-      function Clone (N : Ada_Node'Class) return Node_Rewriting_Handle is
-        (if N.Is_Null then No_Node_Rewriting_Handle else Clone (Handle (N)));
-
-      function Detach (N : Ada_Node'Class) return Node_Rewriting_Handle;
-      --  Replace N with No_Node_Rewriting_Handle, and return its previous
-      --  handle for possible reuse elsewhere in the tree.
-
-      ------------
-      -- Detach --
-      ------------
-
-      function Detach (N : Ada_Node'Class) return Node_Rewriting_Handle is
-      begin
-         if N.Is_Null then
-            return No_Node_Rewriting_Handle;
-         end if;
-
-         return H : constant Node_Rewriting_Handle := Handle (N) do
-            Replace (H, No_Node_Rewriting_Handle);
-         end return;
-      end Detach;
-
-      ----------------------
-      -- Make_Formal_Type --
-      ----------------------
-
-      function Make_Formal_Type
-        (FT_Name : Wide_Wide_String;
-         TE      : Type_Expr) return Node_Rewriting_Handle
-      is
-         Is_Tagged : constant Boolean :=
-           TE.P_Designated_Type_Decl.P_Is_Tagged_Type;
-
-      begin
-         return
-           Create_Generic_Formal_Type_Decl
-             (RC,
-              Generic_Formal_F_Decl    =>
-                Create_Type_Decl
-                  (RC,
-                   Base_Type_Decl_F_Name     =>
-                     Make_Defining_Name (FT_Name),
-
-                   Type_Decl_F_Discriminants =>
-                     Make (Ada_Unknown_Discriminant_Part),
-
-                   Type_Decl_F_Type_Def      =>
-                     Create_Private_Type_Def
-                       (RC,
-                        Private_Type_Def_F_Has_Abstract =>
-                          (if Is_Tagged
-                           then Make (Ada_Abstract_Present)
-                           else No_Node_Rewriting_Handle),
-
-                        Private_Type_Def_F_Has_Tagged   =>
-                          (if Is_Tagged
-                           then Make (Ada_Tagged_Present)
-                           else No_Node_Rewriting_Handle),
-
-                        Private_Type_Def_F_Has_Limited  =>
-                          Make (Ada_Limited_Present)),
-
-                   Type_Decl_F_Aspects       =>
-                     No_Node_Rewriting_Handle),
-
-              Generic_Formal_F_Aspects => No_Node_Rewriting_Handle);
-      end Make_Formal_Type;
-
       -------------------------------
       -- Extend_Statement_Sequence --
       -------------------------------
@@ -838,7 +1740,10 @@ package body Instrument.Tree is
              From                => F,
              To                  => T,
              Typ                 => Typ,
-             Index               => UIC.Current_Insertion_Info.Index,
+             Index               => (case UIC.Current_Insertion_Info.Method is
+                                     when Statement | Declaration =>
+                                       UIC.Current_Insertion_Info.Index,
+                                     when others => 0),
              Instrument_Location =>
                --  See discussion in comment for declaration of
                --  Instrument_Location_Type.
@@ -871,7 +1776,13 @@ package body Instrument.Tree is
 
          procedure Insert_Statement_Witness (SCE : SC_Entry; LL_SCO_Id : Nat)
            with Pre =>
-             UIC.Current_Insertion_Info.RH_List /= No_Node_Rewriting_Handle;
+             (case UIC.Current_Insertion_Info.Method is
+              when Statement | Declaration =>
+                not UIC.Current_Insertion_Info.Preelab
+                  and then
+                UIC.Current_Insertion_Info.RH_List /= No_Node_Rewriting_Handle,
+              when Expression_Function     => True,
+              when None                    => False);
          --  Insert statement witness call for the given SCE
 
          ------------------------------
@@ -894,51 +1805,176 @@ package body Instrument.Tree is
             UIC.Unit_Bits.Statement_Bits.Append
               ((LL_SCO_Id, Executed => UIC.Unit_Bits.Last_Statement_Bit));
 
-            if SCE.N.Kind = Ada_Elsif_Stmt_Part then
-               declare
-                  Old_Cond : Node_Rewriting_Handle :=
-                    Handle (SCE.N.As_Elsif_Stmt_Part.F_Cond_Expr);
-                  New_Cond : constant Node_Rewriting_Handle :=
-                    Create_Regular_Node
-                      (RC,
-                       Ada_Bin_Op,
-                       Children =>
-                         (1 => Make_Statement_Witness
-                            (UIC,
-                             Bit    => UIC.Unit_Bits.Last_Statement_Bit,
-                             Flavor => Function_Call),
+            case Insert_Info.Method is
+
+            when Statement | Declaration =>
+
+               if SCE.N.Kind = Ada_Elsif_Stmt_Part then
+                  declare
+                     Old_Cond : Node_Rewriting_Handle :=
+                       Handle (SCE.N.As_Elsif_Stmt_Part.F_Cond_Expr);
+                     New_Cond : constant Node_Rewriting_Handle :=
+                       Create_Regular_Node
+                         (RC,
+                          Ada_Bin_Op,
+                          Children =>
+                            (1 => Make_Statement_Witness
+                               (UIC,
+                                Bit    => UIC.Unit_Bits.Last_Statement_Bit,
+                                Flavor => Function_Call),
+
+                             2 => Make (UIC, Ada_Op_Or_Else),
+
+                             --  Placeholder for relocation of old condition
+                             --  after it is detached from the tree.
+
+                             3 => No_Node_Rewriting_Handle));
+
+                  begin
+                     --  Detach old condition from tree and replace it with
+                     --  AND THEN node.
+
+                     Replace (Old_Cond, New_Cond);
+
+                     --  Now reattach old condition in new AND THEN node. If it
+                     --  is AND, OR, XOR or OR ELSE binary operation, we need
+                     --  to wrap it in parens to generate valid code.
+
+                     if Kind (Old_Cond) = Ada_Bin_Op
+                        and then Kind (Child (Old_Cond, 2)) in
+                                 Ada_Op_And
+                               | Ada_Op_Or
+                               | Ada_Op_Xor
+                               | Ada_Op_And_Then
+                     then
+                        Old_Cond := Create_Regular_Node
+                          (RC,
+                           Ada_Paren_Expr,
+                           Children => (1 => Old_Cond));
+                     end if;
+
+                     Set_Child (New_Cond, 3, Old_Cond);
+                  end;
 
-                          2 => Make (Ada_Op_And_Then),
+               else
+                  if Kind (SCE.Insertion_N) = Ada_Accept_Stmt_With_Stmts
+                    and then SCE.Instrument_Location = After
+                  then
+                     --  In the case of an accept_statement containing a
+                     --  sequence of statements, if Instrument_Location is
+                     --  After, we want to call the witness after the entry has
+                     --  been accepted, but before the enclosed statements are
+                     --  executed, so insert the witness call in the inner
+                     --  statement list at first position.
+
+                     Insert_List :=
+                       Child
+                         (Child
+                            (SCE.Insertion_N,
+                             I_Accept_Stmt_With_Stmts_F_Stmts),
+                          I_Handled_Stmts_F_Stmts);
+
+                     Insert_Pos  := 1;
 
-                          --  Placeholder for relocation of old condition after
-                          --  it is detached from the tree.
+                  else
+                     if SCE.Instrument_Location = Before_Parent then
+                        Insert_Info := Insert_Info.Parent;
+                        Insert_Pos := Insert_Info.Index;
+                     else
+                        Insert_Pos := SCE.Index;
+                     end if;
 
-                          3 => No_Node_Rewriting_Handle));
+                     Insert_List := Insert_Info.RH_List;
 
-               begin
-                  --  Detach old condition from tree and replace it with
-                  --  AND THEN node.
+                     --  Adjust insertion to account for any insertion
+                     --  performed outside of the processing of the current
+                     --  list (case of the above special processing for accept
+                     --  statements).  Note that SCE.N might not be a direct
+                     --  element of the enclosing list (e.g. in the case where
+                     --  it is a named statement), so we must first go up to
+                     --  the parent of SCE.N that *is* an element of that list,
+                     --  and *then* scan forward to determine the current
+                     --  position of that parent note within the list.
 
-                  Replace (Old_Cond, New_Cond);
+                     declare
+                        RH_Element_Node : Node_Rewriting_Handle :=
+                          SCE.Insertion_N;
+                        RH_Children_Count : constant Natural :=
+                          Children_Count (Insert_Info.RH_List);
+                     begin
+                        --  Find the parent of SCE.N that is an element of the
+                        --  enclosing list.
 
-                  --  Now reattach old condition in new AND THEN node. If it
-                  --  is AND, OR, XOR or OR ELSE binary operation, we need to
-                  --  wrap it in parens to generate valid code.
+                        while Parent (RH_Element_Node)
+                          /= Insert_Info.RH_List
+                        loop
+                           RH_Element_Node := Parent (RH_Element_Node);
+                        end loop;
 
-                  if Kind (Old_Cond) = Ada_Bin_Op
-                     and then Kind (Child (Old_Cond, 2)) in
-                        Ada_Op_And | Ada_Op_Or | Ada_Op_Xor | Ada_Op_Or_Else
-                  then
-                     Old_Cond := Create_Regular_Node
-                       (RC,
-                        Ada_Paren_Expr,
-                        Children => (1 => Old_Cond));
+                        --  Scan forward in enclosing list for adjusted
+                        --  position of the element node.
+
+                        while Child
+                          (Insert_Info.RH_List,
+                           Integer (Insert_Pos
+                             + Insert_Info.Rewriting_Offset))
+                          /= RH_Element_Node
+                        loop
+                           Insert_Info.Rewriting_Offset :=
+                             Insert_Info.Rewriting_Offset + 1;
+                           pragma Assert
+                             (Insert_Pos + Insert_Info.Rewriting_Offset
+                              <= RH_Children_Count);
+                        end loop;
+                     end;
+
+                     --  The witness is inserted at the current location of the
+                     --  statement, so that it will occur immediately *before*
+                     --  it in the instrumented sources. This is necessary
+                     --  because we want to mark a statement as executed
+                     --  anytime it has commenced execution (including in cases
+                     --  it raises an exception or otherwise transfers
+                     --  control). However in some special cases we have to
+                     --  insert after the statement, see comment for
+                     --  Instrument_Location_Type.
+
+                     Insert_Pos := Insert_Pos
+                       + Insert_Info.Rewriting_Offset
+                       + (case SCE.Instrument_Location is
+                             when Before | Before_Parent => 0,
+                             when After  => 1);
                   end if;
 
-                  Set_Child (New_Cond, 3, Old_Cond);
-               end;
+                  --  Insert witness statement or declaration
+
+                  Insert_Child
+                    (Handle => Insert_List,
+                     Index  => Insert_Pos,
+                     Child  =>
+                       Make_Statement_Witness
+                         (UIC,
+                          Bit    => UIC.Unit_Bits.Last_Statement_Bit,
+                          Flavor =>
+                            (case Insert_Info.Method is
+                             when Statement => Procedure_Call,
+                             when Declaration => Declaration,
+                             when Expression_Function | None =>
+                                    raise Program_Error)));
+
+                  --  Update the rewriting offset iff we inserted an element in
+                  --  the current rewriting list: that offset specifically
+                  --  refers to that list, whereas we may have inserted an item
+                  --  in a nested list, in which case we will adjust
+                  --  automatically the rewriting offset accordingly when
+                  --  processing that list.
+
+                  if Insert_Info.RH_List = Insert_List then
+                     Insert_Info.Rewriting_Offset :=
+                       Insert_Info.Rewriting_Offset + 1;
+                  end if;
+               end if;
 
-            elsif SCE.N.Parent.Kind = Ada_Expr_Function then
+            when Expression_Function =>
 
                --  Wrap the expression in the following construct:
                --
@@ -1056,110 +2092,9 @@ package body Instrument.Tree is
                          2 => Expr)));
                end Witness_For_Expr_Function;
 
-            else
-               if Kind (SCE.Insertion_N) = Ada_Accept_Stmt_With_Stmts
-                 and then SCE.Instrument_Location = After
-               then
-                  --  In the case of an accept_statement containing a sequence
-                  --  of statements, if Instrument_Location is After, we want
-                  --  to call the witness after the entry has been accepted,
-                  --  but before the enclosed statements are executed, so
-                  --  insert the witness call in the inner statement list
-                  --  at first position.
-
-                  Insert_List :=
-                    Child
-                      (Child
-                         (SCE.Insertion_N,
-                          I_Accept_Stmt_With_Stmts_F_Stmts),
-                       I_Handled_Stmts_F_Stmts);
-
-                  Insert_Pos  := 1;
-
-               else
-                  if SCE.Instrument_Location = Before_Parent then
-                     Insert_Info := Insert_Info.Parent;
-                     Insert_Pos := Insert_Info.Index;
-                  else
-                     Insert_Pos := SCE.Index;
-                  end if;
-
-                  Insert_List := Insert_Info.RH_List;
-
-                  --  Adjust insertion to account for any insertion performed
-                  --  outside of the processing of the current list (case of
-                  --  the above special processing for accept statements).
-                  --  Note that SCE.N might not be a direct element of the
-                  --  enclosing list (e.g. in the case where it is a named
-                  --  statement), so we must first go up to the parent of
-                  --  SCE.N that *is* an element of that list, and *then* scan
-                  --  forward to determine the current position of that parent
-                  --  note within the list.
-
-                  declare
-                     RH_Element_Node : Node_Rewriting_Handle :=
-                       SCE.Insertion_N;
-                     RH_Children_Count : constant Natural :=
-                       Children_Count (Insert_Info.RH_List);
-                  begin
-                     --  Find the parent of SCE.N that is an element of the
-                     --  enclosing list.
-
-                     while Parent (RH_Element_Node)
-                       /= Insert_Info.RH_List
-                     loop
-                        RH_Element_Node := Parent (RH_Element_Node);
-                     end loop;
-
-                     --  Scan forward in enclosing list for adjusted position
-                     --  of the element node.
-
-                     while Child
-                       (Insert_Info.RH_List,
-                        Integer (Insert_Pos
-                          + Insert_Info.Rewriting_Offset))
-                       /= RH_Element_Node
-                     loop
-                        Insert_Info.Rewriting_Offset :=
-                          Insert_Info.Rewriting_Offset + 1;
-                        pragma Assert
-                          (Insert_Pos + Insert_Info.Rewriting_Offset
-                           <= RH_Children_Count);
-                     end loop;
-                  end;
-
-                  --  The witness is inserted at the current location of the
-                  --  statement, so that it will occur immediately *before*
-                  --  it in the instrumented sources. This is necessary because
-                  --  we want to mark a statement as executed anytime it has
-                  --  commenced execution (including in cases it raises an
-                  --  exception or otherwise transfers control). However in
-                  --  some special cases we have to insert after the statement,
-                  --  see comment for Instrument_Location_Type.
-
-                  Insert_Pos := Insert_Pos
-                    + Insert_Info.Rewriting_Offset
-                    + (case SCE.Instrument_Location is
-                          when Before | Before_Parent => 0,
-                          when After  => 1);
-               end if;
-
-               --  Insert witness statement or declaration
-
-               Insert_Child
-                 (Handle => Insert_List,
-                  Index  => Insert_Pos,
-                  Child  =>
-                    Make_Statement_Witness
-                      (UIC,
-                       Bit    => UIC.Unit_Bits.Last_Statement_Bit,
-                       Flavor => (if Insert_Info.Witness_Use_Statement
-                                  then Procedure_Call
-                                  else Declaration)));
-
-               Insert_Info.Rewriting_Offset :=
-                 Insert_Info.Rewriting_Offset + 1;
-            end if;
+            when None =>
+               raise Program_Error;
+            end case;
          end Insert_Statement_Witness;
 
       --  Start of processing for Set_Statement_Entry
@@ -1210,24 +2145,31 @@ package body Instrument.Tree is
                   Last               => (J = SC_Last),
                   Pragma_Aspect_Name => Pragma_Aspect_Name);
 
-               --  Can't instrument statement if there is no enclosing list
-               --  to which a witness call can be attached.  Likewise for a
-               --  top-level declaration in a Preelaborate package.
+               --  Insert a witness call for this statement obligation
+               --  unless...
 
-               if UIC.Current_Insertion_Info.Preelab
-                 or else
-                  UIC.Current_Insertion_Info.RH_List = No_Node_Rewriting_Handle
-               then
-                  null;
+               if
+                  --  ... there is no enclosing list to which a witness call
+                  --  can be attached.
+
+                  UIC.Current_Insertion_Info.Method /= None
+
+                  --  ... this is a top-level declaration in a Preelaborate
+                  --  package.
 
-               --  Do not attempt to instrument a pragma that we know for
-               --  certain will not generate code (such as Annotate or
-               --  elaboration control pragmas).
+                  and then (UIC.Current_Insertion_Info.Method
+                              not in Statement | Declaration
+                            or else not UIC.Current_Insertion_Info.Preelab)
 
-               elsif not Is_Pragma
-                 or else Pragma_Might_Generate_Code
-                           (Case_Insensitive_Get_Pragma_Id
-                              (Pragma_Aspect_Name))
+                  --  ... this is a pragma that we know for certain will not
+                  --  generate code (such as Annotate or elaboration control
+                  --  pragmas).
+
+                  and then (not Is_Pragma
+                              or else
+                            Pragma_Might_Generate_Code
+                              (Case_Insensitive_Get_Pragma_Id
+                                 (Pragma_Aspect_Name)))
                then
                   Insert_Statement_Witness (SCE, SCOs.SCO_Table.Last);
                end if;
@@ -1306,81 +2248,6 @@ package body Instrument.Tree is
          end loop;
       end Traverse_Aspects;
 
-      ------------------------------------------------
-      -- Degenerate subprograms                     --
-      -- (null procedures and expression functions) --
-      ------------------------------------------------
-
-      --  Degenerate subprograms require special handling because we need a
-      --  place to insert witness calls for statement coverage, and in the case
-      --  of expression functions, a place to declare temporary local variables
-      --  for the MC/DC state buffer for any decision in the expression.
-      --
-      --  We provide these locations by generating a generic subprogram in the
-      --  pure buffers unit, and replacing the degenerate subprogram with an
-      --  instantiation of that generic subprogram. The statement witness and
-      --  MC/DC state variable declarations are inserted in the generic body.
-      --
-      --  For expression functions, we then create a new, augmented expression
-      --  function that takes the addresses of the MC/DC states as additional
-      --  formal parameters, and we pass this new function as a generic
-      --  parameter in the instantiation.
-      --
-      --  Also note that we wrap both the augmented expression function and
-      --  the generic instantiation in a nested package, so that they do
-      --  not introduce unwanted additional primitive operations. We use
-      --  a renaming-as-body of the instantiation to associate it with the
-      --  original subprogram name, while preserving all aspects and default
-      --  parameters.
-      --
-      --  For instance, given the following null subprogram:
-      --
-      --     procedure Foo
-      --       (Arg1 : Arg1_Type;
-      --        Arg2 : in out Arg2_Type) is null;
-      --
-      --  We generate the following declaration in the pure buffer unit:
-      --
-      --     --  See Gen_Decl below
-      --     generic
-      --        type Par1 (<>) is limited private;
-      --        type Par2 (<>) is limited private;
-      --     procedure Null_Proc_[Subprogram_Index](S|B|U)_Gen
-      --       (Arg1 : Par2;
-      --        Arg2 : in out Par2);
-      --
-      --  and the following body:
-      --
-      --     --  See Gen_Body below
-      --     procedure Null_Proc_[Subprogram_Index](S|B|U)_Gen
-      --       (Arg1 : Par2;
-      --        Arg2 : in out Par2) is
-      --     begin
-      --        [Witness call];
-      --     end;
-
-      --  The expression function MC/DC state inserter inserts MC/DC state
-      --  buffers as variable declartions in the generic body, and ensures
-      --  that references to these variables are passed to the instrumented
-      --  expression function.
-
-      type Expr_Func_MCDC_State_Inserter is new Root_MCDC_State_Inserter with
-         record
-            N_Spec        : Node_Rewriting_Handle;
-            Call_Params   : Node_Rewriting_Handle;
-
-            Formal_Params : Node_Rewriting_Handle := No_Node_Rewriting_Handle;
-            --  Formal parameter list where new parameters are added to hold
-            --  MC/DC temporary buffers. This is set lazily from N_Spec.
-            --  This can therefore be tested for No_Node_Rewriting_Handle to
-            --  determine if any parameter was inserted.
-         end record;
-
-      overriding function Insert_MCDC_State
-        (Inserter : in out Expr_Func_MCDC_State_Inserter;
-         UIC      : in out Unit_Inst_Context;
-         Name     : String) return String;
-
       ------------------------------------
       -- Traverse_Degenerate_Subprogram --
       ------------------------------------
@@ -1389,37 +2256,41 @@ package body Instrument.Tree is
         (N      : Basic_Decl;
          N_Spec : Subp_Spec)
       is
-         Is_Expr_Function : constant Boolean := N.Kind = Ada_Expr_Function;
-         Ctrl_Type        : constant Base_Type_Decl :=
-           N_Spec.P_Primitive_Subp_Tagged_Type;
-
-         N_Expr : constant Expr :=
-           (if Is_Expr_Function
-            then N.As_Expr_Function.F_Expr
-            else No_Expr);
-
-         E : Instrumentation_Entities renames UIC.Entities;
+         --  See the "Degenerate subprograms" comment section above for a
+         --  description of the of transformation we implement in this
+         --  procedure.
 
-         Orig_Subp : constant Node_Rewriting_Handle := Handle (N);
+         Saved_Insertion_Info : constant Insertion_Info_Access :=
+           UIC.Current_Insertion_Info;
+         --  Insertion info inherited from the caller, which "points" to the
+         --  degenerate subprogram N. We "save" it because this procedure
+         --  transiently changes UIC.Current_Insertion_Info.
 
-         Orig_Overriding : constant Overriding_Node :=
-           N.As_Base_Subp_Body.F_Overriding;
+         Saved_MCDC_State_Inserter : constant Any_MCDC_State_Inserter :=
+           UIC.MCDC_State_Inserter;
+         --  Likewise for MC/DC state inserter
 
-         Orig_Spec : constant Node_Rewriting_Handle := Clone (N_Spec);
-         --  Saved copy of the original spec before it is augmented
-         --  with additional parameters for MC/DC states.
+         procedure Insert (New_Node : Node_Rewriting_Handle);
+         --  Insert New_Node in sequence at original location of the degenerate
+         --  subprogram.
 
-         New_Subp_Decl : Node_Rewriting_Handle;
+         ------------
+         -- Insert --
+         ------------
 
-         N_Params : constant Param_Spec_List :=
-           (if N_Spec.F_Subp_Params.Is_Null
-            then No_Param_Spec_List
-            else N_Spec.F_Subp_Params.F_Params);
+         procedure Insert (New_Node : Node_Rewriting_Handle) is
+         begin
+            Insert_Child
+              (Handle => Saved_Insertion_Info.RH_List,
+               Index  => Saved_Insertion_Info.Index
+               + Saved_Insertion_Info.Rewriting_Offset
+               + 1,
+               Child  => New_Node);
+            Saved_Insertion_Info.Rewriting_Offset :=
+              Saved_Insertion_Info.Rewriting_Offset + 1;
+         end Insert;
 
-         Call_Params : constant Node_Rewriting_Handle :=
-           (if Is_Expr_Function
-            then Make (Ada_Assoc_List)
-            else No_Node_Rewriting_Handle);
+         Is_Expr_Function : constant Boolean := N.Kind = Ada_Expr_Function;
 
          Gen_Names_Prefix : constant Wide_Wide_String :=
            To_Wide_Wide_String
@@ -1428,643 +2299,281 @@ package body Instrument.Tree is
               & Img (UIC.Degenerate_Subprogram_Index)
               & Part_Tags (UIC.Instrumented_Unit.Part)
               & '_');
+         --  Prefix for the name of all entities we create here
 
-         Wrapper_Pkg_Name : constant Node_Rewriting_Handle :=
-           Make_Identifier (Gen_Names_Prefix & "Pkg");
-
-         --  The augmented expression function, taking supplementary
-         --  parameters for state buffers, and the generic instantiation,
-         --  must be wrapped in a package so that they do not create
-         --  additional primitive operations.
-
-         Wrapper_Pkg_Decls : constant Node_Rewriting_Handle :=
-           Create_Regular_Node (RC, Ada_Ada_Node_List, No_Children);
-
-         Wrapper_Pkg : constant Node_Rewriting_Handle :=
-           Create_Package_Decl
-             (RC,
-              Base_Package_Decl_F_Package_Name => Wrapper_Pkg_Name,
-              Base_Package_Decl_F_Aspects      =>
-                No_Node_Rewriting_Handle,
-              Base_Package_Decl_F_Public_Part  =>
-                Create_Public_Part
-                  (RC,
-                   Declarative_Part_F_Decls => Wrapper_Pkg_Decls),
-              Base_Package_Decl_F_Private_Part =>
-                No_Node_Rewriting_Handle,
-              Base_Package_Decl_F_End_Name     =>
-                No_Node_Rewriting_Handle);
-
-         N_Subp_Name : constant Defining_Name := N_Spec.F_Subp_Name;
-         --  Node for the original subprogram name. For an expression
-         --  function, will be changed to be used as the name for the
-         --  augmented expression function.
-
-         Orig_Name : constant Libadalang.Analysis.Name := N_Subp_Name.F_Name;
-
-         Saved_Insertion_Info : constant Insertion_Info_Access :=
-           UIC.Current_Insertion_Info;
-
-         procedure Insert (New_Node : Node_Rewriting_Handle);
-         --  Insert New_Node in sequence at original location of the
-         --  degenerate subprogram.
-
-         --  Additional declarations for expression functions only
-
-         Saved_MCDC_State_Inserter : constant Any_MCDC_State_Inserter :=
-           UIC.MCDC_State_Inserter;
-         --  Save location where MC/DC state objects are inserted
-
-         EF_Inserter : aliased Expr_Func_MCDC_State_Inserter :=
-           (N_Spec      => Handle (N_Spec),
-            Call_Params => Call_Params,
-            others      => <>);
-
-         --  Additional declarations for null procedures only
-
-         Gen_Formals : constant Node_Rewriting_Handle :=
-           (if Is_Expr_Function
-            then No_Node_Rewriting_Handle
-            else Make (Ada_Ada_Node_List));
-
-         Gen_Subp_Param_Specs : constant Node_Rewriting_Handle :=
-           (if Is_Expr_Function or else N_Spec.F_Subp_Params.Is_Null
-            then No_Node_Rewriting_Handle
-            else Make (Ada_Param_Spec_List));
-
-         Gen_Subp_Name : constant Wide_Wide_String :=
-           Gen_Names_Prefix & "Gen";
-
-         Gen_Body_Stmt : constant Node_Rewriting_Handle :=
+         Call_Params : constant Node_Rewriting_Handle :=
            (if Is_Expr_Function
-            then No_Node_Rewriting_Handle
-            else Make (Ada_Null_Stmt));
-
-         Gen_Body_Stmt_List : constant Node_Rewriting_Handle :=
-           Create_Regular_Node
-             (RC, Ada_Stmt_List, (1 => Gen_Body_Stmt));
-
-         Gen_Subp_Spec : constant Node_Rewriting_Handle :=
-           Create_Subp_Spec
-             (RC,
-              Subp_Spec_F_Subp_Kind    => Make (Ada_Subp_Kind_Procedure),
-              Subp_Spec_F_Subp_Name    =>
-                Make_Defining_Name (Gen_Subp_Name),
-
-              Subp_Spec_F_Subp_Params  =>
-                (if Gen_Subp_Param_Specs = No_Node_Rewriting_Handle
-                 then No_Node_Rewriting_Handle
-                 else Create_Params
-                        (RC, Params_F_Params => Gen_Subp_Param_Specs)),
-
-              Subp_Spec_F_Subp_Returns => No_Node_Rewriting_Handle);
-
-         Gen_Decl : constant Node_Rewriting_Handle :=
-           Create_Generic_Subp_Decl
-             (RC,
-              Generic_Decl_F_Formal_Part    =>
-                Create_Generic_Formal_Part
-                  (RC, Generic_Formal_Part_F_Decls => Gen_Formals),
-
-              Generic_Subp_Decl_F_Subp_Decl =>
-                Create_Generic_Subp_Internal
-                  (RC,
-                   Generic_Subp_Internal_F_Subp_Spec => Gen_Subp_Spec,
-                   Generic_Subp_Internal_F_Aspects   =>
-                     No_Node_Rewriting_Handle),
-              Generic_Subp_Decl_F_Aspects   => No_Node_Rewriting_Handle);
-
-         Gen_Body_Decls : constant Node_Rewriting_Handle :=
-           Make (Ada_Ada_Node_List);
+            then Make (UIC, Ada_Assoc_List)
+            else No_Node_Rewriting_Handle);
+         --  List of formal/actual associations for the call to the augmented
+         --  function. Unused if we are not processing an expression function.
 
-         Inst_Params : constant Node_Rewriting_Handle :=
-           Make (Ada_Assoc_List);
+         ------------------------------------
+         -- Collection of various nodes... --
+         ------------------------------------
 
-         Gen_Body_Insertion_Info : aliased Insertion_Info :=
-           (RH_List               => Gen_Body_Stmt_List,
-            RH_Private_List       => No_Node_Rewriting_Handle,
-            Index                 => 1,
-            Rewriting_Offset      => 0,
-            Witness_Use_Statement => True,
+         Common_Nodes : constant Degenerate_Subp_Common_Nodes :=
+           Create_Degenerate_Subp_Common_Nodes
+             (UIC, N, N_Spec, Gen_Names_Prefix);
+         --  ... common to all processings in this subprogram
 
-            --  Even if the current package has elaboration restrictions, this
-            --  Insertion_Info is used to insert a witness call in the
-            --  procedure in the generic body, so it has no elaboration
-            --  restriction itself, hence Preelab set to False.
-            Preelab               => False,
+         NP_Nodes : Null_Proc_Nodes;
+         --  ... specifically for the instrumentation of null procedures
 
-            Parent                => null);
+         ------------------------------------------------------------
+         -- Local contexts for statement and MC/DC instrumentation --
+         ------------------------------------------------------------
 
          Saved_Dominant : constant Dominant_Info := Current_Dominant;
          --  Save last statement in current sequence as dominant
 
-         Orig_Subp_Index : constant Positive :=
-           Saved_Insertion_Info.Index +
-             Saved_Insertion_Info.Rewriting_Offset;
-         --  Original position of the degenerate subprogram in the rewritten
-         --  tree.
-
-         Append_List : constant Node_Rewriting_Handle :=
-            (if Saved_Insertion_Info.RH_Private_List
-                  /= No_Node_Rewriting_Handle
-             then Saved_Insertion_Info.RH_Private_List
-             else Saved_Insertion_Info.RH_List);
-
-         ------------
-         -- Insert --
-         ------------
+         New_Insertion_Info : aliased Insertion_Info;
+         --  Witness insertion info for statements (for both null procedures
+         --  and expression functions).
 
-         procedure Insert (New_Node : Node_Rewriting_Handle) is
-         begin
-            Insert_Child
-              (Handle => Saved_Insertion_Info.RH_List,
-               Index  => Saved_Insertion_Info.Index
-               + Saved_Insertion_Info.Rewriting_Offset
-               + 1,
-               Child  => New_Node);
-            Saved_Insertion_Info.Rewriting_Offset :=
-              Saved_Insertion_Info.Rewriting_Offset + 1;
-         end Insert;
+         EF_Inserter : aliased Expr_Func_MCDC_State_Inserter :=
+           (N_Spec        => N_Spec,
+            Call_Params   => Call_Params,
+            Formal_Params => No_Node_Rewriting_Handle);
+         --   MC/DC state inserter for this expression function (unused if
+         --   instrumenting a null procedure).
 
       --  Start of processing for Traverse_Degenerate_Subprogram
 
       begin
          --------------------------
-         -- 0. Preparation steps --
+         -- 1. Preparation steps --
          --------------------------
 
          --  Cannot instrument a (null procedure) primitive of an interface
          --  type, because it must be either abstract or null.
 
          if not Is_Expr_Function
-           and then not Ctrl_Type.Is_Null
-           and then Ctrl_Type.P_Is_Interface_Type
+           and then not Common_Nodes.Ctrl_Type.Is_Null
+           and then Common_Nodes.Ctrl_Type.P_Is_Interface_Type
          then
             return;
          end if;
 
-         if MCDC_Coverage_Enabled or else not Is_Expr_Function then
-            UIC.Degenerate_Subprogram_Index :=
-              UIC.Degenerate_Subprogram_Index + 1;
+         UIC.Degenerate_Subprogram_Index :=
+           UIC.Degenerate_Subprogram_Index + 1;
+
+         if Is_Expr_Function then
 
-            -----------------------------------------------------
-            -- 1. Analysis of the degenerate subprogram's spec --
-            -----------------------------------------------------
+            if MCDC_Coverage_Enabled then
 
-            for J in 1 .. (if N_Params.Is_Null
-                           then 0
-                           else N_Params.Children_Count)
-            loop
-               declare
-                  P_Spec : constant Param_Spec :=
-                    N_Params.Children (J).As_Param_Spec;
-                  P_Type : constant Type_Expr := P_Spec.F_Type_Expr;
-                  Formal_Type_Name : constant Wide_Wide_String :=
-                    "Par" & To_Wide_Wide_String (Img (J));
-
-                  Is_Anonymous_Access : constant Boolean :=
-                    P_Type.Kind = Ada_Anonymous_Type;
-
-                  Formal_Subtype_Indication : constant Subtype_Indication :=
-                    (if Is_Anonymous_Access
-                     then P_Type.As_Anonymous_Type
-                         .F_Type_Decl
-                         .F_Type_Def.As_Type_Access_Def
-                         .F_Subtype_Indication
-                     else P_Type.As_Subtype_Indication);
-
-                  Subp_Param_Type : Node_Rewriting_Handle :=
-                    Make_Identifier (Formal_Type_Name);
-                  --  In the case of an anonymous access parameter, this is
-                  --  subsequently wrapped in an access definition.
+               --  Pass all expression function paramaters to the augmented
+               --  expression function call.
 
-               begin
-                  if Is_Expr_Function then
-                     declare
-                        Param_Ids : constant Defining_Name_List :=
-                          P_Spec.F_Ids;
-                     begin
-                        --  Pass parameter in call
+               for J in 1 .. (if Common_Nodes.N_Params.Is_Null
+                              then 0
+                              else Common_Nodes.N_Params.Children_Count)
+               loop
+                  for Id of Common_Nodes.N_Params.Child (J)
+                           .As_Param_Spec.F_Ids.Children
+                  loop
+                     Append_Child
+                       (Call_Params, Make_Identifier (UIC, Id.Text));
+                  end loop;
+               end loop;
+            end if;
 
-                        for J in 1 .. Param_Ids.Children_Count loop
-                           Append_Child
-                             (Call_Params,
-                              Make_Identifier (Param_Ids.Child (J).Text));
-                        end loop;
-                     end;
+            New_Insertion_Info := (Method => Expression_Function);
 
-                  else
-                     --  Add formal type
+         else
+            --  Null procedure handling: create all the nodes for the
+            --  declaration to generate.
 
-                     Append_Child
-                       (Gen_Formals,
-                        Make_Formal_Type
-                          (Formal_Type_Name,
-                           Formal_Subtype_Indication.As_Type_Expr));
+            Create_Null_Proc_Nodes (NP_Nodes, UIC, N_Spec, Gen_Names_Prefix);
+            Collect_Null_Proc_Formals (Common_Nodes, NP_Nodes, UIC);
 
-                     --  Add formal parameter to generic subprogram spec
+            --  Allow witness insertion for the "null" statement in the generic
+            --  procedure (NP_Nodes.Null_Stmt).
 
-                     if Is_Anonymous_Access then
-                        declare
-                           Anon_Type_Def : constant Type_Access_Def :=
-                             P_Type.As_Anonymous_Type
-                               .F_Type_Decl
-                               .F_Type_Def.As_Type_Access_Def;
-
-                           --  Determine if this is a controlling access
-                           --  parameter, in which case the corresponding
-                           --  formal in the generic subprogram must be
-                           --  explicitly null excluding.
-
-                           Formal_Subt_Decl : constant Base_Type_Decl :=
-                             Formal_Subtype_Indication.P_Designated_Type_Decl;
-                           Is_Controlling : constant Boolean :=
-                             (if Ctrl_Type.Is_Null
-                              then False
-                              else
-                                Formal_Subt_Decl = Ctrl_Type
-                                  or else
-                                Formal_Subt_Decl = Ctrl_Type.P_Full_View);
+            New_Insertion_Info :=
+              (Method                => Statement,
+               RH_List               => NP_Nodes.Stmt_List,
+               Index                 => 1,
+               Rewriting_Offset      => 0,
 
-                        begin
-                           Subp_Param_Type :=
-                             Create_Anonymous_Type_Decl
-                               (RC,
-                                Base_Type_Decl_F_Name                =>
-                                  No_Node_Rewriting_Handle,
-                                Type_Decl_F_Discriminants            =>
-                                  No_Node_Rewriting_Handle,
-                                Type_Decl_F_Type_Def                 =>
-                                  Create_Type_Access_Def
-                                    (RC,
-                                     Access_Def_F_Has_Not_Null            =>
-                                       (if Is_Controlling
-                                        then Make (Ada_Not_Null_Present)
-                                        else Clone
-                                               (Anon_Type_Def.F_Has_Not_Null)),
-                                     Type_Access_Def_F_Has_All            =>
-                                       No_Node_Rewriting_Handle,
-                                     Type_Access_Def_F_Has_Constant       =>
-                                       Clone (Anon_Type_Def.F_Has_Constant),
-                                     Type_Access_Def_F_Subtype_Indication =>
-                                       Subp_Param_Type),
-                                Type_Decl_F_Aspects                  =>
-                                  No_Node_Rewriting_Handle);
-                        end;
-                     end if;
+               --  Even if the current package has elaboration restrictions,
+               --  this Insertion_Info is used to insert a witness call in the
+               --  procedure in the generic body: the elaboration restriction
+               --  does not apply there.
 
-                     Append_Child
-                       (Gen_Subp_Param_Specs,
-                        Create_Param_Spec
-                          (RC,
-                           Param_Spec_F_Ids          =>
-                             Clone (P_Spec.F_Ids),
-                           Param_Spec_F_Has_Aliased  =>
-                             Clone (P_Spec.F_Has_Aliased),
-                           Param_Spec_F_Mode         =>
-                             Clone (P_Spec.F_Mode),
-                           Param_Spec_F_Type_Expr    =>
-                             Subp_Param_Type,
-                           Param_Spec_F_Default_Expr =>
-                             No_Node_Rewriting_Handle,
-                           Param_Spec_F_Aspects      =>
-                             No_Node_Rewriting_Handle));
-
-                     --  Add actual type to instantiation
+               Preelab               => False,
 
-                     Append_Child
-                       (Inst_Params, Clone (Formal_Subtype_Indication));
-                  end if;
-               end;
-            end loop;
+               Parent                => null);
          end if;
 
          ----------------------------------
          -- 2. Statement instrumentation --
          ----------------------------------
 
-         --  The statement witness for the null statement (null procedure) or
-         --  return statement (expression function) will be inserted in the
-         --  generic body.
-
-         UIC.Current_Insertion_Info :=
-           Gen_Body_Insertion_Info'Unchecked_Access;
+         UIC.Current_Insertion_Info := New_Insertion_Info'Unchecked_Access;
+         UIC.MCDC_State_Inserter := EF_Inserter'Unchecked_Access;
 
          --  Output statement SCO for degenerate subprogram body (null
          --  statement or freestanding expression) outside of the dominance
-         --  chain. Note that the notional null statement for a null procedure
-         --  is not materialized in the Libadalang tree, so we instead use the
-         --  spec node to provide a sloc.
+         --  chain.
 
          Current_Dominant := No_Dominant;
          if Is_Expr_Function then
-            Extend_Statement_Sequence (N_Expr, 'X');
+            declare
+               N_Expr : constant Expr := N.As_Expr_Function.F_Expr;
+            begin
+               Extend_Statement_Sequence (N_Expr, 'X');
+               Process_Decisions_Defer (N_Expr, 'X');
+            end;
          else
+            --  Even though there is a "null" keyword in the null procedure,
+            --  is no dedicated node for it in the Libadalang parse tree: use
+            --  the whole null procedure declaration to provide a sloc.
+
             Extend_Statement_Sequence
               (N           => N,
                Typ         => 'X',
-               Insertion_N => Gen_Body_Stmt);
-         end if;
-
-         EF_Inserter.Call_Params := Call_Params;
-
-         UIC.MCDC_State_Inserter := EF_Inserter'Unchecked_Access;
-
-         if Is_Expr_Function then
-            Process_Decisions_Defer (N_Expr, 'X');
+               Insertion_N => NP_Nodes.Null_Stmt);
          end if;
          Set_Statement_Entry;
 
-         UIC.MCDC_State_Inserter := Saved_MCDC_State_Inserter;
-
          --  Restore current dominant information designating last statement
          --  in previous sequence (i.e. make the dominance chain skip over
          --  the degenerate body).
 
          Current_Dominant := Saved_Dominant;
 
+         --  Restore saved insertion context
+
+         UIC.MCDC_State_Inserter := Saved_MCDC_State_Inserter;
          UIC.Current_Insertion_Info := Saved_Insertion_Info;
 
-         --  Now see if we need to generate an instrumented subprogram
+         --  If we are instrumenting an expression function but are not going
+         --  to instrument a decision in it, there is no need to generate the
+         --  augmented expression function: stop there.
 
          if Is_Expr_Function
               and then
-             (not MCDC_Coverage_Enabled
-                or else
-              EF_Inserter.Formal_Params = No_Node_Rewriting_Handle)
+            EF_Inserter.Formal_Params = No_Node_Rewriting_Handle
          then
             return;
          end if;
 
-         --  Remove the original declaration from the tree
+         ----------------------------
+         -- 3. Rework declarations --
+         ----------------------------
+
+         --  Remove the original declaration (N) from the tree. Note that since
+         --  .RH_List (the instrumented list of declarations from which N must
+         --  be removed) may contain more elements than before instrumenting.
+         --  So in order to remove it, we must recompute N's index in .RH_List.
 
-         pragma Assert
-           (Orig_Subp =
-              Child
-                (Saved_Insertion_Info.RH_List,
-                 Orig_Subp_Index));
          Remove_Child
-           (Saved_Insertion_Info.RH_List,
-            Orig_Subp_Index);
+           (Saved_Insertion_Info.RH_List, Index_In_Rewriting_Tree (N));
          Saved_Insertion_Info.Rewriting_Offset :=
            Saved_Insertion_Info.Rewriting_Offset - 1;
 
-         --  If there is no previous declaration, generate one, keeping the
-         --  original aspects and default parameters. Then make sure that
-         --  the original null procedure or expression function is detached
-         --  from the tree.
-
-         if N.As_Base_Subp_Body.P_Previous_Part.Is_Null then
-            New_Subp_Decl :=
-              Create_Subp_Decl (RC,
-                                Classic_Subp_Decl_F_Overriding =>
-                                  Detach (Orig_Overriding),
-                                Classic_Subp_Decl_F_Subp_Spec  =>
-                                  Orig_Spec,
-                                Subp_Decl_F_Aspects            =>
-                                  Detach (N.F_Aspects));
-            Insert (New_Subp_Decl);
-         end if;
-
-         --  For an expression function, insert wrapper package now.
-         --  For a null procedure it, push it down to the end of this list
-         --  of declarations.
-
-         if Is_Expr_Function then
-            Insert (Wrapper_Pkg);
-         else
-            Append_Child (Append_List, Wrapper_Pkg);
+         --  For null procedures, if there is no previous declaration, generate
+         --  one, keeping the original aspects and default parameters. Then
+         --  make sure that the original null procedure is detached from the
+         --  tree.
+         --
+         --  Note that we must not do this for expression functions, as having
+         --  both a function declaration and the completing function expression
+         --  in the same scope triggers early freezing for controlling types
+         --  involved. This means that instrumenting would move the freezing
+         --  point, which can produce invalid Ada sources (for instance
+         --  primitives cannot be declared after the freezing point, and
+         --  primitives could be declared after this expression function).
+         --
+         --  ... except for self-referencing expression functions (for instance
+         --  recursive ones), as the generated code requires the declaration to
+         --  be legal Ada.
+
+         if N.As_Base_Subp_Body.P_Previous_Part.Is_Null
+            and then (not Is_Expr_Function
+                      or else Is_Self_Referencing (UIC, N.As_Expr_Function))
+         then
+            Insert (Create_Subp_Decl
+              (RC,
+               Classic_Subp_Decl_F_Overriding =>
+                 Detach (Common_Nodes.N_Overriding),
+               Classic_Subp_Decl_F_Subp_Spec  => Clone (N_Spec),
+               Subp_Decl_F_Aspects            => Detach (N.F_Aspects)));
          end if;
 
          if Is_Expr_Function then
-            -------------------------------------------
-            -- 3(ef). Insert new expression function --
-            -------------------------------------------
-
             declare
-               Orig_Name_Text : constant Wide_Wide_String :=
-                 Text (Orig_Name);
-               Is_Op_Symbol : constant Boolean :=
-                 Orig_Name_Text (Orig_Name_Text'First) = '"';
-
-               Augmented_Expr_Func_Name : constant Wide_Wide_String :=
-                 (if Is_Op_Symbol then
-                     Op_Symbol_To_Name (N_Subp_Name.F_Name) & "_Op"
-                  else Orig_Name_Text) & "_With_State";
-
-               Call_Expr : constant Node_Rewriting_Handle :=
-                 Create_Call_Expr
-                   (RC,
-                    Call_Expr_F_Name   =>
-                      Create_Dotted_Name
-                        (RC,
-                         Dotted_Name_F_Prefix =>
-                           Clone (Wrapper_Pkg_Name),
-                         Dotted_Name_F_Suffix =>
-                           Make_Identifier (Augmented_Expr_Func_Name)),
-                    Call_Expr_F_Suffix => Call_Params);
-
-               New_Expr_Func : constant Node_Rewriting_Handle :=
-                 Create_Expr_Function
-                   (RC,
-                    Base_Subp_Body_F_Overriding => Clone (Orig_Overriding),
-                    Base_Subp_Body_F_Subp_Spec  => Clone (Orig_Spec),
-                    Expr_Function_F_Expr        =>
-                      Create_Paren_Expr (RC, Call_Expr),
-                    Expr_Function_F_Aspects     => Detach (N.F_Aspects));
-
+               Augmented_Expr_Function : Node_Rewriting_Handle;
+               New_Expr_Function       : Node_Rewriting_Handle;
             begin
-               --  Set new name for original expression function
+               --  Create the augmented expression function and amend the
+               --  original one.
 
-               Set_Child
-                 (Handle (N_Subp_Name),
-                  I_Defining_Name_F_Name,
-                  Make_Identifier (Augmented_Expr_Func_Name));
+               Create_Augmented_Expr_Function
+                 (UIC,
+                  Common_Nodes,
+                  EF_Inserter.Formal_Params,
+                  Call_Params,
+                  Augmented_Expr_Function,
+                  New_Expr_Function);
 
-               --  ... move it to the wrapper package
+               --  First comes the wrapper package, then the new expression
+               --  function.
 
-               Append_Child (Wrapper_Pkg_Decls, Orig_Subp);
+               Insert (Common_Nodes.Wrapper_Pkg);
+               Insert (New_Expr_Function);
 
-               --  Insert new expression function calling instrumented one
+               --  The augmented expression function must appear in the
+               --  wrapper package.
 
-               Insert (New_Expr_Func);
+               Append_Child (Common_Nodes.Wrapper_Pkg_Decls, Handle (N));
             end;
 
          else
-
-            --------------------------------------------------------
-            -- 3(np). Insert procedure instantiation and renaming --
-            --------------------------------------------------------
+            --  For null procedures...
 
             declare
-               Gen_Body : constant Node_Rewriting_Handle :=
-                 Create_Subp_Body
-                   (RC,
-                    Base_Subp_Body_F_Overriding => No_Node_Rewriting_Handle,
-                    Base_Subp_Body_F_Subp_Spec  => Clone (Gen_Subp_Spec),
-                    Subp_Body_F_Aspects         => No_Node_Rewriting_Handle,
+               Subp_Body     : Node_Rewriting_Handle;
+               Instance      : Node_Rewriting_Handle;
+               Renaming_Decl : Node_Rewriting_Handle;
+            begin
+               --  Create the generic subprogram body, its instantiation and
+               --  a renaming for that instatiation.
 
-                    Subp_Body_F_Decls           =>
-                      Create_Declarative_Part
-                        (RC,
-                         Declarative_Part_F_Decls => Gen_Body_Decls),
+               Complete_Null_Proc_Decls
+                 (UIC,
+                  Common_Nodes,
+                  NP_Nodes,
+                  Subp_Body,
+                  Instance,
+                  Renaming_Decl);
 
-                    Subp_Body_F_Stmts           =>
-                      Create_Handled_Stmts
-                        (RC,
-                         Handled_Stmts_F_Stmts      =>
-                           Gen_Body_Stmt_List,
-                         Handled_Stmts_F_Exceptions =>
-                           No_Node_Rewriting_Handle),
-                    Subp_Body_F_End_Name        => No_Node_Rewriting_Handle);
-
-               Instance : constant Node_Rewriting_Handle :=
-                 Create_Generic_Subp_Instantiation
-                   (RC,
-                    Generic_Subp_Instantiation_F_Overriding        =>
-                      No_Node_Rewriting_Handle,
-                    Generic_Subp_Instantiation_F_Kind              =>
-                      Make (Ada_Subp_Kind_Procedure),
-                    Generic_Subp_Instantiation_F_Subp_Name         =>
-                      Create_Defining_Name (RC, Detach (Orig_Name)),
-                    Generic_Subp_Instantiation_F_Generic_Subp_Name =>
-                      Create_Dotted_Name
-                        (RC,
-                         Dotted_Name_F_Prefix =>
-                           Clone (E.Unit_Buffers),
-                         Dotted_Name_F_Suffix =>
-                           Make_Identifier (Gen_Subp_Name)),
-                    Generic_Subp_Instantiation_F_Params            =>
-                      Inst_Params,
-                    Generic_Subp_Instantiation_F_Aspects           =>
-                      No_Node_Rewriting_Handle);
-
-               Renaming_Decl : constant Node_Rewriting_Handle :=
-                 Create_Subp_Renaming_Decl
-                   (RC,
-                    Base_Subp_Body_F_Subp_Spec   =>
-                      Clone (Orig_Spec),
-                    Base_Subp_Body_F_Overriding  =>
-                      Clone (Orig_Overriding),
-                    Subp_Renaming_Decl_F_Renames =>
-                      Create_Renaming_Clause
-                        (RC,
-                         Renaming_Clause_F_Renamed_Object =>
-                           Create_Dotted_Name
-                             (RC,
-                              Dotted_Name_F_Prefix =>
-                                Clone (Wrapper_Pkg_Name),
-                              Dotted_Name_F_Suffix =>
-                                Clone (Orig_Name))),
-                    Subp_Renaming_Decl_F_Aspects =>
-                      No_Node_Rewriting_Handle);
+               --  Insert the renaming in the wrapper package
 
-            begin
-               Append_Child (Wrapper_Pkg_Decls, Instance);
-               Append_Child (Append_List, Renaming_Decl);
+               Append_Child (Common_Nodes.Wrapper_Pkg_Decls, Instance);
+
+               --  Push the wrapper package and the renaming down to the end of
+               --  the current list of declarations.
+
+               Append_Child
+                 (Common_Nodes.Append_List, Common_Nodes.Wrapper_Pkg);
+               Append_Child (Common_Nodes.Append_List, Renaming_Decl);
 
-               --  Unparse the generic now, for later insertion in the pure
-               --  buffers unit (at which time the rewriting context will no
-               --  longer be available).
+               --  Unparse the generic subprogram now, for later insertion in
+               --  the pure buffers unit (at which time the rewriting context
+               --  will no longer be available).
 
                UIC.Degenerate_Subprogram_Generics.Append
                  ((Generic_Subp_Decl =>
-                       To_Unbounded_Wide_Wide_String (Unparse (Gen_Decl)),
+                     To_Unbounded_Wide_Wide_String
+                       (Unparse (NP_Nodes.Subp_Decl)),
                    Generic_Subp_Body =>
-                     To_Unbounded_Wide_Wide_String (Unparse (Gen_Body))));
+                     To_Unbounded_Wide_Wide_String (Unparse (Subp_Body))));
             end;
          end if;
       end Traverse_Degenerate_Subprogram;
 
-      -----------------------
-      -- Insert_MCDC_State --
-      -----------------------
-
-      overriding function Insert_MCDC_State
-        (Inserter : in out Expr_Func_MCDC_State_Inserter;
-         UIC      : in out Unit_Inst_Context;
-         Name     : String) return String
-      is
-         pragma Unreferenced (UIC);
-
-         Holder_Type : constant Wide_Wide_String :=
-           "GNATcov_RTS.Buffers.MCDC_State_Holder";
-
-         State_Identifier : constant Node_Rewriting_Handle :=
-           Make_Identifier (To_Wide_Wide_String (Name));
-
-         State_Formal : constant Node_Rewriting_Handle :=
-           Create_Defining_Name (RC, State_Identifier);
-
-         State_Param_Spec : constant Node_Rewriting_Handle :=
-           Create_Param_Spec
-             (RC,
-              Param_Spec_F_Ids          =>
-                Create_Regular_Node
-                  (RC,
-                   Ada_Defining_Name_List,
-                   Children => (1 => State_Formal)),
-              Param_Spec_F_Has_Aliased  =>
-                No_Node_Rewriting_Handle,
-              Param_Spec_F_Mode         =>
-                No_Node_Rewriting_Handle,
-              Param_Spec_F_Type_Expr    =>
-                Make_Identifier (Holder_Type),
-              Param_Spec_F_Default_Expr =>
-                No_Node_Rewriting_Handle,
-              Param_Spec_F_Aspects      =>
-                No_Node_Rewriting_Handle);
-
-         State_Actual : constant Node_Rewriting_Handle :=
-           Create_Qual_Expr
-             (RC,
-              Qual_Expr_F_Prefix =>
-                Make_Identifier (Holder_Type),
-              Qual_Expr_F_Suffix =>
-                Create_Aggregate
-                  (RC,
-                   Base_Aggregate_F_Ancestor_Expr => No_Node_Rewriting_Handle,
-                   Base_Aggregate_F_Assocs        =>
-                     Create_Regular_Node
-                       (RC,
-                        Kind     => Ada_Assoc_List,
-                        Children =>
-                          (1 => Create_Aggregate_Assoc
-                             (RC,
-                              Aggregate_Assoc_F_Designators =>
-                                Create_Regular_Node
-                                  (RC, Ada_Alternatives_List,
-                                   (1 => Create_Regular_Node
-                                           (RC, Ada_Others_Designator,
-                                            No_Children))),
-                              Aggregate_Assoc_F_R_Expr =>
-                                Create_Regular_Node
-                                  (RC, Ada_Box_Expr, No_Children))))));
-
-      begin
-         if Inserter.Formal_Params = No_Node_Rewriting_Handle then
-            if Child (Inserter.N_Spec, I_Subp_Spec_F_Subp_Params)
-              = No_Node_Rewriting_Handle
-            then
-               Set_Child
-                 (Inserter.N_Spec,
-                  I_Subp_Spec_F_Subp_Params,
-                  Create_Params
-                    (Handle          => RC,
-                     Params_F_Params => Make (Ada_Param_Spec_List)));
-            end if;
-            Inserter.Formal_Params :=
-              Child
-                (Child (Inserter.N_Spec, I_Subp_Spec_F_Subp_Params),
-                 I_Params_F_Params);
-         end if;
-
-         Append_Child (Inserter.Formal_Params, State_Param_Spec);
-         Append_Child (Inserter.Call_Params, State_Actual);
-
-         return Name & ".State'Address";
-      end Insert_MCDC_State;
-
       --------------------------------
       -- Traverse_Subp_Decl_Or_Stub --
       --------------------------------
@@ -2900,6 +3409,9 @@ package body Instrument.Tree is
          end case;
       end Traverse_One;
 
+      Saved_Insertion_Info : constant Insertion_Info_Access :=
+         UIC.Current_Insertion_Info;
+
       Items_Count : constant Natural :=
         (if L.Is_Null then 0 else L.Children_Count);
 
@@ -2918,16 +3430,29 @@ package body Instrument.Tree is
 
       --  Set up rewriting for lists of declarations/statements
 
-      Current_Insertion_Info.Preelab := Preelab;
-      if not L.Is_Null and then L.Kind /= Ada_Pragma_Node_List then
-         Current_Insertion_Info.RH_List := Handle (L);
-         if not Priv_Part.Is_Null then
-            Current_Insertion_Info.RH_Private_List :=
-              Handle (Priv_Part.F_Decls);
-         end if;
+      if not (L.Is_Null or else L.Kind = Ada_Pragma_Node_List) then
+         declare
+            Method : constant Insertion_Method :=
+              (if L.Kind = Ada_Stmt_List
+               then Statement
+               else Declaration);
+            II : Insertion_Info (Method);
+         begin
+            II.RH_List := Handle (L);
+            II.Index := 0;
+            II.Rewriting_Offset := 0;
+            II.Preelab := Preelab;
+            II.Parent := Saved_Insertion_Info;
+
+            if Method = Declaration then
+               II.RH_Private_List :=
+                 (if Priv_Part.Is_Null
+                  then No_Node_Rewriting_Handle
+                  else Handle (Priv_Part.F_Decls));
+            end if;
 
-         Current_Insertion_Info.Witness_Use_Statement :=
-           L.Kind = Ada_Stmt_List;
+            Current_Insertion_Info := II;
+         end;
       end if;
 
       --  Loop through statements or declarations
@@ -2936,7 +3461,9 @@ package body Instrument.Tree is
          declare
             N : constant Ada_Node := L.Child (J);
          begin
-            Current_Insertion_Info.Index := J;
+            if Current_Insertion_Info.Method in Statement | Declaration then
+               Current_Insertion_Info.Index := J;
+            end if;
             Traverse_One (N);
          end;
       end loop;
@@ -2949,7 +3476,7 @@ package body Instrument.Tree is
 
       --  Pop insertion info
 
-      UIC.Current_Insertion_Info := Current_Insertion_Info.Parent;
+      UIC.Current_Insertion_Info := Saved_Insertion_Info;
       return Current_Dominant;
    end Traverse_Declarations_Or_Statements;
 
diff --git a/tools/gnatcov/instrument.adb b/tools/gnatcov/instrument.adb
index 2b370bb22..1d7b8e7e4 100644
--- a/tools/gnatcov/instrument.adb
+++ b/tools/gnatcov/instrument.adb
@@ -2,7 +2,7 @@
 --                                                                          --
 --                               GNATcoverage                               --
 --                                                                          --
---                     Copyright (C) 2008-2020, AdaCore                     --
+--                     Copyright (C) 2008-2021, AdaCore                     --
 --                                                                          --
 -- GNATcoverage is free software; you can redistribute it and/or modify it  --
 -- under terms of the GNU General Public License as published by the  Free  --
@@ -359,6 +359,10 @@ package body Instrument is
       Put_Warnings_And_Style_Checks_Pragmas (File);
       Put_Language_Version_Pragma;
       File.Put_Line ("with System;");
+
+      File.Put_Line ("with GNATcov_RTS;");
+      File.Put_Line (Runtime_Version_Check);
+
       File.New_Line;
       File.Put_Line ("package " & Pkg_Name & " is");
       File.New_Line;
@@ -392,6 +396,7 @@ package body Instrument is
 
          Create_File (Info, File, To_Filename (Info.Project, CU_Name));
 
+         Put_Warnings_And_Style_Checks_Pragmas (File);
          Put_Language_Version_Pragma;
          File.Put_Line ("package body " & Pkg_Name & " is");
          File.New_Line;
@@ -510,8 +515,7 @@ package body Instrument is
    ----------------------------------
 
    procedure Instrument_Units_Of_Interest
-     (Dump_Trigger         : Any_Dump_Trigger;
-      Dump_Channel         : Any_Dump_Channel;
+     (Dump_Config          : Any_Dump_Config;
       Language_Version     : Any_Language_Version;
       Ignored_Source_Files : access GNAT.Regexp.Regexp)
    is
@@ -534,7 +538,7 @@ package body Instrument is
 
       Main_To_Instrument_Vector : Main_To_Instrument_Vectors.Vector;
       --  List of mains to instrument *which are not units of interest*. Always
-      --  empty when Dump_Trigger is Manual.
+      --  empty when Dump_Config.Trigger is Manual.
       --
       --  We need a separate list for these as mains which are units of
       --  interest are instrumented to dump coverage buffers at the same time
@@ -543,8 +547,7 @@ package body Instrument is
       --  Then create the instrumenter context
 
       IC                : Inst_Context := Create_Context
-         (Provider, Dump_Trigger, Dump_Channel, Language_Version,
-          Ignored_Source_Files);
+         (Provider, Dump_Config, Language_Version, Ignored_Source_Files);
       Root_Project_Info : constant Project_Info_Access :=
          Get_Or_Create_Project_Info (IC, Project.Project.Root_Project);
 
@@ -663,7 +666,7 @@ package body Instrument is
       --  If we need to instrument all Ada mains, also go through them now, so
       --  that we can prepare output directories for their projects later on.
 
-      if Dump_Trigger /= Manual then
+      if Dump_Config.Trigger /= Manual then
          for Main of Project.Enumerate_Ada_Mains loop
             Register_Main_To_Instrument
               (IC, Main_To_Instrument_Vector, Main.File, Main.Project);
diff --git a/tools/gnatcov/instrument.ads b/tools/gnatcov/instrument.ads
index 1a0769a73..0e9d87143 100644
--- a/tools/gnatcov/instrument.ads
+++ b/tools/gnatcov/instrument.ads
@@ -2,7 +2,7 @@
 --                                                                          --
 --                               GNATcoverage                               --
 --                                                                          --
---                     Copyright (C) 2008-2018, AdaCore                     --
+--                     Copyright (C) 2008-2021, AdaCore                     --
 --                                                                          --
 -- GNATcoverage is free software; you can redistribute it and/or modify it  --
 -- under terms of the GNU General Public License as published by the  Free  --
@@ -18,10 +18,14 @@
 
 --  Support for source instrumentation
 
+with Ada.Strings.Unbounded;
+
 with GNAT.Regexp;
 
 package Instrument is
 
+   package US renames Ada.Strings.Unbounded;
+
    ---------------------------------------------
    -- Mapping of coverage buffer bits to SCOs --
    ---------------------------------------------
@@ -47,20 +51,51 @@ package Instrument is
    --  Channel where to dump coverage buffers. See the user documentation for
    --  the --dump-channel command-line option.
 
+   type Any_Dump_Config (Channel : Any_Dump_Channel := Any_Dump_Channel'First)
+   is record
+      Trigger : Any_Dump_Trigger := Manual;
+
+      case Channel is
+         when Binary_File =>
+            Filename_Simple : Boolean := False;
+            --  Whether to generate source traces with simple filenames.
+            --
+            --  Controlled by --dump-filename-simple.
+
+            Filename_Env_Var : US.Unbounded_String;
+            --  Name of the environment variable which, if set, contains the
+            --  default filename for created source traces. If empty, use the
+            --  default one (see Default_Trace_Filename_Env_Var in
+            --  GNATcov_RTS.Traces.Output.Files).
+            --
+            --  Controlled by --dump-filename-env-var.
+
+            Filename_Prefix  : US.Unbounded_String;
+            --  Prefix for the source trace filename. If empty, use the
+            --  program's basename (see Default_Trace_Filename_Prefix in
+            --  GNATcov_RTS.Traces.Output.Files).
+            --
+            --  Controlled by --dump-filename-prefix.
+         when others =>
+            null;
+      end case;
+   end record;
+   --  Bundle for all configuration related to automatic dump of coverage
+   --  buffers.
+
    type Any_Language_Version is (Ada_83, Ada_95, Ada_2005, Ada_2012);
 
    procedure Instrument_Units_Of_Interest
-     (Dump_Trigger         : Any_Dump_Trigger;
-      Dump_Channel         : Any_Dump_Channel;
+     (Dump_Config          : Any_Dump_Config;
       Language_Version     : Any_Language_Version;
       Ignored_Source_Files : access GNAT.Regexp.Regexp);
    --  Generate instrumented sources for the source files of all units of
    --  interest. Also save mappings between coverage buffers and SCOs for each
    --  library units to SID files (one per library unit).
    --
-   --  Depending on Dump_Trigger and Dump_Channel, instrument mains to schedule
-   --  a call to the dump procedure for the list of coverage buffers in all
-   --  mains in the project.
+   --  Depending on Dump_Config, instrument mains to schedule a call to the
+   --  dump procedure for the list of coverage buffers in all mains in the
+   --  project.
    --
    --  Language_Version restricts what source constructs the instrumenter is
    --  allowed to use. For instance, if Ada_2005 (or a lower version) is
diff --git a/tools/gnatcov/rts/gnatcov_rts-buffers.adb b/tools/gnatcov/rts/gnatcov_rts-buffers.adb
index ea4fc3ce0..68d00bd2e 100644
--- a/tools/gnatcov/rts/gnatcov_rts-buffers.adb
+++ b/tools/gnatcov/rts/gnatcov_rts-buffers.adb
@@ -45,7 +45,7 @@ package body GNATcov_RTS.Buffers is
    is
    begin
       Witness (Buffer_Address, Bit);
-      return (Data => True);
+      return (Data => False);
    end Witness;
 
    function Witness
@@ -53,7 +53,7 @@ package body GNATcov_RTS.Buffers is
    is
    begin
       Witness (Buffer_Address, Bit);
-      return True;
+      return False;
    end Witness;
 
    function Witness
diff --git a/tools/gnatcov/rts/gnatcov_rts-traces-output-base64.adb b/tools/gnatcov/rts/gnatcov_rts-traces-output-base64.adb
index 2308f316b..5cb9c0781 100644
--- a/tools/gnatcov/rts/gnatcov_rts-traces-output-base64.adb
+++ b/tools/gnatcov/rts/gnatcov_rts-traces-output-base64.adb
@@ -2,7 +2,7 @@
 --                                                                          --
 --                   GNATcoverage Instrumentation Runtime                   --
 --                                                                          --
---                     Copyright (C) 2019-2020, AdaCore                     --
+--                     Copyright (C) 2019-2021, AdaCore                     --
 --                                                                          --
 -- GNATcoverage is free software; you can redistribute it and/or modify it  --
 -- under terms of the GNU General Public License as published by the  Free  --
@@ -24,8 +24,12 @@
 
 --  This unit needs to be compilable with Ada 95 compilers
 
+with GNATcov_RTS.Traces.Output.Text_IO;
+
 package body GNATcov_RTS.Traces.Output.Base64 is
 
+   package TIO renames Output.Text_IO;  --  Just a shorthand
+
    --  Base64-over-stdout stream
 
    type Uint6 is mod 2 ** 6;
@@ -138,11 +142,11 @@ package body GNATcov_RTS.Traces.Output.Base64 is
       --  Introduce a newline when needed in order to avoid exceeding 80
       --  characters per line.
 
-      Ada.Text_IO.Put (Out_Digits);
+      TIO.Put (Out_Digits);
       Output.Columns := Output.Columns + 4;
       if Output.Columns >= 80 then
          Output.Columns := 0;
-         Ada.Text_IO.New_Line;
+         TIO.New_Line;
       end if;
 
       Output.Bytes := (others => 0);
@@ -165,15 +169,15 @@ package body GNATcov_RTS.Traces.Output.Base64 is
          Next    => 1,
          Columns => 0);
    begin
-      Ada.Text_IO.New_Line;
-      Ada.Text_IO.Put_Line ("== GNATcoverage source trace file ==");
+      TIO.New_Line;
+      TIO.Put_Line ("== GNATcoverage source trace file ==");
       Helper (Buffer, Buffers, Program_Name, Exec_Date, User_Data);
       Flush (Buffer);
       if Buffer.Columns /= 0 then
-         Ada.Text_IO.New_Line;
+         TIO.New_Line;
       end if;
-      Ada.Text_IO.Put_Line ("== End ==");
-      Ada.Text_IO.New_Line;
+      TIO.Put_Line ("== End ==");
+      TIO.New_Line;
    end Write_Trace_File;
 
 end GNATcov_RTS.Traces.Output.Base64;
diff --git a/tools/gnatcov/rts/gnatcov_rts-traces-output-base64.ads b/tools/gnatcov/rts/gnatcov_rts-traces-output-base64.ads
index 5585de4b9..771d01472 100644
--- a/tools/gnatcov/rts/gnatcov_rts-traces-output-base64.ads
+++ b/tools/gnatcov/rts/gnatcov_rts-traces-output-base64.ads
@@ -2,7 +2,7 @@
 --                                                                          --
 --                   GNATcoverage Instrumentation Runtime                   --
 --                                                                          --
---                     Copyright (C) 2019-2020, AdaCore                     --
+--                     Copyright (C) 2019-2021, AdaCore                     --
 --                                                                          --
 -- GNATcoverage is free software; you can redistribute it and/or modify it  --
 -- under terms of the GNU General Public License as published by the  Free  --
@@ -24,8 +24,6 @@
 
 --  This unit needs to be compilable with Ada 95 compilers
 
-with Ada.Text_IO;
-
 package GNATcov_RTS.Traces.Output.Base64 is
 
    procedure Write_Trace_File
diff --git a/tools/gnatcov/rts/gnatcov_rts-traces-output-bytes_io.adb b/tools/gnatcov/rts/gnatcov_rts-traces-output-bytes_io.adb
new file mode 100644
index 000000000..42d4e845d
--- /dev/null
+++ b/tools/gnatcov/rts/gnatcov_rts-traces-output-bytes_io.adb
@@ -0,0 +1,64 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                   GNATcoverage Instrumentation Runtime                   --
+--                                                                          --
+--                       Copyright (C) 2021, AdaCore                        --
+--                                                                          --
+-- GNATcoverage is free software; you can redistribute it and/or modify it  --
+-- under terms of the GNU General Public License as published by the  Free  --
+-- Software  Foundation;  either version 3,  or (at your option) any later  --
+-- version. This software is distributed in the hope that it will be useful --
+-- but WITHOUT ANY WARRANTY;  without even the implied warranty of MERCHAN- --
+-- TABILITY or FITNESS FOR A PARTICULAR PURPOSE.                            --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This unit needs to be compilable with Ada 95 compilers
+
+package body GNATcov_RTS.Traces.Output.Bytes_IO is
+
+   ------------
+   --  Close --
+   ------------
+
+   procedure Close (File : in out File_Type) is
+   begin
+      OSLIB.Close (FD => File);
+   end Close;
+
+   -------------
+   --  Create --
+   -------------
+
+   procedure Create (File : in out File_Type; Name : String) is
+      use type OSLIB.File_Descriptor;
+   begin
+      File := OSLIB.Create_File (Name => Name, Fmode => OSLIB.Binary);
+      if File = OSLIB.Invalid_FD then
+         raise IO_Error;
+      end if;
+   end Create;
+
+   ------------
+   --  Write --
+   ------------
+
+   procedure Write (File : File_Type; Byte : U8) is
+      N : Integer;
+   begin
+      N := OSLIB.Write (FD => File, A => Byte'Address, N => 1);
+      if N /= 1 then
+         raise IO_Error;
+      end if;
+   end Write;
+
+end GNATcov_RTS.Traces.Output.Bytes_IO;
diff --git a/tools/gnatcov/rts/gnatcov_rts-traces-output-bytes_io.ads b/tools/gnatcov/rts/gnatcov_rts-traces-output-bytes_io.ads
new file mode 100644
index 000000000..d9b371237
--- /dev/null
+++ b/tools/gnatcov/rts/gnatcov_rts-traces-output-bytes_io.ads
@@ -0,0 +1,61 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                   GNATcoverage Instrumentation Runtime                   --
+--                                                                          --
+--                       Copyright (C) 2021, AdaCore                        --
+--                                                                          --
+-- GNATcoverage is free software; you can redistribute it and/or modify it  --
+-- under terms of the GNU General Public License as published by the  Free  --
+-- Software  Foundation;  either version 3,  or (at your option) any later  --
+-- version. This software is distributed in the hope that it will be useful --
+-- but WITHOUT ANY WARRANTY;  without even the implied warranty of MERCHAN- --
+-- TABILITY or FITNESS FOR A PARTICULAR PURPOSE.                            --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This unit needs to be compilable with Ada 95 compilers
+
+--  This provides the base IO interface for use by the "bin-file" trace
+--  dumper, restricted to configurations where we can assume that a full
+--  GNAT RTS is available.
+--
+--  The interface is devised as a simple subset of Ada.Direct_IO. It may
+--  be used from "atexit" handlers though, so may only resort to low level
+--  mechanisms as this triggers after the runtime has been finalized.
+
+--  The base IO interface exposed by GNAT.OS_Lib, going through elementary
+--  int file descriptors, is well suited for our purpose.
+
+with Interfaces;
+with GNAT.OS_Lib;
+
+private package GNATcov_RTS.Traces.Output.Bytes_IO is
+
+   package OSLIB renames GNAT.OS_Lib;
+
+   subtype File_Type is OSLIB.File_Descriptor;
+   subtype U8 is Interfaces.Unsigned_8;
+
+   IO_Error : exception;
+   --  Exception we raise in case of errors reported by the underlying
+   --  IO engine.
+
+   procedure Close (File : in out File_Type);
+
+   procedure Create (File : in out File_Type; Name : String);
+   --  Create or reset a file of the requested Name, ready for writing
+   --  in binary mode. Raise IO_Error if the operation somehow fails and
+   --  would yield an invalid File descriptor.
+
+   procedure Write (File : File_Type; Byte : U8);
+
+end GNATcov_RTS.Traces.Output.Bytes_IO;
diff --git a/tools/gnatcov/rts/gnatcov_rts-traces-output-files.adb b/tools/gnatcov/rts/gnatcov_rts-traces-output-files.adb
index fc0f36bf4..ef091d796 100644
--- a/tools/gnatcov/rts/gnatcov_rts-traces-output-files.adb
+++ b/tools/gnatcov/rts/gnatcov_rts-traces-output-files.adb
@@ -2,7 +2,7 @@
 --                                                                          --
 --                   GNATcoverage Instrumentation Runtime                   --
 --                                                                          --
---                     Copyright (C) 2019-2020, AdaCore                     --
+--                     Copyright (C) 2019-2021, AdaCore                     --
 --                                                                          --
 -- GNATcoverage is free software; you can redistribute it and/or modify it  --
 -- under terms of the GNU General Public License as published by the  Free  --
@@ -24,108 +24,200 @@
 
 --  This unit needs to be compilable with Ada 95 compilers
 
-with Ada.Calendar.Conversions;
 with Ada.Command_Line;
-with Ada.Direct_IO;
-
-with Interfaces;
-with Interfaces.C;
 with Interfaces.C.Strings;
-
 with System;
 
-with GNATcov_RTS.Buffers; use GNATcov_RTS.Buffers;
+with GNATcov_RTS.Traces.Output.Bytes_IO;
 
 package body GNATcov_RTS.Traces.Output.Files is
 
-   package Bytes_IO is new Ada.Direct_IO (Interfaces.Unsigned_8);
+   package BIO renames Output.Bytes_IO;  --  Just a shorthand
+
+   type Process_Id is new Interfaces.Unsigned_64;
+   function Current_Process_Id return Process_Id;
+   pragma Import (C, Current_Process_Id, "gnatcov_rts_getpid");
 
    procedure Write_Bytes
-     (File  : in out Bytes_IO.File_Type;
+     (File  : in out BIO.File_Type;
       Bytes : System.Address;
       Count : Natural);
    --  Callback for GNATcov_RTS.Traces.Output.Generic_Write_Trace_File
 
-   ----------------------------
-   -- Default_Trace_Filename --
-   ----------------------------
+   function Basename (Name : String) return String;
+   --  Return the base name of the Name file.
+   --
+   --  Note that this unit must be compilable with an Ada 95 compiler, so this
+   --  is a good enough replacement of Ada.Directories.Simple_Name (introduced
+   --  in Ada 2005).
 
-   function Default_Trace_Filename return String is
+   function Environment_Variable (Name : String) return String;
+   --  Return the value for the Name environment variable. Return an empty
+   --  string if there is no matching environment variable.
+   --
+   --  Note that this unit must be compilable with an Ada 95 compiler, so this
+   --  is a good enough replacement of Ada.Environment_Variables (introduced in
+   --  Ada 2005).
+
+   Hex_Digits : constant array (0 .. 15) of Character := "0123456789abcdef";
+   function Hex_Image (Value : Unsigned_64) return String;
+   --  Return Timestamp as an hexadecimal string
+
+   function Default_Trace_Basename
+     (Prefix : String := Default_Trace_Filename_Prefix;
+      Tag    : String := "";
+      Simple : Boolean := False) return String;
+   --  Helper for Default_Trace_Filename, to be called when the environment
+   --  variable does not provide the source trace filename. Return the basename
+   --  for the source trace file.
+
+   --------------
+   -- Basename --
+   --------------
+
+   function Basename (Name : String) return String is
+      First : Natural := Name'Last + 1;
+   begin
+      for J in reverse Name'Range loop
+         exit when Name (J) = '/' or Name (J) = '\';
+         First := J;
+      end loop;
+      return Name (First .. Name'Last);
+   end Basename;
 
-      --  We need this unit to be compileable in Ada 95 mode, so we cannot
-      --  use:
-      --
-      --  * Ada.Environment_Variables: directly use the libc's getenv function.
-      --  * Ada.Directories.Simple_Name: do a good enough approximation
-      --    instead.
+   --------------------------
+   -- Environment_Variable --
+   --------------------------
 
+   function Environment_Variable (Name : String) return String is
       use Interfaces.C.Strings;
 
-      function Environment_Variable (Name : String) return String;
-      --  Return the value for the Name environment variable. Return an empty
-      --  string if there is no matching environment variable.
+      function getenv (Name : chars_ptr) return chars_ptr;
+      pragma Import (C, getenv);
+
+      C_Name : chars_ptr          := New_String (Name);
+      Result : constant chars_ptr := getenv (C_Name);
+   begin
+      Free (C_Name);
+      if Result = Null_Ptr then
+         return "";
+      else
+         return Value (Result);
+      end if;
+   end Environment_Variable;
 
-      function Basename (Name : String) return String;
-      --  Return the base name of the Name file
+   -----------------------------------
+   -- Default_Trace_Filename_Prefix --
+   -----------------------------------
 
-      --------------------------
-      -- Environment_Variable --
-      --------------------------
+   function Default_Trace_Filename_Prefix return String is
+   begin
+      return Basename (Ada.Command_Line.Command_Name);
+   end Default_Trace_Filename_Prefix;
 
-      function Environment_Variable (Name : String) return String is
-         function getenv (Name : chars_ptr) return chars_ptr;
-         pragma Import (C, getenv);
+   ---------------
+   -- Hex_Image --
+   ---------------
 
-         C_Name : chars_ptr := New_String (Name);
-         Result : constant chars_ptr := getenv (C_Name);
+   function Hex_Image (Value : Unsigned_64) return String is
+      Remaining  : Unsigned_64 := Value;
+      Result     : String (1 .. 16);
+      Next_Digit : Positive := Result'Last;
+   begin
+      --  Store the actual result in Result (Next_Digit - 1 .. Result'Last),
+      --  updating Next_Digit as we progress (Remaining is updated each time
+      --  we add a digit).
+
+      if Value = 0 then
+         return "0";
+      end if;
+
+      while Remaining /= 0 loop
+         Result (Next_Digit) :=
+            Hex_Digits (Natural (Remaining mod 16));
+         Remaining := Remaining / 16;
+         Next_Digit := Next_Digit - 1;
+      end loop;
+      return Result (Next_Digit + 1 .. Result'Last);
+   end Hex_Image;
+
+   ----------------------------
+   -- Default_Trace_Basename --
+   ----------------------------
+
+   function Default_Trace_Basename
+     (Prefix : String := Default_Trace_Filename_Prefix;
+      Tag    : String := "";
+      Simple : Boolean := False) return String
+   is
+      Extension : constant String := ".srctrace";
+   begin
+      if Simple then
+         return Prefix & Extension;
+      end if;
+
+      declare
+         Suffix : constant String :=
+           "-" & Hex_Image (Unsigned_64 (Current_Process_Id))
+           & "-" & Hex_Image (Unsigned_64 (Clock))
+           & Extension;
       begin
-         Free (C_Name);
-         if Result = Null_Ptr then
-            return "";
+         if Tag = "" then
+            return Prefix & Suffix;
          else
-            return Value (Result);
+            return Prefix & "-" & Tag & Suffix;
          end if;
-      end Environment_Variable;
+      end;
+   end Default_Trace_Basename;
 
-      --------------
-      -- Basename --
-      --------------
+   ----------------------------
+   -- Default_Trace_Filename --
+   ----------------------------
 
-      function Basename (Name : String) return String is
-         First : Natural := Name'Last + 1;
-      begin
-         for J in reverse Name'Range loop
-            exit when Name (J) = '/' or Name (J) = '\';
-            First := J;
-         end loop;
-         return Name (First .. Name'Last);
-      end Basename;
+   function Default_Trace_Filename
+     (Env_Var : String := Default_Trace_Filename_Env_Var;
+      Prefix  : String := Default_Trace_Filename_Prefix;
+      Tag     : String := "";
+      Simple  : Boolean := False) return String
+   is
+      Env_Trace_Filename : constant String := Environment_Variable (Env_Var);
+   begin
+      if Env_Trace_Filename = "" then
+         return Default_Trace_Basename (Prefix, Tag, Simple);
 
-      Env_Trace_Filename : constant String :=
-         Environment_Variable (GNATCOV_TRACE_FILE);
+      elsif Env_Trace_Filename (Env_Trace_Filename'Last) = '/'
+        or else Env_Trace_Filename (Env_Trace_Filename'Last) = '\'
+      then
+         return Env_Trace_Filename
+                & Default_Trace_Basename (Prefix, Tag, Simple);
 
-   begin
-      if Env_Trace_Filename /= "" then
-         return Env_Trace_Filename;
       else
-         return Basename (Ada.Command_Line.Command_Name) & ".srctrace";
+         return Env_Trace_Filename;
       end if;
    end Default_Trace_Filename;
 
+   -----------
+   -- Clock --
+   -----------
+
+   function Clock return Time is
+      function time return Time;
+      pragma Import (C, time, "gnatcov_rts_time_to_uint64");
+   begin
+      return time;
+   end Clock;
+
    -----------------
    -- Format_Date --
    -----------------
 
-   function Format_Date (Date : Ada.Calendar.Time) return Serialized_Timestamp
-   is
-      use Ada.Calendar;
-      use Interfaces.C;
-      Timestamp : long := Ada.Calendar.Conversions.To_Unix_Time (Date);
-      Result    : Serialized_Timestamp;
+   function Format_Date (Timestamp : Time) return Serialized_Timestamp is
+      Result : Serialized_Timestamp;
+      TS     : Time := Timestamp;
    begin
       for I in Result'Range loop
-         Result (I) := Character'Val (Timestamp mod 2 ** 8);
-         Timestamp := Timestamp / 2 ** 8;
+         Result (I) := Character'Val (TS mod 2**8);
+         TS         := TS / 2**8;
       end loop;
       return Result;
    end Format_Date;
@@ -135,7 +227,7 @@ package body GNATcov_RTS.Traces.Output.Files is
    -----------------
 
    procedure Write_Bytes
-     (File  : in out Bytes_IO.File_Type;
+     (File  : in out BIO.File_Type;
       Bytes : System.Address;
       Count : Natural)
    is
@@ -145,13 +237,13 @@ package body GNATcov_RTS.Traces.Output.Files is
       pragma Import (Ada, Content);
    begin
       for I in Content'Range loop
-         Bytes_IO.Write (File, Content (I));
+         BIO.Write (File, Content (I));
       end loop;
       pragma Unreferenced (File);
    end Write_Bytes;
 
    procedure Write_Trace_File is new
-      GNATcov_RTS.Traces.Output.Generic_Write_Trace_File (Bytes_IO.File_Type);
+     GNATcov_RTS.Traces.Output.Generic_Write_Trace_File (BIO.File_Type);
 
    ----------------------
    -- Write_Trace_File --
@@ -159,21 +251,21 @@ package body GNATcov_RTS.Traces.Output.Files is
 
    procedure Write_Trace_File
      (Buffers      : Unit_Coverage_Buffers_Array;
+      Filename     : String := Default_Trace_Filename;
       Program_Name : String := Ada.Command_Line.Command_Name;
-      Filename     : String := "";
-      Exec_Date    : Ada.Calendar.Time := Ada.Calendar.Clock;
+      Exec_Date    : Time := Clock;
       User_Data    : String := "")
    is
-      File : Bytes_IO.File_Type;
+      File : BIO.File_Type;
    begin
       if Filename = "" then
-         Bytes_IO.Create (File, Name => Default_Trace_Filename);
+         BIO.Create (File, Name => Default_Trace_Filename);
       else
-         Bytes_IO.Create (File, Name => Filename);
+         BIO.Create (File, Name => Filename);
       end if;
       Write_Trace_File
         (File, Buffers, Program_Name, Format_Date (Exec_Date), User_Data);
-      Bytes_IO.Close (File);
+      BIO.Close (File);
    end Write_Trace_File;
 
 end GNATcov_RTS.Traces.Output.Files;
diff --git a/tools/gnatcov/rts/gnatcov_rts-traces-output-files.ads b/tools/gnatcov/rts/gnatcov_rts-traces-output-files.ads
index ed484097c..ef0627e3a 100644
--- a/tools/gnatcov/rts/gnatcov_rts-traces-output-files.ads
+++ b/tools/gnatcov/rts/gnatcov_rts-traces-output-files.ads
@@ -24,38 +24,73 @@
 
 --  This unit needs to be compilable with Ada 95 compilers
 
-with Ada.Calendar;
 with Ada.Command_Line;
 
 with GNATcov_RTS.Buffers.Lists; use GNATcov_RTS.Buffers.Lists;
 
 package GNATcov_RTS.Traces.Output.Files is
 
-   GNATCOV_TRACE_FILE : constant String := "GNATCOV_TRACE_FILE";
-   --  Name of the environment variable to contain the default file name for
-   --  output trace files.
+   type Time is new Interfaces.Unsigned_64;
+   --  Derived type to represent timestamps (as a number of seconds elapsed)
 
-   function Default_Trace_Filename return String;
+   Default_Trace_Filename_Env_Var : constant String := "GNATCOV_TRACE_FILE";
+   --  Default name of the environment variable which controls the default
+   --  filename for source traces: see the Default_Trace_Filename function
+   --  below.
+
+   function Clock return Time;
+   --  Returns the number of seconds since the UNIX epoch
+
+   function Default_Trace_Filename_Prefix return String;
+   --  Return the basename for the current program
+
+   function Default_Trace_Filename
+     (Env_Var : String := Default_Trace_Filename_Env_Var;
+      Prefix  : String := Default_Trace_Filename_Prefix;
+      Tag     : String := "";
+      Simple  : Boolean := False) return String;
    --  Return the default name of the trace file to write.
    --
-   --  This returns the content of the GNATCOV_TRACE_FILE environment variable.
-   --  If this environment variable is not defined or empty, fallback to
-   --  "PROGRAM.srctrace", where PROGRAM is the name of the running program.
+   --  If the Env_Var environment variable is not defined or empty, return:
+   --
+   --  * "PROGRAM.srctrace" if Simple is True (PROGRAM is the name of the
+   --    running program).
+   --
+   --  * "PROGRAM-TAG-PID-CLOCK.srctrace" if Simple is False (PID is the
+   --    current process ID and CLOCK is the result of the Clock function in
+   --    decimal representation). The "-TAG" part is omitted if Tag is the
+   --    empty string.
+   --
+   --  If the Env_Var environment variable is defined and not empty, then:
+   --
+   --  * if it ends with "/" or "\", consider it contains the name of a
+   --    directory: use the algorithm described above to compute the basename
+   --    and return the filename in that directory;
+   --
+   --  * otherwise, just return the content of that environment variable.
+   --
+   --  Note that since this unit needs to be compilable with Ada 95 compilers,
+   --  and that there was no standard Ada.Directories package in Ada 95, we
+   --  have no easy access to a predicate checking if a path is a valid
+   --  directory. This is why we use the kludgy separator-ending heuristic here
+   --  instead.
 
-   function Format_Date (Date : Ada.Calendar.Time) return Serialized_Timestamp;
-   --  Return Date represented as a little-endian 64-bit Unix timestamp
+   function Format_Date
+     (Timestamp : Time) return Serialized_Timestamp;
+   --  Return Timestamp represented as a little-endian 64-bit Unix timestamp
 
    procedure Write_Trace_File
      (Buffers      : Unit_Coverage_Buffers_Array;
+      Filename     : String := Default_Trace_Filename;
       Program_Name : String := Ada.Command_Line.Command_Name;
-      Filename     : String := "";
-      Exec_Date    : Ada.Calendar.Time := Ada.Calendar.Clock;
+      Exec_Date    : Time := Clock;
       User_Data    : String := "");
    --  Write a trace file in Filename to contain the data in Buffers.
    --
-   --  If Filename is not provided, use Default_Trace_Filename.
-   --
    --  Program_Name, Exec_Date, and User_Data are used to fill the
    --  corresponding metadata in the written trace file.
+   --
+   --  Exec_Date is given to produce the Timestamp. Use the current
+   --  time by default.
 
 end GNATcov_RTS.Traces.Output.Files;
diff --git a/tools/gnatcov/rts/gnatcov_rts-traces-output-text_io.ads b/tools/gnatcov/rts/gnatcov_rts-traces-output-text_io.ads
new file mode 100644
index 000000000..df45056f8
--- /dev/null
+++ b/tools/gnatcov/rts/gnatcov_rts-traces-output-text_io.ads
@@ -0,0 +1,46 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                   GNATcoverage Instrumentation Runtime                   --
+--                                                                          --
+--                       Copyright (C) 2021, AdaCore                        --
+--                                                                          --
+-- GNATcoverage is free software; you can redistribute it and/or modify it  --
+-- under terms of the GNU General Public License as published by the  Free  --
+-- Software  Foundation;  either version 3,  or (at your option) any later  --
+-- version. This software is distributed in the hope that it will be useful --
+-- but WITHOUT ANY WARRANTY;  without even the implied warranty of MERCHAN- --
+-- TABILITY or FITNESS FOR A PARTICULAR PURPOSE.                            --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This unit needs to be compilable with Ada 95 compilers
+
+--  This provides the base IO interface for use by the "base64-stdout" trace
+--  dumper, available in all configurations.
+--
+--  The interface is devised as a simple subset of Ada.Text_IO. It may
+--  be used from "atexit" handlers though, so may only resort to low level
+--  mechanisms as this triggers after the runtime has been finalized.
+
+--  GNAT.IO provides the low level services we need and is available from
+--  most if not all the GNAT runtime profiles so is a good common ground for
+--  our use.
+
+with GNAT.IO;
+
+private package GNATcov_RTS.Traces.Output.Text_IO is
+
+   procedure New_Line (N : Positive := 1) renames GNAT.IO.New_Line;
+   procedure Put (S : String) renames GNAT.IO.Put;
+   procedure Put_Line (S : String) renames GNAT.IO.Put_Line;
+
+end GNATcov_RTS.Traces.Output.Text_IO;
diff --git a/tools/gnatcov/rts/gnatcov_rts.ads b/tools/gnatcov/rts/gnatcov_rts.ads
index bc18d14f5..a1e4f5ecb 100644
--- a/tools/gnatcov/rts/gnatcov_rts.ads
+++ b/tools/gnatcov/rts/gnatcov_rts.ads
@@ -28,5 +28,13 @@
 --  This unit needs to be compilable with Ada 95 compilers
 
 package GNATcov_RTS is
+
    pragma Pure;
+
+   Version : constant := 1;
+   --  For compatibility with the GNATcoverage in use, GNATcov_RTS is
+   --  versioned.
+   --
+   --  1 -- initial runtime version
+
 end GNATcov_RTS;
diff --git a/tools/gnatcov/rts/gnatcov_rts.gpr b/tools/gnatcov/rts/gnatcov_rts.gpr
index 2972b8a51..c193c69c2 100644
--- a/tools/gnatcov/rts/gnatcov_rts.gpr
+++ b/tools/gnatcov/rts/gnatcov_rts.gpr
@@ -17,6 +17,7 @@ project GNATcov_RTS is
       "gnatcov_rts-traces.adb",
       "gnatcov_rts-traces-output.ads",
       "gnatcov_rts-traces-output.adb",
+      "gnatcov_rts-traces-output-text_io.ads",
       "gnatcov_rts-traces-output-base64.ads",
       "gnatcov_rts-traces-output-base64.adb");
    for Object_Dir use "obj-gnatcov_rts";
diff --git a/tools/gnatcov/rts/gnatcov_rts_c_interface.c b/tools/gnatcov/rts/gnatcov_rts_c_interface.c
new file mode 100644
index 000000000..e1b5d65f0
--- /dev/null
+++ b/tools/gnatcov/rts/gnatcov_rts_c_interface.c
@@ -0,0 +1,44 @@
+/****************************************************************************
+ *                                                                          *
+ *                   GNATcoverage Instrumentation Runtime                   *
+ *                                                                          *
+ *                      Copyright (C) 2020, AdaCore                         *
+ *                                                                          *
+ * GNATcoverage is free software; you can redistribute it and/or modify it  *
+ * under terms of the GNU General Public License as published by the  Free  *
+ * Software  Foundation;  either version 3,  or (at your option) any later  *
+ * version. This software is distributed in the hope that it will be useful *
+ * but WITHOUT ANY WARRANTY;  without even the implied warranty of MERCHAN- *
+ * TABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public *
+ * License for  more details.  You should have  received  a copy of the GNU *
+ * General  Public  License  distributed  with  this  software;   see  file *
+ * COPYING3.  If not, go to http://www.gnu.org/licenses for a complete copy *
+ * of the license.                                                          *
+ *                                                                          *
+ ****************************************************************************/
+
+#include <time.h>
+#include <stdlib.h>
+
+#if defined (_WIN32)
+#  include <processthreadsapi.h>
+#else
+#  include <sys/types.h>
+#  include <unistd.h>
+#endif
+
+#include "gnatcov_rts_c_interface.h"
+
+uint64_t
+gnatcov_rts_time_to_uint64 (void) {
+  return (uint64_t) time (NULL);
+}
+
+uint64_t
+gnatcov_rts_getpid (void) {
+#if defined (_WIN32)
+  return (uint64_t) GetCurrentProcessId ();
+#else
+  return (uint64_t) getpid();
+#endif
+}
diff --git a/tools/gnatcov/rts/gnatcov_rts_c_interface.h b/tools/gnatcov/rts/gnatcov_rts_c_interface.h
new file mode 100644
index 000000000..a8d4dad12
--- /dev/null
+++ b/tools/gnatcov/rts/gnatcov_rts_c_interface.h
@@ -0,0 +1,34 @@
+/****************************************************************************
+ *                                                                          *
+ *                   GNATcoverage Instrumentation Runtime                   *
+ *                                                                          *
+ *                      Copyright (C) 2020, AdaCore                         *
+ *                                                                          *
+ * GNATcoverage is free software; you can redistribute it and/or modify it  *
+ * under terms of the GNU General Public License as published by the  Free  *
+ * Software  Foundation;  either version 3,  or (at your option) any later  *
+ * version. This software is distributed in the hope that it will be useful *
+ * but WITHOUT ANY WARRANTY;  without even the implied warranty of MERCHAN- *
+ * TABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public *
+ * License for  more details.  You should have  received  a copy of the GNU *
+ * General  Public  License  distributed  with  this  software;   see  file *
+ * COPYING3.  If not, go to http://www.gnu.org/licenses for a complete copy *
+ * of the license.                                                          *
+ *                                                                          *
+ ****************************************************************************/
+
+#include <stdint.h>
+
+/* The C "time" function can return integers of
+   different size depending on the platform.
+   Here, we ensure that the returned result will be an
+   expected long long (a 64 bit integer). It will thus
+   be compatible with 32 bit as well as 64 bit architectures.
+   It also ensures compatibility with Ada Long_Long_Integer
+   standard type. */
+extern uint64_t
+gnatcov_rts_time_to_uint64 (void);
+
+/* Return the current process ID as an unsigned 64-bit integer. */
+extern uint64_t
+gnatcov_rts_getpid (void);
diff --git a/tools/gnatcov/rts/gnatcov_rts_full.gpr b/tools/gnatcov/rts/gnatcov_rts_full.gpr
index 26df82a34..507fc1cae 100644
--- a/tools/gnatcov/rts/gnatcov_rts_full.gpr
+++ b/tools/gnatcov/rts/gnatcov_rts_full.gpr
@@ -15,4 +15,6 @@ library project GNATcov_RTS_Full is
    package Compiler is
       for Default_Switches ("Ada") use ("-O2", "-g");
    end Compiler;
+
+   for Languages use ("Ada", "C");
 end GNATcov_RTS_Full;
diff --git a/tools/gnatcov/sc_obligations.adb b/tools/gnatcov/sc_obligations.adb
index 82ce0f1f2..ff4f6ce31 100644
--- a/tools/gnatcov/sc_obligations.adb
+++ b/tools/gnatcov/sc_obligations.adb
@@ -2,7 +2,7 @@
 --                                                                          --
 --                               GNATcoverage                               --
 --                                                                          --
---                     Copyright (C) 2009-2020, AdaCore                     --
+--                     Copyright (C) 2009-2021, AdaCore                     --
 --                                                                          --
 -- GNATcoverage is free software; you can redistribute it and/or modify it  --
 -- under terms of the GNU General Public License as published by the  Free  --
@@ -27,6 +27,7 @@ with Ada.Text_IO;             use Ada.Text_IO;
 with ALI_Files;     use ALI_Files;
 with Aspects;       use Aspects;
 with Checkpoints;   use Checkpoints;
+with Coverage.Source;
 with Coverage.Tags; use Coverage, Coverage.Tags;
 with Diagnostics;   use Diagnostics;
 with Files_Table;   use Files_Table;
@@ -352,14 +353,14 @@ package body SC_Obligations is
    -----------------------------------------
 
    procedure Checkpoint_Load_Merge_Unit
-     (Relocs     : in out Checkpoint_Relocations;
+     (CLS        : access Checkpoint_Load_State;
       CP_CU      : CU_Info;
       Real_CU_Id : CU_Id);
    --  Load CU from checkpoint that corresponds to a current unit of interest
    --  whose ID is Real_CU_Id.
 
    procedure Checkpoint_Load_New_Unit
-     (Relocs     : in out Checkpoint_Relocations;
+     (CLS        : access Checkpoint_Load_State;
       CP_Vectors : Source_Coverage_Vectors;
       CP_CU      : in out CU_Info;
       CP_CU_Id   : CU_Id;
@@ -368,7 +369,7 @@ package body SC_Obligations is
    --  interest. The newly assigned CU_Id is returned in New_CU_Id.
 
    procedure Checkpoint_Load_Unit
-     (Relocs     : in out Checkpoint_Relocations;
+     (CLS        : access Checkpoint_Load_State;
       CP_Vectors : Source_Coverage_Vectors;
       CP_CU      : in out CU_Info;
       CP_CU_Id   : CU_Id;
@@ -435,12 +436,12 @@ package body SC_Obligations is
    --------------------------------
 
    procedure Checkpoint_Load_Merge_Unit
-     (Relocs     : in out Checkpoint_Relocations;
+     (CLS        : access Checkpoint_Load_State;
       CP_CU      : CU_Info;
       Real_CU_Id : CU_Id)
    is
+      Relocs  : Checkpoint_Relocations renames CLS.Relocations;
       Real_CU : CU_Info renames CU_Vector.Reference (Real_CU_Id).Element.all;
-
    begin
       --  Here we already have loaded full SCO information for this CU, so
       --  all we need to do is to populate the tables mapping the SCO and
@@ -486,13 +487,14 @@ package body SC_Obligations is
    ------------------------------
 
    procedure Checkpoint_Load_New_Unit
-     (Relocs     : in out Checkpoint_Relocations;
+     (CLS        : access Checkpoint_Load_State;
       CP_Vectors : Source_Coverage_Vectors;
       CP_CU      : in out CU_Info;
       CP_CU_Id   : CU_Id;
       New_CU_Id  : out CU_Id)
-
    is
+      Relocs : Checkpoint_Relocations renames CLS.Relocations;
+
       New_First_Instance : Inst_Id;
       New_First_SCO      : SCO_Id;
 
@@ -797,6 +799,15 @@ package body SC_Obligations is
       CP_CU.First_SCO := New_First_SCO;
 
       CU_Vector.Append (CP_CU);
+
+      --  If we are loading a SID file, create source coverage data structures.
+      --  There is no need to do it when loading a checkpoint: that checkpoint
+      --  was created loading a SID file, and thus already has the
+      --  corresponding SCI tables populated.
+
+      if CLS.Purpose = Instrumentation then
+         Coverage.Source.Initialize_SCI_For_Instrumented_CU (New_CU_Id);
+      end if;
    end Checkpoint_Load_New_Unit;
 
    --------------------------
@@ -804,12 +815,13 @@ package body SC_Obligations is
    --------------------------
 
    procedure Checkpoint_Load_Unit
-     (Relocs     : in out Checkpoint_Relocations;
+     (CLS        : access Checkpoint_Load_State;
       CP_Vectors : Source_Coverage_Vectors;
       CP_CU      : in out CU_Info;
       CP_CU_Id   : CU_Id;
       New_CU_Id  : out CU_Id)
    is
+      Relocs : Checkpoint_Relocations renames CLS.Relocations;
    begin
       if CP_CU.Provider = Instrumenter then
          Instrumented_Units_Present := True;
@@ -845,7 +857,7 @@ package body SC_Obligations is
 
       if New_CU_Id = No_CU_Id then
          Checkpoint_Load_New_Unit
-           (Relocs,
+           (CLS,
             CP_Vectors,
             CP_CU,
             CP_CU_Id  => CP_CU_Id,
@@ -888,7 +900,7 @@ package body SC_Obligations is
 
             else
                Checkpoint_Load_Merge_Unit
-                 (Relocs,
+                 (CLS,
                   CP_CU      => CP_CU,
                   Real_CU_Id => New_CU_Id);
             end if;
@@ -1041,7 +1053,7 @@ package body SC_Obligations is
                CP_CU    : CU_Info := Element (Cur);
             begin
                Checkpoint_Load_Unit
-                 (Relocs,
+                 (CLS,
                   CP_Vectors,
                   CP_CU,
                   CP_CU_Id  => CP_CU_Id,
@@ -2609,11 +2621,23 @@ package body SC_Obligations is
                else
                   --  Case of >T / >F: dominant SCO is a decision
 
-                  Dom_Sloc_SCO :=
-                    Sloc_To_SCO_Map
-                      (SCOD.Dominant_Sloc.Source_File, Decision)
-                    .Element ((SCOD.Dominant_Sloc.L, No_Local_Location));
-                  pragma Assert (Kind (Dom_Sloc_SCO) = Decision);
+                  if Sloc_To_SCO_Map
+                       (SCOD.Dominant_Sloc.Source_File, Decision)
+                     .Contains ((SCOD.Dominant_Sloc.L, No_Local_Location))
+                  then
+                     Dom_Sloc_SCO :=
+                       Sloc_To_SCO_Map
+                         (SCOD.Dominant_Sloc.Source_File, Decision)
+                       .Element ((SCOD.Dominant_Sloc.L, No_Local_Location));
+                     pragma Assert (Kind (Dom_Sloc_SCO) = Decision);
+                  else
+                     Report
+                       (First_Sloc (SCOD.Sloc_Range),
+                        "dominant decision of statement " & Image (SCO)
+                        & " has no associated SCO"
+                        & ", discarding dominance information");
+                     Dom_Sloc_SCO := No_SCO_Id;
+                  end if;
                end if;
 
                SCOD.Dominant := Dom_Sloc_SCO;
diff --git a/tools/gnatcov/trace_adapters/dynamorio/CMakeLists.txt b/tools/gnatcov/trace_adapters/dynamorio/CMakeLists.txt
index 85a7ad1e5..44adfaf39 100644
--- a/tools/gnatcov/trace_adapters/dynamorio/CMakeLists.txt
+++ b/tools/gnatcov/trace_adapters/dynamorio/CMakeLists.txt
@@ -3,10 +3,12 @@
 # cmake -DDynamoRIO_DIR=$PWD/../dynamorio/cmake ../dr-gnatcov
 # make
 # ../dynamorio/bin64/drrun -client libqtrace.so 0 -- /bin/ls
-
-cmake_minimum_required(VERSION 2.6)
+cmake_minimum_required(VERSION 3.15)
+project(qtrace C)
 
 add_library(qtrace SHARED qtrace.c)
+target_link_libraries(qtrace)
+
 find_package(DynamoRIO)
 if (NOT DynamoRIO_FOUND)
   message(FATAL_ERROR "DynamoRIO package required to build")
diff --git a/tools/gnatcov/trace_adapters/dynamorio/Makefile b/tools/gnatcov/trace_adapters/dynamorio/Makefile
index 4f2637050..8deb8e04c 100644
--- a/tools/gnatcov/trace_adapters/dynamorio/Makefile
+++ b/tools/gnatcov/trace_adapters/dynamorio/Makefile
@@ -7,11 +7,7 @@ DYNRIO_CLIENT=INVALID
 
 ifeq ($(HOST_OS), windows)
 DYNRIO_CLIENT=build/$(DYNRIO_CONFIG)/qtrace.dll
-ifeq ($(BITS_ARCH), 32)
-G_OPTION=-G"Visual Studio 12"
-else
-G_OPTION=-G"Visual Studio 12 Win64"
-endif
+G_OPTION=-G"Visual Studio 17 2022"
 endif
 
 ifeq ($(HOST_OS), linux)
@@ -20,7 +16,7 @@ G_OPTION=
 endif
 
 #########
-# Build #  
+# Build #
 #########
 
 all: $(DYNRIO_CLIENT)
@@ -29,8 +25,8 @@ all: $(DYNRIO_CLIENT)
 
 $(DYNRIO_CLIENT):
 	mkdir build || true
-	cd build && cmake -DDynamoRIO_DIR=$(DYNRIO_PREFIX)/cmake $(G_OPTION) ..
-	cd build && cmake --build . --config $(DYNRIO_CONFIG)
+	cd build && cmake -Wno-dev -DDynamoRIO_DIR=$(DYNRIO_PREFIX)/cmake $(G_OPTION) ..
+	cd build && cmake --build . --config $(DYNRIO_CONFIG) -v
 
 ################
 # Installation #
