Merge pull request #68 from abakst/abakst/errno

Support CodeHawk `errno` analysis

Author: sipma

chc/api/XPredicate.py

@@ -1231,3 +1231,17 @@ def is_valid_mem(self) -> bool:
 
     def __str__(self) -> str:
         return "valid-mem(" + str(self.term) + ")"
+
+
+@ifdregistry.register_tag("ew", XPredicate)
+class XWritesErrno(XPredicate):
+    """errno must have been written locally.
+    """
+
+    def __init__(
+            self, ifd: "InterfaceDictionary", ixval: IT.IndexedTableValue
+    ) -> None:
+        XPredicate.__init__(self, ifd, ixval)
+
+    def __str__(self) -> str:
+        return "errno-must-written()"

chc/cmdline/chkc

@@ -759,7 +759,7 @@ def parse() -> argparse.Namespace:
     cfileanalyze.add_argument(
         "--analysis",
         default="undefined-behavior",
-        choices=["undefined-behavior", "outputparameters"],
+        choices=["undefined-behavior", "outputparameters", "errno"],
         help="choose analysis for creating primary proof obligations")
     cfileanalyze.add_argument(
         "--collect-diagnostics",
@@ -809,7 +809,7 @@ def parse() -> argparse.Namespace:
     cfilereport.add_argument(
         "--analysis",
         default="undefined-behavior",
-        choices=["undefined-behavior", "outputparameters"],
+        choices=["undefined-behavior", "outputparameters", "errno"],
         help="choose analysis for reporting results")
     cfilereport.add_argument(
         "--open",
@@ -857,7 +857,7 @@ def parse() -> argparse.Namespace:
     cfilerun.add_argument(
         "--analysis",
         default="undefined-behavior",
-        choices=["undefined-behavior", "outputparameters"],
+        choices=["undefined-behavior", "outputparameters", "errno"],
         help="choose analysis for creating primary proof obligations")
     cfilerun.add_argument(
         "--collect-diagnostics",
@@ -1588,7 +1588,7 @@ def parse() -> argparse.Namespace:
     cprojectanalyze.add_argument(
         "--analysis",
         default="undefined-behavior",
-        choices=["undefined-behavior", "outputparameters"],
+        choices=["undefined-behavior", "outputparameters", "errno"],
         help="choose analysis for creating primary proof obligations")
     cprojectanalyze.add_argument(
         "--collect-diagnostics",
@@ -1635,7 +1635,7 @@ def parse() -> argparse.Namespace:
     cprojectreport.add_argument(
         "--analysis",
         default="undefined-behavior",
-        choices=["undefined-behavior", "outputparameters"],
+        choices=["undefined-behavior", "outputparameters", "errno"],
         help="choose analysis for reporting results")
     cprojectreport.add_argument(
         "--verbose", "-v",
@@ -1667,7 +1667,7 @@ def parse() -> argparse.Namespace:
     cprojectreportfile.add_argument(
         "--analysis",
         default="undefined-behavior",
-        choices=["undefined-behavior", "outputparameters"],
+        choices=["undefined-behavior", "outputparameters", "errno"],
         help="choose analysis for reporting results")
     cprojectreportfile.add_argument(
         "--showcode",

chc/proof/CPOPredicate.py

@@ -61,6 +61,7 @@
     'cus': 'unsigned-to-signed-cast',
     'cuu': 'unsigned-to-unsigned-cast',
     'dr': 'distinct-region',
+    'ew': 'errno-must-written',
     'fc': 'format-cast',
     'ft': 'format-string',
     'ga': 'global-address',
@@ -2231,6 +2232,24 @@ def __str__(self) -> str:
         return "preserves-all-memory()"
 
 
+@pdregistry.register_tag("ew", CPOPredicate)
+class CPOErrnoMustBeWritten(CPOPredicate):
+    """errno-must-written(): true if errno must have been written locally.
+    """
+
+    def __init__(
+            self, pd: "CFilePredicateDictionary", ixval: IT.IndexedTableValue
+    ) -> None:
+        CPOPredicate.__init__(self, pd, ixval)
+
+    @property
+    def is_errno_must_written(self) -> bool:
+        return True
+
+    def __str__(self) -> str:
+        return "errno-must-written()"
+
+
 @pdregistry.register_tag("pv", CPOPredicate)
 class CPOPreservedValue(CPOPredicate):
     """preserves-value(exp): true of a function that preserves the value of exp.