diff --git a/chc/app/CFile.py b/chc/app/CFile.py index bd13a46..b154cb9 100644 --- a/chc/app/CFile.py +++ b/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]]: diff --git a/chc/app/CFunction.py b/chc/app/CFunction.py index 8d0b93d..e7799cf 100644 --- a/chc/app/CFunction.py +++ b/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()