Merge branch 'master' into invariantquery

Author: sipma

README.md

@@ -4,33 +4,28 @@ Sound Static Analysis of C for Memory Safety (Undefined Behavior)
 ### Quick start
 
 The CodeHawk-C Analyzer consists of two parts:
-- A python front end (this repository) through which all user interaction
+- A Python front end (this repository) through which all user interaction
   is performed, and
-- An ocaml abstract-interpretation engine that powers the analysis.
+- An OCaml abstract-interpretation engine that powers the analysis.
 
-To use the CodeHawk-C Analyzer first clone or download the ocaml application
+To use the CodeHawk-C Analyzer first clone or download the OCaml application
 from
 ```
 https://github.com/static-analysis-engineering/codehawk
 ```
-and build according to the accompanying instructions given there.
-Then copy the following files from that build:
-```
-codehawk/CodeHawk/CHC/cchcil/parseFile
-codehawk/CodeHawk/CHC/cchcmdline/canalyzer
-```
-to the following location in this repository:
-```
-CodeHawk-C/chc/bin/linux/
-```
-or
-```
-CodeHawk-C/chc/bin/macOS
-```
-depending on the platform where the executables were built.
-Alternatively, you can edit the path to these two executables directly
-in chc/util/Config.py or chc/util/ConfigLocal.py, so there is no need
-to copy them or update them with each new version of the ocaml analyzer.
+and build with `dune` according to the accompanying instructions given there.
+
+You can either:
+- Copy `chc/util/ConfigLocal.template` to `chc/util/ConfigLocal.py`
+in this repository, and edit the latter file to set the paths for
+`config.canalyzer` and `config.cparser` to the `dune`-built binaries,
+which should be in `your-path-to-codehawk/CodeHawk/_build/install/default/bin/`.
+This allows CodeHawk-C to automatically use newly-built versions of the
+OCaml analyzer.
+- Or, you can copy the `canalyzer` and `parseFile` binaries from that location
+into `chc/bin/linux/` or `chc/bin/macOS` within this repository.
+To allow CodeHawk-C to use newly-built versions of the OCaml analyzer,
+you will have to re-copy the binaries after every build.
 
 Set the python path and path:
 ```
@@ -47,8 +42,8 @@ which should show something like:
 Analyzer configuration:
 -----------------------
   platform : linux
-  parser   : /home/user/codehawk/CodeHawk/CHC/cchcil/parseFile (found)
-  analyzer : /home/user/codehawk/CodeHawk/CHC/cchcmdline/canalyzer (found)
+  parser   : /home/user/codehawk/CodeHawk/_build/install/default/bin/parseFile (found)
+  analyzer : /home/user/codehawk/CodeHawk/_build/install/default/bin/canalyzer (found)
 
   summaries: /home/user/CodeHawk-C/chc/summaries/cchsummaries.jar (found)
 ```
@@ -60,9 +55,9 @@ Interaction with the analyzer is primarily through the command-line interpreter
    ```
    > chkc c-file parse <filename>
    > chkc c-file analyze <filename>
-   > chkc c-file report-file <filename>
+   > chkc c-file report <filename>
    ```
-   The first command preprocesses the file with gcc; the preprocessed file (.i file)
+   The first command preprocesses the file with `cc`; the preprocessed file (.i file)
    is then parsed with **parseFile** (a wrapper for goblint-cil,
    https://opam.ocaml.org/packages/goblint-cil/).
    The second command analyzes the parsed artifacts, and the third command (and

chc/app/CPrettyPrinter.py

@@ -310,12 +310,12 @@ def visit_funarg(self, funarg: CT.CFunArg) -> None:
                     self.funtypptr_with_name(ptx, funarg.name)
                     return
 
-            if (
-                    argtyp.attributes.length > 0
-                    and argtyp.attributes.attributes[0].name == "arraylen"):
-                self.ptrarg_with_attribute_length(
-                    ptargtyp, argtyp.attributes.attributes[0], funarg.name)
-                return
+            # if (
+            #        argtyp.attributes.length > 0
+            #         and argtyp.attributes.attributes[0].name == "arraylen"):
+            #    self.ptrarg_with_attribute_length(
+            #        ptargtyp, argtyp.attributes.attributes[0], funarg.name)
+            #    return
 
         funarg.typ.accept(self)
         self.ccode.write(" ")

chc/app/CTyp.py

@@ -184,6 +184,10 @@ def is_pointer(self) -> bool:
     def is_struct(self) -> bool:
         return False
 
+    @property
+    def is_union(self) -> bool:
+        return False
+
     @property
     def is_void(self) -> bool:
         return False
@@ -388,6 +392,10 @@ def name(self) -> str:
     def is_struct(self) -> bool:
         return self.compinfo.is_struct
 
+    @property
+    def is_union(self) -> bool:
+        return not self.compinfo.is_struct
+
     def accept(self, visitor: "CVisitor") -> None:
         visitor.visit_comptyp(self)
 

chc/cmdline/ParseManager.py

@@ -221,32 +221,32 @@ def save_semantics(self) -> None:
             )
         os.chdir(cwd)
 
-    def preprocess_file_with_gcc(
+    def preprocess_file_with_cc(
             self,
             cfilename: str,
             copyfiles: bool = True,
             moreoptions: List[str] = []) -> str:
-        """Invoke gcc preprocessor on c source file.
+        """Invoke C preprocessor on c source file.
 
         Args:
             cfilename: c source code filename relative to cpath
             moreoptions: list of additional options to be given to the
                            preprocessor
 
         Effects:
-            invokes the gcc preprocessor on the c source file and optionally
+            invokes the C preprocessor on the c source file and optionally
             copies the original source file and the generated .i file to the
-            tgtpath/sourcefiles directory
+            tgtpath/sourcefiles directory.
         """
 
-        chklogger.logger.info("Preprocess file with gcc: %s", cfilename)
+        chklogger.logger.info("Preprocess file with cc: %s", cfilename)
         cwd = os.getcwd()
         mac = self.config.platform == "mac"
         ifilename = cfilename[:-1] + "i"
         macoptions = [
             "-U___BLOCKS___", "-D_DARWIN_C_SOURCE", "-D_FORTIFY_SOURCE=0"]
         cmd = [
-            "gcc",
+            "cc",
             "-fno-inline",
             "-fno-builtin",
             "-E",
@@ -498,7 +498,7 @@ def parse_ifiles(self, copyfiles: bool = True) -> None:
         targetfiles.save_xml_file(self.analysisresultspath)
 
     def parse_cfiles(self, copyfiles: bool = True) -> None:
-        """Preprocess (with gcc) and run the CodeHawk C parser on all .c
+        """Preprocess and run the CodeHawk C parser on all .c
         files in the directory."""
 
         os.chdir(self.projectpath)
@@ -509,7 +509,7 @@ def parse_cfiles(self, copyfiles: bool = True) -> None:
                     fname = self.normalize_filename(os.path.join(d, fname))
                     if fname.startswith("semantics"):
                         continue
-                    ifilename = self.preprocess_file_with_gcc(fname, copyfiles)
+                    ifilename = self.preprocess_file_with_cc(fname, copyfiles)
                     self.parse_ifile(ifilename)
                     targetfiles.add_file(self.normalize_filename(fname))
         targetfiles.save_xml_file(self.analysisresultspath)
@@ -585,7 +585,7 @@ def save_xml_file(self, tgtpath: str) -> None:
 
 if __name__ == "__main__":
 
-    # preprocess and parse single files with gcc
+    # preprocess and parse single files with cc
     thisdir = os.path.dirname(os.path.abspath(__file__))
     topdir = os.path.dirname(os.path.dirname(thisdir))
     testsdir = os.path.join(topdir, "tests")
@@ -594,5 +594,5 @@ def save_xml_file(self, tgtpath: str) -> None:
     pm = ParseManager(id115dir, "kendra115", id115dir)
     pm.initialize_paths()
     for f in ["id115.c", "id116.c", "id117.c", "id118.c"]:
-        ifilename = pm.preprocess_file_with_gcc(f)
+        ifilename = pm.preprocess_file_with_cc(f)
         pm.parse_ifile(ifilename)