Implement first two levels of assertion coverage

This change adds the possibility of computing the coverage of assertions
and contracts for levels:

* ATC (Assertion True Coverage): an assertion is covered if its whole
decision has been evaluated to True at least once.
* ATCC (Assertion True Condition Coverage): and assertion is covered if
every condition of the decision has been evaluated at least once in the
context of an evaluation to True of the whole decision.

The relevant assertions and contracts are Assert, Assert_And_Cut,
Assume, Check, Loop_Invariant, Type_Invariant, Precondition,
Postcondition.

The only unsupported cases are Pre/Postcondition and Type_Invariant as
pragma statements which are not instrumented. A warning is issued
stating as much, and the rest of the code is instrumented as normal.

Issue: #7
TN: O212-062

Author: Viviane Garèse

testsuite/SCOV/internals/cnotes.py

@@ -126,6 +126,11 @@
 
 # cPartCov : independent effect of condition not demonstrated (=report)
 
+# aNoCov    : assertion never evaluated (=report)
+# atNoCov   : assertion expression outcome TRUE never evaluated (=report)
+# acPartCov : assertion condition was never evaluated during an evaluation of
+#             the decision to True (=report)
+
 # xBlock0  : exempted block, 0 deviations (=report)
 # xBlock1  : exempted block, >0 deviations (=report)
 # xBlock2  : exempted block, >0 undetermined coverage items (=report)
@@ -168,8 +173,9 @@
  XotNoCov, XofNoCov, XoPartCov, XoNoCov,
  XcPartCov,
  Xr0, Xr0c,
+ aNoCov, atNoCov, acPartCov,
  blockNote,
- xBlock0, xBlock1, xBlock2) = range(50)
+ xBlock0, xBlock1, xBlock2) = range(53)
 
 NK_image = {None: "None",
             lNoCode: "lNoCode", lNotCoverable: "lNotCoverable",
@@ -192,7 +198,8 @@
             XotNoCov: "XotNoCov", XofNoCov: "XofNoCov", XoPartCov: "XoPartCov",
             XoNoCov: "XoNoCov",
             XcPartCov: "XcPartCov",
-            Xr0: "Xr0", Xr0c: "Xr0c"}
+            Xr0: "Xr0", Xr0c: "Xr0c",
+            aNoCov: "aNoCov", atNoCov: "atNoCov", acPartCov: "acPartCov"}
 
 
 # ===============================
@@ -221,6 +228,9 @@
 # MCDC violations
 cNoteKinds = (etNoCov, efNoCov, ePartCov, eNoCov,  cPartCov, eUndetCov)
 
+# Assertion violations
+aNoteKinds = (aNoCov, atNoCov, acPartCov)
+
 # Exemption regions
 xNoteKinds = (xBlock0, xBlock1, xBlock2)
 
@@ -247,6 +257,7 @@
 # if they could be emitted and report them as unmatched.
 
 erNoteKinds = sNoteKinds+dNoteKinds+cNoteKinds+xNoteKinds+tNoteKinds+XNoteKinds
+erNoteKinds += aNoteKinds
 xrNoteKinds = erNoteKinds+rAntiKinds+XrAntiKinds
 
 

testsuite/SCOV/internals/driver.py

@@ -936,6 +936,13 @@ def check_expectations(self):
             "stmt+decision": 2,
             "stmt+mcdc": 3,
             "stmt+uc_mcdc": 3,
+            "stmt+atc": 1,
+            "stmt+decision+atc": 2,
+            "stmt+decision+atcc": 2,
+            "stmt+mcdc+atc": 3,
+            "stmt+mcdc+atcc": 3,
+            "stmt+uc_mcdc+atc": 3,
+            "stmt+uc_mcdc+atcc": 3,
         }
 
         stricter_level = (
@@ -1164,6 +1171,43 @@ def _scofiles_list(self):
                              for soi in self.sources_of_interest())
                 if scof}
 
+    def wdbase_for(self, covlevel):
+        """
+        Compute a short base prefix for the working directory that will
+        contain the output of coverage analysis for level covlevel.
+
+        Uses the first letter of the highest level ('s' for "stmt" or 'u' for
+        "stmt+uc_mcdc") and the full name of the assertion level if assertion
+        coverage is enabled.
+        """
+        levels = covlevel.split("+")
+
+        if len(levels) == 1:
+            return "s_"
+
+        wdbase = levels[1][0]
+        wdbase += levels[-1] if self.assert_lvl else ""
+
+        return wdbase + "_"
+
+    def xcovlevel_for(self, wdname):
+        """
+        Compute the source coverage level from the working directory prefix
+        by matching the first letter of the highest coverage level plus the
+        full name of the assertion level is enabled.
+        """
+        res = "stmt"
+        wdbase = wdname.split('_')[0]
+
+        for lvl in ["decision", "mcdc", "uc_mcdc"]:
+            if wdbase[0] == lvl[0]:
+                res += "+" + lvl
+
+        if len(wdbase) > 1:
+            res += "+" + wdbase[1:]
+
+        return res
+
 
 class SCOV_helper_bin_traces(SCOV_helper):
     """SCOV_helper specialization for the binary execution trace based mode."""

testsuite/SCOV/internals/rnexpanders.py

@@ -11,9 +11,10 @@
 from .cnotes import (
     xBlock0, xBlock1, sNoCov, sPartCov, sNotCoverable, dfAlways, dtAlways,
     dfNoCov, dtNoCov, dNoCov, dPartCov, efNoCov, etNoCov, eNoCov, ePartCov,
-    cPartCov, Enote, KnoteDict, erNoteKinds, sUndetCov, dUndetCov, eUndetCov,
-    xBlock2, XsNoCov, XsPartCov, XsNotCoverable, XsUndetCov, XotNoCov,
-    XofNoCov, XoPartCov, XoNoCov, XcPartCov
+    cPartCov, aNoCov, atNoCov, acPartCov, Enote, KnoteDict, erNoteKinds,
+    sUndetCov, dUndetCov, eUndetCov, xBlock2, XsNoCov, XsPartCov,
+    XsNotCoverable, XsUndetCov, XotNoCov, XofNoCov, XoPartCov, XoNoCov,
+    XcPartCov
 )
 from .segments import Sloc, Sloc_from_match
 from .stags import Stag_from
@@ -79,7 +80,6 @@ def __init__(self, sloc, diag):
 
 
 def Rdiagline_from(text):
-
     p = re.match(Rdiagline.re, text)
 
     return Rdiagline(sloc=Sloc_from_match(p),
@@ -207,7 +207,6 @@ def __init__(self, re_notes):
         self.enotes = []
 
     def try_parse_enote(self, rline):
-
         dline = Rdiagline_from(rline)
 
         # If no match at all, punt.
@@ -570,6 +569,22 @@ def __init__(self):
         self.noteblocks.append(
             VIOsection(re_start="MCDC COVERAGE", re_notes=mcdc_notes))
 
+        # Assertion coverage
+
+        atc_notes = {
+            "contract expression outcome TRUE never": atNoCov,
+            "contract expression never evaluated": aNoCov,
+        }
+        self.noteblocks.append(
+            VIOsection(re_start="ATC COVERAGE", re_notes=atc_notes))
+
+        atcc_notes = {
+            "condition was never evaluated during an evaluation of the "
+            "decision to True": acPartCov
+        }
+        self.noteblocks.append(
+            VIOsection(re_start="ATCC COVERAGE", re_notes=atcc_notes))
+
         # Non coverable items
 
         nc_notes = {

testsuite/SCOV/internals/xnexpanders.py

@@ -1203,10 +1203,25 @@ def __decode_note_choice(self, text):
             or
             [('stmt', 'l+'), ('stmt+decision', 'l+')]
         """
-        level_from_char = {"s": "stmt",
-                           "d": "stmt+decision",
-                           "m": "stmt+mcdc",
-                           "u": "stmt+uc_mcdc"}
+        level_from_char = {"s": ["stmt"],
+                           "d": ["stmt+decision"],
+                           "m": ["stmt+mcdc"],
+                           "u": ["stmt+uc_mcdc"]}
+
+        def make_assert_lvl_combinaison(assert_lvl):
+            """
+            Add the assertion coverage level assert_lvl to other regular
+            coverage level combinaisons defined in level_from_char. Return the
+            list of combinaisons.
+            """
+            return [level_from_char[c][0] + "+" + assert_lvl
+                    for c in level_from_char]
+
+        assert_level_from_char = {"a": make_assert_lvl_combinaison("atc"),
+                                  "c": make_assert_lvl_combinaison("atcc")}
+
+        level_from_char.update(assert_level_from_char)
+
         result = text.split("=>")
 
         if len(result) == 1:
@@ -1220,7 +1235,12 @@ def __decode_note_choice(self, text):
             note = result[1].lstrip(' ')
             lev_list = result[0].rstrip(' ')
 
-            return [(level_from_char[lchar], note) for lchar in lev_list]
+            res = []
+            for lchar in lev_list:
+                for combinaison in level_from_char[lchar]:
+                    res.append((combinaison, note))
+
+            return res
 
     def __select_lnote(self, text):
         """Decode text to return the line note for the current

testsuite/SCOV/internals/xnotep.py

@@ -18,7 +18,8 @@
     oPartCov, ofNoCov, otNoCov, r0, r0c, sNoCov, sNotCoverable, sPartCov,
     xBlock0, xBlock1, xBlock2, xNoteKinds, lUndetCov, sUndetCov, dUndetCov,
     eUndetCov, XsNoCov, XsPartCov, XsNotCoverable, XsUndetCov, XotNoCov,
-    XofNoCov, XoPartCov, XoNoCov, XcPartCov, Xr0, Xr0c
+    XofNoCov, XoPartCov, XoNoCov, XcPartCov, Xr0, Xr0c, aNoCov, atNoCov,
+    acPartCov
 )
 from .segments import Line, Section, Segment
 from .stags import Stag_from
@@ -181,6 +182,7 @@ class XnoteP:
               'e?': eUndetCov,
               'oT-': otNoCov, 'oF-': ofNoCov, 'o!': oPartCov, 'o-': oNoCov,
               'c!': cPartCov,
+              'a-': aNoCov, 'aT-': atNoCov, 'ac!': acPartCov,
               'x0': xBlock0, 'x+': xBlock1, 'x?': xBlock2,
               '0': r0, '0c': r0c,
               # Exempted notes

testsuite/SCOV/report.py

@@ -16,6 +16,7 @@
 
 from e3.fs import ls
 
+from SCOV.internals.driver import SCOV_helper
 from SCOV.internals.cnotes import xNoteKinds
 from SCOV.internals.tfiles import Tfile
 from SUITE.tutils import XCOV, thistest, frame
@@ -139,15 +140,6 @@ def check(self):
     "stmt+uc_mcdc": ["STMT", "DECISION", "MCDC"]
 }
 
-# Base prefix of the working subdirectory for each xcovlevel. ??? This is
-# relying too much on knowledge about how the testuite driver works ...
-xcovlevel_from = {
-    "sc_": "stmt",
-    "dc_": "stmt+decision",
-    "mc_": "stmt+mcdc",
-    "uc_": "stmt+uc_mcdc"
-}
-
 
 class ReportChecker:
     """Whole report checker"""
@@ -301,7 +293,9 @@ def __process_one_test(self, qde):
         # applicable xcov-level
         self.__setup_expectations(
             ntraces=len(qde.drivers),
-            xcovlevel=xcovlevel_from[os.path.basename(qde.wdir)[0:3]],
+            xcovlevel=SCOV_helper.xcovlevel_for(self.tc,
+                                                os.path.basename
+                                                (qde.wdir)),
             xregions=xregions)
 
         reports = ls(os.path.join(qde.wdir, "test.rep"))

testsuite/SCOV/tc.py

@@ -124,7 +124,7 @@ def __drivers_from(self, cspec):
         return [drv for drv in self.all_drivers if re.search(drv_expr, drv)]
 
     def __init__(self, extradrivers="", extracargs="", category=CAT.auto,
-                 tolerate_messages=None):
+                 tolerate_messages=None, assert_lvl=None):
         # By default, these test cases expect no error from subprocesses (xrun,
         # xcov, etc.)
         self.expect_failures = False
@@ -171,6 +171,8 @@ def __init__(self, extradrivers="", extracargs="", category=CAT.auto,
                          if category == CAT.auto else
                          category)
 
+        self.assert_lvl = assert_lvl
+
         # - extra compilation arguments, added to what --cargs was provided to
         #   the testsuite command line:
         self.extracargs = extracargs
@@ -191,19 +193,24 @@ def __xcovlevels(self):
         if thistest.options.xcov_level:
             return [thistest.options.xcov_level]
 
+        assert not thistest.options.qualif_level
+
         default_xcovlevels_for = {
             # Tests without categories should be ready for anything.
             # Exercise with the strictest possible mode:
-            None: ["stmt+mcdc"],
+            None:         ["stmt+mcdc"],
 
-            CAT.stmt: ["stmt"],
+            CAT.stmt:     ["stmt"],
             CAT.decision: ["stmt+decision"],
-            CAT.mcdc: ["stmt+mcdc", "stmt+uc_mcdc"]}
+            CAT.mcdc:     ["stmt+mcdc", "stmt+uc_mcdc"],
+        }
 
-        defaults = default_xcovlevels_for[self.category]
-        return ([defaults[0]]
-                if thistest.options.qualif_level else
-                defaults)
+        # Add a "+" before the name of the assertion coverage level in order
+        # to append it at the end of the the other specified coverage levels
+        # passed to gnatcov.
+        alvl = ("+" + self.assert_lvl) if self.assert_lvl else ""
+
+        return [d + alvl for d in default_xcovlevels_for[self.category]]
 
     def __register_qde_for(self, drvo):
         """
@@ -215,13 +222,6 @@ def __register_qde_for(self, drvo):
                     drivers=drvo.drivers, xrnotes=drvo.xrnotes,
                     wdir=os.path.normpath(drvo.awdir())))
 
-    # Base prefix for Working directories, per --level. Shared across
-    # runs for multiples levels.
-    _wdbase_for = {"stmt": "st_",
-                   "stmt+decision": "dc_",
-                   "stmt+mcdc": "mc_",
-                   "stmt+uc_mcdc": "uc_"}
-
     def __run_one_covlevel(self, covlevel, covcontrol, subdirhint):
         """
         Run this testcase individual drivers and consolidation tests with
@@ -236,7 +236,7 @@ def __run_one_covlevel(self, covlevel, covcontrol, subdirhint):
 
         # Compute the Working directory base for this level, then run the test
         # for each indivdual driver.
-        this_wdbase = self._wdbase_for[covlevel]
+        this_wdbase = this_scov_helper.wdbase_for(self, covlevel)
 
         wdctl = WdirControl(wdbase=this_wdbase, bdbase=self._available_bdbase,
                             subdirhint=subdirhint)

testsuite/tests/O212-062-assertions/src/assertions.adb

@@ -0,0 +1,59 @@
+pragma Assertion_Policy (Check);
+pragma Ada_2012;
+
+package body Assertions is
+
+   ---------
+   -- Foo --
+   ---------
+
+   function Foo (I : Integer) return Integer
+   is
+      High : Integer := 3;                                     -- # foo_hi_decl
+   begin
+     for J in 1 .. High loop                                   -- # foo_loop_1
+       pragma Loop_Invariant (J = J + 1 - 1 and then J < 4);   -- # foo_inv_1
+     end loop;
+
+     for J in 1 .. High loop                                   -- # foo_loop_2
+       pragma Loop_Invariant (J = J + 1 - 1 or else J < 4);    -- # foo_inv_2
+     end loop;
+     return I;                                                 -- # foo_return
+   end Foo;
+
+   ----------
+   -- Same --
+   ----------
+
+   function Same (A, B : Boolean) return Boolean 
+   is
+      --  Subprogram body with aspect without prior declaration
+
+      function Id (C : Boolean) return Boolean
+        with Pre  => C or else (C or else not C),              -- # id_pre
+             Post => Id'Result = C                             -- # id_post
+      is
+      begin
+         return C;                                             -- # id_ret
+      end Id;
+
+   begin
+      --  Decision nested as parameter of a function call within an assertion.
+      --  The function parameter should not be seen as a condition for the
+      --  assertion decision.
+
+      --  Last two conditions are not evaluated
+
+      pragma Assert (Id (A or else B) or else A or else B);    -- # nested_1
+
+      --  Last condition is not evaluated
+
+      pragma Assert (B or else A or else Id (A or else B));    -- # nested_2
+
+      --  All conditions are evaluated
+
+      pragma Assert (B or else Id (A or else B));              -- # nested_3
+      return B;                                                -- # same_ret
+   end Same;
+
+end Assertions;