CMD: add command-line option to control status of system includes

Author: sipma

chc/app/CApplication.py

@@ -93,12 +93,14 @@ def __init__(
             targetpath: str,
             contractpath: str,
             singlefile: bool = False,
+            keep_system_includes: bool = False,
             excludefiles: List[str] = []) -> None:
         self._projectpath = projectpath
         self._projectname = projectname
         self._targetpath = targetpath
         self._contractpath = contractpath
         self._singlefile = singlefile
+        self._keep_system_includes = keep_system_includes
         self._excludefiles = excludefiles
         self._indexmanager = IndexManager(singlefile)
         self._globalcontract: Optional[CGlobalContract] = None
@@ -138,6 +140,19 @@ def globalcontract(self) -> CGlobalContract:
     def is_singlefile(self) -> bool:
         return self._singlefile
 
+    @property
+    def keep_system_includes(self) -> bool:
+        """Returns true if functions from the system path ('/') must be included
+
+        This property is false by default and must be enabled via a command-line
+        option.
+
+        It is intended to, by default, filter out functions defined in header
+        files, that would otherwise be included in every source file.
+        """
+
+        return self._keep_system_includes
+
     @property
     def excludefiles(self) -> List[str]:
         return self._excludefiles

chc/app/CFile.py

@@ -154,6 +154,10 @@ def name(self) -> str:
     def capp(self) -> "CApplication":
         return self._capp
 
+    @property
+    def keep_system_includes(self) -> bool:
+        return self.capp.keep_system_includes
+
     @property
     def targetpath(self) -> str:
         return self.capp.targetpath

chc/app/CFileGlobals.py

@@ -179,6 +179,10 @@ def __init__(self, cfile: "CFile", xnode: ET.Element) -> None:
     def cfile(self) -> "CFile":
         return self._cfile
 
+    @property
+    def keep_system_includes(self) -> bool:
+        return self.cfile.keep_system_includes
+
     @property
     def declarations(self) -> "CFileDeclarations":
         return self.cfile.declarations
@@ -284,6 +288,16 @@ def gfunctions(self) -> Dict[int, CGFunction]:
                     xiloc = xf.get("iloc")
                     if xivinfo is not None and xiloc is not None:
                         vinfo = self.declarations.get_varinfo(int(xivinfo))
+                        if (
+                                not self.keep_system_includes
+                                and vinfo.vdecl is not None
+                                and vinfo.vdecl.file.startswith("/")):
+                            chklogger.logger.info(
+                                "%s: Skip system function %s defined in %s",
+                                self.cfile.cfilename,
+                                vinfo.vname,
+                                vinfo.vdecl.file)
+                            continue
                         loc = self.declarations.get_location(int(xiloc))
                         gfun = CGFunction(loc, vinfo)
                         self._gfunctions[vinfo.vid] = gfun

chc/app/CHVersion.py

@@ -1 +1 @@
-chcversion: str = "0.2.0-2024-11-04"
+chcversion: str = "0.2.0-2025-10-24"

chc/cmdline/AnalysisManager.py

@@ -54,7 +54,7 @@ def __init__(
         wordsize: int = 0,
         unreachability: bool = False,
         thirdpartysummaries: List[str] = [],
-        nofilter: bool = True,
+        keep_system_includes: bool = False,
         verbose: bool = False,
     ) -> None:
         """Initialize the analyzer location and target file location.
@@ -72,13 +72,8 @@ def __init__(
         """
 
         self._capp = capp
-        # self.contractpath = capp.contractpath
         self._config = Config()
-        # self.chsummaries = self.config.summaries
-        # self.path = self.capp.path
-        # self.canalyzer = self.config.canalyzer
-        # self.gui = self.config.chc_gui
-        self.nofilter = nofilter
+        self._keep_system_includes = keep_system_includes
         self.wordsize = wordsize
         self.thirdpartysummaries = thirdpartysummaries
         self.unreachability = unreachability
@@ -88,6 +83,10 @@ def __init__(
     def capp(self) -> "CApplication":
         return self._capp
 
+    @property
+    def keep_system_includes(self) -> bool:
+        return self._keep_system_includes
+
     @property
     def contractpath(self) -> Optional[str]:
         return self.capp.contractpath
@@ -189,8 +188,8 @@ def _create_file_primary_proofobligations_cmd_partial(self) -> List[str]:
             cmd.extend(["-contractpath", self.contractpath])
         cmd.extend(["-projectname", self.capp.projectname])
 
-        if self.nofilter:
-            cmd.append("-nofilter")
+        if self.keep_system_includes:
+            cmd.append("-keep_system_includes")
         if self.wordsize > 0:
             cmd.extend(["-wordsize", str(self.wordsize)])
         cmd.append(self.targetpath)
@@ -283,8 +282,8 @@ def _generate_and_check_file_cmd_partial(
         if not (self.contractpath is None):
             cmd.extend(["-contractpath", self.contractpath])
         cmd.extend(["-projectname", self.capp.projectname])
-        if self.nofilter:
-            cmd.append("-nofilter")
+        if self.keep_system_includes:
+            cmd.append("-keep_system_includes")
         if self.wordsize > 0:
             cmd.extend(["-wordsize", str(self.wordsize)])
         if self.unreachability:

chc/cmdline/ParseManager.py

@@ -72,7 +72,7 @@ def __init__(
             projectpath: str,
             projectname: str,
             targetpath: str,
-            filter: bool = False,
+            keep_system_includes: bool = False,
             posix: bool = False,
             verbose: bool = True,
             keepUnused: bool = False,
@@ -96,7 +96,7 @@ def __init__(
             self._targetpath, self._projectname)
         self._analysisresultspath = UF.get_analysisresults_path(
             self._targetpath, self._projectname)
-        self._filter = filter
+        self._keep_system_includes = keep_system_includes
         self._posix = posix
         self._keepUnused = keepUnused
         self._verbose = verbose
@@ -160,8 +160,8 @@ def tgtplatform(self) -> str:
         return self._tgtplatform
 
     @property
-    def filter(self) -> bool:
-        return self._filter
+    def keep_system_includes(self) -> bool:
+        return self._keep_system_includes
 
     @property
     def posix(self) -> bool:
@@ -439,8 +439,8 @@ def parse_with_ccommands(
                 "-targetdirectory",
                 self.analysisresultspath
             ]
-            if not self.filter:
-                command.append("-nofilter")
+            if self.keep_system_includes:
+                command.append("-keep_system_includes")
             if self.keepUnused:
                 command.append("-keepUnused")
             command.append(ifilename)
@@ -533,8 +533,8 @@ def parse_ifile(self, ifilename: str) -> int:
             "-targetdirectory",
             self.analysisresultspath,
         ]
-        if not self.filter:
-            cmd.append("-nofilter")
+        if not self.keep_system_includes:
+            cmd.append("-keep_system_includes")
         if self.keepUnused:
             cmd.append("-keepUnused")
         cmd.append(ifilename)

chc/cmdline/c_file/cfileutil.py

@@ -117,6 +117,7 @@ def cfile_parse_file(args: argparse.Namespace) -> NoReturn:
     # arguments
     pcfilename: str = os.path.abspath(args.filename)
     opttgtpath: Optional[str] = args.tgtpath
+    keep_system_includes: bool = args.keep_system_includes
     loglevel: str = args.loglevel
     logfilename: Optional[str] = args.logfilename
     logfilemode: str = args.logfilemode
@@ -154,7 +155,8 @@ def cfile_parse_file(args: argparse.Namespace) -> NoReturn:
 
     chklogger.logger.info("Target path: %s", targetpath)
 
-    parsemanager = ParseManager(projectpath, projectname, targetpath)
+    parsemanager = ParseManager(
+        projectpath, projectname, targetpath, keep_system_includes=keep_system_includes)
     parsemanager.remove_semantics()
     parsemanager.initialize_paths()
 
@@ -418,6 +420,7 @@ def cfile_analyze_file(args: argparse.Namespace) -> NoReturn:
     xcfilename: str = args.filename
     opttgtpath: Optional[str] = args.tgtpath
     wordsize: int = args.wordsize
+    keep_system_includes: bool = args.keep_system_includes
     verbose: bool = args.verbose
     loglevel: str = args.loglevel
     logfilename: Optional[str] = args.logfilename
@@ -468,12 +471,21 @@ def cfile_analyze_file(args: argparse.Namespace) -> NoReturn:
     contractpath = os.path.join(targetpath, "chc_contracts")
 
     capp = CApplication(
-        projectpath, projectname, targetpath, contractpath, singlefile=True)
+        projectpath,
+        projectname,
+        targetpath,
+        contractpath,
+        singlefile=True,
+        keep_system_includes=keep_system_includes)
 
     capp.initialize_single_file(cfilename)
     cfile = capp.get_cfile()
 
-    am = AnalysisManager(capp, verbose=verbose, wordsize=wordsize)
+    am = AnalysisManager(
+        capp,
+        verbose=verbose,
+        wordsize=wordsize,
+        keep_system_includes=keep_system_includes)
 
     am.create_file_primary_proofobligations(cfilename)
     am.reset_tables(cfile)
@@ -578,6 +590,7 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn:
     # arguments
     pcfilename: str = os.path.abspath(args.filename)
     opttgtpath: Optional[str] = args.tgtpath
+    keep_system_includes: bool = args.keep_system_includes
     cshowcode: bool = args.showcode
     copen: bool = args.open
     cshowinvariants: bool = args.showinvariants
@@ -622,7 +635,8 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn:
 
     chklogger.logger.info("Target path: %s", targetpath)
 
-    parsemanager = ParseManager(projectpath, projectname, targetpath)
+    parsemanager = ParseManager(
+        projectpath, projectname, targetpath, keep_system_includes=keep_system_includes)
     parsemanager.remove_semantics()
     parsemanager.initialize_paths()
 
@@ -672,7 +686,12 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn:
     contractpath = os.path.join(targetpath, "chc_contracts")
 
     capp = CApplication(
-        projectpath, projectname, targetpath, contractpath, singlefile=True)
+        projectpath,
+        projectname,
+        targetpath,
+        contractpath,
+        singlefile=True,
+        keep_system_includes=keep_system_includes)
 
     capp.initialize_single_file(cfilename)
     cfile = capp.get_cfile()
@@ -695,7 +714,12 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn:
     chklogger.logger.info("cfile analyze completed")
 
     capp = CApplication(
-        projectpath, projectname, targetpath, contractpath, singlefile=True)
+        projectpath,
+        projectname,
+        targetpath,
+        contractpath,
+        singlefile=True,
+        keep_system_includes=keep_system_includes)
     capp.initialize_single_file(cfilename)
     cfile = capp.get_cfile()
 

chc/cmdline/c_project/cprojectutil.py

@@ -68,7 +68,7 @@
 
 def print_error(m: str) -> None:
     sys.stderr.write(("*" * 80) + "\n")
-    sys.stderr.write(m + "\n")
+    sys.stderr.write("F:" + m + "\n")
     sys.stderr.write(("*" * 80) + "\n")
 
 
@@ -110,6 +110,7 @@ def cproject_parse_project(args: argparse.Namespace) -> NoReturn:
     projectpath: str = args.path
     projectname: str = args.projectname
     opttgtpath: Optional[str] = args.tgtpath
+    keep_system_includes: bool = args.keep_system_includes
     loglevel: str = args.loglevel
     logfilename: Optional[str] = args.logfilename
     logfilemode: str = args.logfilemode
@@ -156,7 +157,8 @@ def cproject_parse_project(args: argparse.Namespace) -> NoReturn:
         print_error("The compile_commands.json file was found empty")
         exit(1)
 
-    parsemanager = ParseManager(projectpath, projectname, targetpath)
+    parsemanager = ParseManager(
+        projectpath, projectname, targetpath, keep_system_includes=keep_system_includes)
     parsemanager.remove_semantics()
     parsemanager.initialize_paths()
     parsemanager.parse_with_ccommands(compilecommands, copyfiles=True)
@@ -423,6 +425,7 @@ def cproject_analyze_project(args: argparse.Namespace) -> NoReturn:
     # arguments
     tgtpath: str = args.tgtpath
     projectname: str = args.projectname
+    keep_system_includes: bool = args.keep_system_includes
     maxprocesses: int = args.maxprocesses
     loglevel: str = args.loglevel
     logfilename: Optional[str] = args.logfilename
@@ -458,6 +461,7 @@ def cproject_analyze_project(args: argparse.Namespace) -> NoReturn:
         projectname,
         targetpath,
         contractpath,
+        keep_system_includes=keep_system_includes,
         excludefiles=excludefiles)
 
     def save_xrefs(f: "CFile") -> None:
@@ -475,9 +479,10 @@ def save_xrefs(f: "CFile") -> None:
         projectname,
         targetpath,
         contractpath,
+        keep_system_includes=keep_system_includes,
         excludefiles=excludefiles)
 
-    am = AnalysisManager(capp, verbose=True)
+    am = AnalysisManager(capp, verbose=True, keep_system_includes=keep_system_includes)
 
     with timing("analysis"):
 
@@ -490,13 +495,13 @@ def save_xrefs(f: "CFile") -> None:
             exit(1)
 
         for i in range(1):
-            am.generate_and_check_app("llrvisp", processes=maxprocesses)
+            am.generate_and_check_app("visp", processes=maxprocesses)
             capp.reinitialize_tables()
             capp.update_spos()
 
         for i in range(5):
             capp.update_spos()
-            am.generate_and_check_app("llrvisp", processes=maxprocesses)
+            am.generate_and_check_app("visp", processes=maxprocesses)
             capp.reinitialize_tables()
 
     timestamp = os.stat(UF.get_cchpath(targetpath, projectname)).st_ctime