add error handling

chc/app/CFile.py

@@ -370,7 +370,11 @@ def collect_post_assumes(self) -> None:
         """Collect callsite postconditions from callee's contracts and add as assume."""
 
         for fn in self.get_functions():
-            fn.collect_post_assumes()
+            try:
+                fn.collect_post_assumes()
+            except UF.CHCError as e:
+                chklogger.logger.error(str(e))
+                continue
 
         self.save_interface_dictionary()
         self.save_predicate_dictionary()
@@ -444,7 +448,11 @@ def get_functions(self) -> Iterable[CFunction]:
 
     def iter_functions(self, f: Callable[[CFunction], None]) -> None:
         for fn in self.get_functions():
-            f(fn)
+            try:
+                f(fn)
+            except UF.CHCError as e:
+                chklogger.logger.error(str(e))
+                continue
 
     def get_compinfos(self) -> List["CCompInfo"]:
         return self.cfileglobals.get_compinfos()
@@ -482,16 +490,28 @@ def get_callinstrs(self) -> List["CCallInstr"]:
 
     def reload_spos(self) -> None:
         for fn in self.get_functions():
-            fn.reload_spos()
+            try:
+                fn.reload_spos()
+            except UF.CHCError as e:
+                chklogger.logger.error(e.msg)
+                continue
 
     def reload_ppos(self) -> None:
         for fn in self.get_functions():
-            fn.reload_ppos()
+            try:
+                fn.reload_ppos()
+            except UF.CHCError as e:
+                chklogger.logger.error(e.msg)
+                continue
 
     def get_ppos(self) -> List[CFunctionPO]:
         result: List[CFunctionPO] = []
         for fn in self.get_functions():
-            result.extend(fn.get_ppos())
+            try:
+                result.extend(fn.get_ppos())
+            except UF.CHCError as e:
+                chklogger.logger.error(str(e))
+                continue
         return result
 
     def get_open_ppos(self) -> List[CFunctionPO]:
@@ -521,7 +541,11 @@ def get_ppos_delegated(self) -> List[CFunctionPO]:
     def get_spos(self) -> List[CFunctionPO]:
         result: List[CFunctionPO] = []
         for fn in self.get_functions():
-            result.extend(fn.get_spos())
+            try:
+                result.extend(fn.get_spos())
+            except UF.CHCError as e:
+                chklogger.logger.error(str(e))
+                continue
         return result
 
     def get_line_ppos(self) -> Dict[int, Dict[str, Any]]:

chc/app/CFunction.py

@@ -446,7 +446,10 @@ def get_contract_condition_violations(self) -> List[Tuple[str, str]]:
     def update_spos(self) -> None:
         if self.selfignore():
             return
-        self.proofs.update_spos()
+        try:
+            self.proofs.update_spos()
+        except UF.CHCError as e:
+            chklogger.logger.error(str(e))
 
     def collect_post_assumes(self) -> None:
         """For all call sites collect postconditions from callee's contracts and add as assume."""
@@ -479,19 +482,25 @@ def collect_post(self) -> None:
                         cfuncontract.add_postrequest(tgtpostcondition)
 
     def save_spos(self) -> None:
-        self.proofs.save_spos()
+        try:
+            self.proofs.save_spos()
+        except UF.CHCError as e:
+            chklogger.logger.error(str(e))
 
     def save_pod(self) -> None:
         cnode = ET.Element("function")
         cnode.set("name", self.name)
-        self.podictionary.write_xml(cnode)
-        UF.save_pod_file(
-            self.targetpath,
-            self.projectname,
-            self.cfilepath,
-            self.cfilename,
-            self.name,
-            cnode)
+        try:
+            self.podictionary.write_xml(cnode)
+            UF.save_pod_file(
+                self.targetpath,
+                self.projectname,
+                self.cfilepath,
+                self.cfilename,
+                self.name,
+                cnode)
+        except UF.CHCError as e:
+            chklogger.logger.error(str(e))
 
     def reload_ppos(self) -> None:
         self.proofs.reload_ppos()