Merge branch 'assertion-coverage' into 'master'

Implementation of first two levels of assertion coverage

See merge request eng/cov/gnatcoverage!48

See issue #7 

Implement coverage for assertions for levels ATC and ATCC.

Author: Viviane Garese

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;