diff --git a/chc/cmdline/c_file/cfileutil.py b/chc/cmdline/c_file/cfileutil.py index d385fac..0253fdc 100644 --- a/chc/cmdline/c_file/cfileutil.py +++ b/chc/cmdline/c_file/cfileutil.py @@ -285,6 +285,7 @@ def cfile_report_file(args: argparse.Namespace) -> NoReturn: xcfilename: str = args.filename opttgtpath: Optional[str] = args.tgtpath cshowcode: bool = args.showcode + cshowinvariants: bool = args.showinvariants cfunctions: Optional[List[str]] = args.functions copen: bool = args.open jsonoutput: bool = args.json @@ -334,7 +335,8 @@ def pofilter(po: "CFunctionPO") -> bool: if cfunctions is None: if cshowcode: - print(RP.file_code_tostring(cfile, pofilter=pofilter)) + print(RP.file_code_tostring( + cfile, pofilter=pofilter, showinvs=cshowinvariants)) print(RP.file_proofobligation_stats_tostring(cfile)) exit(0) @@ -356,6 +358,7 @@ def cfile_run_file(args: argparse.Namespace) -> NoReturn: opttgtpath: Optional[str] = args.tgtpath cshowcode: bool = args.showcode copen: bool = args.open + cshowinvariants: bool = args.showinvariants jsonoutput: bool = args.json outputfile: Optional[str] = args.output verbose: bool = args.verbose @@ -492,7 +495,8 @@ def pofilter(po: "CFunctionPO") -> bool: return True if cshowcode: - print(RP.file_code_tostring(cfile, pofilter=pofilter)) + print(RP.file_code_tostring( + cfile, pofilter=pofilter, showinvs=cshowinvariants)) print(RP.file_proofobligation_stats_tostring(cfile)) exit(0) diff --git a/chc/cmdline/chkc b/chc/cmdline/chkc index 1e25f4a..67a3651 100755 --- a/chc/cmdline/chkc +++ b/chc/cmdline/chkc @@ -703,6 +703,10 @@ def parse() -> argparse.Namespace: "--open", action="store_true", help="only show open proof obligations") + cfilereport.add_argument( + "--showinvariants", + action="store_true", + help="show location invariants on the code") cfilereport.add_argument( "--json", action="store_true", @@ -742,6 +746,10 @@ def parse() -> argparse.Namespace: "--open", action="store_true", help="only show open proof obligations") + cfilerun.add_argument( + "--showinvariants", + action="store_true", + help="show location invariants on the code") cfilerun.add_argument( "--json", action="store_true", diff --git a/chc/summaries/cchsummaries.jar b/chc/summaries/cchsummaries.jar index 75aa9f5..a73d685 100644 Binary files a/chc/summaries/cchsummaries.jar and b/chc/summaries/cchsummaries.jar differ