terminate parsing when encountering an error

Author: sipma

chc/app/CGlobalDeclarations.py

@@ -322,13 +322,19 @@ def cleanup(self, checkpoint: int, ckey: int, gckey: int) -> None:
             self.incompatibles[ckey] = set([])
         self.incompatibles[ckey].add(gckey)
         self.reset_conjectures()
+        keystoberemoved: List[int] = []
         for k in self.compinfo_names.keys():
             if k >= checkpoint:
-                self.compinfo_names.pop(k)
+                keystoberemoved.append(k)
+        for k in keystoberemoved:
+            self.compinfo_names.pop(k)
+        fskeystoberemoved: List[Tuple[str, int]] = []
         for fs in self.fieldstrings.keys():
             for gckey in self.fieldstrings[fs]:
                 if gckey >= checkpoint:
-                    self.fieldstrings[fs].remove(gckey)
+                    fskeystoberemoved.append((fs, gckey))
+        for (fs, gckey) in fskeystoberemoved:
+            self.fieldstrings[fs].remove(gckey)
 
     def get_state(self) -> str:
         lines = []

chc/cmdline/AnalysisManager.py

@@ -212,6 +212,7 @@ def create_file_primary_proofobligations(
             chklogger.logger.info(
                 "Ocaml analyzer is called with %s", str(cmd))
             if self.verbose:
+                print(str(cmd))
                 result = subprocess.call(
                     cmd, cwd=self.targetpath, stderr=subprocess.STDOUT)
                 print("\nResult: " + str(result))

chc/cmdline/ParseManager.py

@@ -453,10 +453,16 @@ def parse_with_ccommands(
                 print("\nRun the parser: " + str(command) + "\n")
             sys.stdout.flush()
             if self.verbose:
-                subprocess.call(command)
+                returncode = subprocess.call(command)
                 print("\n" + ("-" * 80) + "\n\n")
             else:
-                subprocess.call(command, stdout=open(os.devnull, "w"))
+                returncopde = (
+                    subprocess.call(command, stdout=open(os.devnull, "w")))
+            if returncode == 1:
+                print("\n" + ("*" * 80))
+                print("Parsing error in " + cfilename)
+                print("*" * 80)
+                break
 
         if self.verbose:
             print("\n\nCollect c files")

chc/cmdline/c_file/cfileutil.py

@@ -486,7 +486,7 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn:
 
     def pofilter(po: "CFunctionPO") -> bool:
         if copen:
-            return not po.is_closed
+            return (po.is_violated or (not po.is_closed))
         else:
             return True
 

chc/reporting/ProofObligations.py

@@ -468,8 +468,14 @@ def function_code_tostring(
     ppos = fn.get_ppos()
     # ppos = [x for x in ppos if pofilter(x)]
     spos = fn.get_spos()
-    fnstartlinenr = fn.get_line_number()
-    if fnstartlinenr is None:
+    if fn.has_line_number():
+        fnstartlinenr = fn.get_line_number()
+        fnstartline = fn.cfile.get_source_line(fnstartlinenr)
+        lines.append("\nFunction " + fn.name)
+        lines.append("-" * 80)
+        lines.append(fnstartline.strip())
+        fd = FunctionDisplay(fn, True)
+    else:
         lines.append(
             "\nFunction "
             + fn.name
@@ -478,12 +484,7 @@ def function_code_tostring(
             + ")"
         )
         fd = FunctionDisplay(fn, False)
-    else:
-        fnstartline = fn.cfile.get_source_line(fnstartlinenr)
-        lines.append("\nFunction " + fn.name)
-        lines.append("-" * 80)
-        lines.append(fnstartline.strip())
-        fd = FunctionDisplay(fn, True)
+
     if showpreamble:
         lines.append("-" * 80)
         lines.append(str(fn.api))
@@ -499,6 +500,7 @@ def function_code_tostring(
         lines.append(
             fd.pos_on_code_tostring(spos, pofilter=pofilter, showinvs=showinvs)
         )
+        lines.append("-" * 80)
     return "\n".join(lines)
 
 

chc/util/IndexedTable.py

@@ -241,9 +241,12 @@ def reset_to_checkpoint(self) -> int:
             if i in self.reserved:
                 continue
             self.indextable.pop(i)
+        toberemoved: List[int] = []
         for k in self.keytable.keys():
             if self.keytable[k] >= cp:
-                self.keytable.pop(k)
+                toberemoved.append(k)
+        for k in toberemoved:
+            self.keytable.pop(k)
         self.checkpoint = None
         self.reserved = []
         self.next = cp