Skip to content

Commit 728c20d

Browse files
committed
PROOF: change representation for rejection reason
1 parent 5d9f0f2 commit 728c20d

9 files changed

Lines changed: 230 additions & 16 deletions

File tree

chc/app/CFunction.py

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -307,7 +307,8 @@ def analysis_digests(self) -> CFunctionAnalysisDigests:
307307
self.cfilename,
308308
self.name)
309309
if adnode is None:
310-
print("DEBUG: No adg file found")
310+
chklogger.logger.warning(
311+
"No adg file encountered for function %s", self.name)
311312
adgnode = None
312313
# raise UF.CHCError(self.xmsg("adg file not found"))
313314
else:

chc/cmdline/AnalysisManager.py

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -282,7 +282,7 @@ def f(cfile: "CFile") -> None:
282282

283283
def f(cfile: "CFile") -> None:
284284
self.create_file_primary_proofobligations(
285-
cfile.cfilename, cfile.cfilepath)
285+
cfile.cfilename, cfile.cfilepath, po_cmd=po_cmd)
286286

287287
self.capp.iter_files(f)
288288

chc/cmdline/c_project/cprojectutil.py

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -533,10 +533,20 @@ def cproject_report(args: argparse.Namespace) -> NoReturn:
533533
projectname: str = args.projectname
534534
canalysis: str = args.analysis
535535
verbose: bool = args.verbose
536+
loglevel: str = args.loglevel
537+
logfilename: Optional[str] = args.logfilename
538+
logfilemode: str = args.logfilemode
536539

537540
targetpath = os.path.abspath(tgtpath)
538541
projectpath = targetpath
539542

543+
set_logging(
544+
loglevel,
545+
targetpath,
546+
logfilename=logfilename,
547+
mode=logfilemode,
548+
msg="c-project report invoked")
549+
540550
statsresult = UF.read_project_summary_results(targetpath, projectname)
541551
if statsresult is not None:
542552
print(RP.project_proofobligation_stats_dict_to_string(statsresult))

chc/cmdline/chkc

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1592,6 +1592,20 @@ def parse() -> argparse.Namespace:
15921592
cprojectreport.add_argument(
15931593
"--verbose", "-v",
15941594
action="store_true")
1595+
cprojectreport.add_argument(
1596+
"--loglevel", "-log",
1597+
choices=UL.LogLevel.options(),
1598+
default="NONE",
1599+
help="activate logging with given level (default to stderr)")
1600+
cprojectreport.add_argument(
1601+
"--logfilename",
1602+
help="name of file to write log messages")
1603+
cprojectreport.add_argument(
1604+
"--logfilemode",
1605+
choices=["a", "w"],
1606+
default="a",
1607+
help="file mode for log file: append (a, default), or write (w)")
1608+
15951609
cprojectreport.set_defaults(func=P.cproject_report)
15961610

15971611
# --- report-file

chc/proof/CFunPODictionary.py

Lines changed: 12 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
#
77
# Copyright (c) 2017-2020 Kestrel Technology LLC
88
# Copyright (c) 2020-2022 Henny B. Sipma
9-
# Copyright (c) 2023-2024 Aarno Labs LLC
9+
# Copyright (c) 2023-2025 Aarno Labs LLC
1010
#
1111
# Permission is hereby granted, free of charge, to any person obtaining a copy
1212
# of this software and associated documentation files (the "Software"), to deal
@@ -36,6 +36,7 @@
3636
from typing import Callable, Dict, List, Mapping, TYPE_CHECKING
3737

3838
from chc.proof.AssumptionType import AssumptionType
39+
from chc.proof.OutputParameterRejectionReason import OutputParameterRejectionReason
3940
from chc.proof.OutputParameterStatus import OutputParameterStatus
4041
from chc.proof.CFunPODictionaryRecord import podregistry
4142
from chc.proof.PPOType import PPOType
@@ -67,12 +68,15 @@ def __init__(
6768
cfun: "CFunction",
6869
xnode: ET.Element) -> None:
6970
self._cfun = cfun
71+
self.output_parameter_rejection_reason_table = IndexedTable(
72+
"output-parameter-rejection-reason-table")
7073
self.output_parameter_status_table = IndexedTable(
7174
"output-parameter-status-table")
7275
self.assumption_type_table = IndexedTable("assumption-table")
7376
self.ppo_type_table = IndexedTable("ppo-type-table")
7477
self.spo_type_table = IndexedTable("spo-type-table")
7578
self.tables = [
79+
self.output_parameter_rejection_reason_table,
7680
self.output_parameter_status_table,
7781
self.assumption_type_table,
7882
self.ppo_type_table,
@@ -106,6 +110,13 @@ def interfacedictionary(self) -> "InterfaceDictionary":
106110

107111
# ------------------------ Retrieve items from dictionary ----------------
108112

113+
def get_output_parameter_rejection_reason(
114+
self, ix: int) -> OutputParameterRejectionReason:
115+
return podregistry.mk_instance(
116+
self,
117+
self.output_parameter_rejection_reason_table.retrieve(ix),
118+
OutputParameterRejectionReason)
119+
109120
def get_output_parameter_status(self, ix: int) -> OutputParameterStatus:
110121
return podregistry.mk_instance(
111122
self,

chc/proof/CFunctionAnalysisDigest.py

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@
3232
from chc.proof.CandidateOutputParameter import CandidateOutputParameter
3333
from chc.proof.OutputParameterCalleeCallsite import OutputParameterCalleeCallsite
3434

35+
from chc.util.loggingutil import chklogger
3536

3637
if TYPE_CHECKING:
3738
from chc.app.CFile import CFile
@@ -119,7 +120,7 @@ def digests(self) -> List[CFunctionAnalysisDigest]:
119120
self.cfun, xdigest)
120121
self._digests.append(digest)
121122
else:
122-
print("DEBUG: xnode is none")
123+
chklogger.logger.warning("Adg xnode is None")
123124
return self._digests
124125

125126
def __str__(self) -> str:
Lines changed: 172 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,172 @@
1+
# ------------------------------------------------------------------------------
2+
# CodeHawk C Analyzer
3+
# Author: Henny Sipma
4+
# ------------------------------------------------------------------------------
5+
# The MIT License (MIT)
6+
#
7+
# Copyright (c) 2025 Aarno Labs LLC
8+
#
9+
# Permission is hereby granted, free of charge, to any person obtaining a copy
10+
# of this software and associated documentation files (the "Software"), to deal
11+
# in the Software without restriction, including without limitation the rights
12+
# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
13+
# copies of the Software, and to permit persons to whom the Software is
14+
# furnished to do so, subject to the following conditions:
15+
#
16+
# The above copyright notice and this permission notice shall be included in all
17+
# copies or substantial portions of the Software.
18+
#
19+
# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
20+
# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
21+
# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
22+
# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
23+
# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
24+
# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
25+
# SOFTWARE.
26+
# ------------------------------------------------------------------------------
27+
28+
from typing import List, TYPE_CHECKING
29+
30+
from chc.proof.CFunPODictionaryRecord import CFunPODictionaryRecord, podregistry
31+
32+
33+
from chc.util.IndexedTable import IndexedTableValue
34+
35+
36+
if TYPE_CHECKING:
37+
from chc.app.CCompInfo import CCompInfo
38+
from chc.app.CDictionary import CDictionary
39+
from chc.app.CTyp import CTyp
40+
from chc.proof.CFunPODictionary import CFunPODictionary
41+
42+
43+
class OutputParameterRejectionReason(CFunPODictionaryRecord):
44+
45+
def __init__(
46+
self, pod: "CFunPODictionary", ixval: IndexedTableValue
47+
) -> None:
48+
CFunPODictionaryRecord.__init__(self, pod, ixval)
49+
50+
51+
@podregistry.register_tag("a", OutputParameterRejectionReason)
52+
class OutputParameterRejectionReasonArrayStruct(OutputParameterRejectionReason):
53+
54+
def __init__(
55+
self, pod: "CFunPODictionary", ixval: IndexedTableValue
56+
) -> None:
57+
OutputParameterRejectionReason.__init__(self, pod, ixval)
58+
59+
@property
60+
def compinfo(self) -> "CCompInfo":
61+
return self.cdecls.get_compinfo(self.args[0])
62+
63+
def __str__(self) -> str:
64+
return "Struct with embedded array: " + str(self.compinfo)
65+
66+
67+
@podregistry.register_tag("at", OutputParameterRejectionReason)
68+
class OutputParameterRejectionReasonArrayType(OutputParameterRejectionReason):
69+
70+
def __init__(
71+
self, pod: "CFunPODictionary", ixval: IndexedTableValue
72+
) -> None:
73+
OutputParameterRejectionReason.__init__(self, pod, ixval)
74+
75+
@property
76+
def typ(self) -> "CTyp":
77+
return self.cdictionary.get_typ(self.args[0])
78+
79+
def __str__(self) -> str:
80+
return "rray type: " + str(self.typ)
81+
82+
83+
@podregistry.register_tag("c", OutputParameterRejectionReason)
84+
class OutputParameterRejectionReasonConstQualifier(OutputParameterRejectionReason):
85+
86+
def __init__(
87+
self, pod: "CFunPODictionary", ixval: IndexedTableValue
88+
) -> None:
89+
OutputParameterRejectionReason.__init__(self, pod, ixval)
90+
91+
@property
92+
def typ(self) -> "CTyp":
93+
return self.cdictionary.get_typ(self.args[0])
94+
95+
def __str__(self) -> str:
96+
return "Const qualifier: " + str(self.typ)
97+
98+
99+
@podregistry.register_tag("o", OutputParameterRejectionReason)
100+
class OutputParameterRejectionReasonOtherReason(OutputParameterRejectionReason):
101+
102+
def __init__(
103+
self, pod: "CFunPODictionary", ixval: IndexedTableValue
104+
) -> None:
105+
OutputParameterRejectionReason.__init__(self, pod, ixval)
106+
107+
@property
108+
def reason(self) -> str:
109+
return self.cdictionary.get_string(self.args[0])
110+
111+
def __str__(self) -> str:
112+
return "Other: " + str(self.reason)
113+
114+
115+
@podregistry.register_tag("p", OutputParameterRejectionReason)
116+
class OutputParameterRejectionReasonPointerPointer(OutputParameterRejectionReason):
117+
118+
def __init__(
119+
self, pod: "CFunPODictionary", ixval: IndexedTableValue
120+
) -> None:
121+
OutputParameterRejectionReason.__init__(self, pod, ixval)
122+
123+
@property
124+
def typ(self) -> "CTyp":
125+
return self.cdictionary.get_typ(self.args[0])
126+
127+
def __str__(self) -> str:
128+
return "Pointer to pointer: " + str(self.typ)
129+
130+
131+
@podregistry.register_tag("r", OutputParameterRejectionReason)
132+
class OutputParameterRejectionReasonParameterRead(OutputParameterRejectionReason):
133+
134+
def __init__(
135+
self, pod: "CFunPODictionary", ixval: IndexedTableValue
136+
) -> None:
137+
OutputParameterRejectionReason.__init__(self, pod, ixval)
138+
139+
@property
140+
def linenumber(self) -> int:
141+
return self.args[0]
142+
143+
def __str__(self) -> str:
144+
return "Parameter is read at line " + str(self.linenumber)
145+
146+
147+
@podregistry.register_tag("s", OutputParameterRejectionReason)
148+
class OutputParameterRejectionReasonSystemStruct(OutputParameterRejectionReason):
149+
150+
def __init__(
151+
self, pod: "CFunPODictionary", ixval: IndexedTableValue
152+
) -> None:
153+
OutputParameterRejectionReason.__init__(self, pod, ixval)
154+
155+
@property
156+
def compinfo(self) -> "CCompInfo":
157+
return self.cdecls.get_compinfo(self.args[0])
158+
159+
def __str__(self) -> str:
160+
return "Target type is a system struct: " + str(self.compinfo)
161+
162+
163+
@podregistry.register_tag("v", OutputParameterRejectionReason)
164+
class OutputParameterRejectionReasonVoidPointer(OutputParameterRejectionReason):
165+
166+
def __init__(
167+
self, pod: "CFunPODictionary", ixval: IndexedTableValue
168+
) -> None:
169+
OutputParameterRejectionReason.__init__(self, pod, ixval)
170+
171+
def __str__(self) -> str:
172+
return "Void pointer"

chc/proof/OutputParameterStatus.py

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@
3636
if TYPE_CHECKING:
3737
from chc.app.CDictionary import CDictionary
3838
from chc.proof.CFunPODictionary import CFunPODictionary
39+
from chc.proof.OutputParameterRejectionReason import OutputParameterRejectionReason
3940

4041

4142
class OutputParameterStatus(CFunPODictionaryRecord):
@@ -103,11 +104,11 @@ def is_rejected(self) -> bool:
103104
return True
104105

105106
@property
106-
def reason(self) -> List[str]:
107-
return [self.cdictionary.get_string(arg) for arg in self.args]
107+
def reasons(self) -> List["OutputParameterRejectionReason"]:
108+
return [self.pod.get_output_parameter_rejection_reason(arg) for arg in self.args]
108109

109110
def __str__(self) -> str:
110-
return "Rejected: " + "; ".join(self.reason)
111+
return "Rejected: " + "; ".join(str(reason) for reason in self.reasons)
111112

112113

113114
@podregistry.register_tag("w", OutputParameterStatus)
@@ -119,7 +120,7 @@ def __init__(
119120
OutputParameterStatus.__init__(self, pod, ixval)
120121

121122
@property
122-
def is_viable(self) -> bool:
123+
def is_written(self) -> bool:
123124
return True
124125

125126
def __str__(self) -> str:

chc/reporting/ProofObligations.py

Lines changed: 12 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -663,16 +663,20 @@ def project_proofobligation_stats_dict_to_string(
663663
pporesults = stats_dict["fileresults"]["ppos"]
664664
sporesults = stats_dict["fileresults"]["spos"]
665665

666-
rhlen = max([len(x) for x in pporesults])
667-
lines.append(
668-
proofobligation_stats_tostring(
669-
pporesults, sporesults, rhlen=rhlen, header1="c files"))
666+
if len(pporesults) > 0:
667+
rhlen = max([len(x) for x in pporesults])
668+
lines.append(
669+
proofobligation_stats_tostring(
670+
pporesults, sporesults, rhlen=rhlen, header1="c files"))
670671

671-
lines.append("\n\nProof Obligation Statistics")
672+
lines.append("\n\nProof Obligation Statistics")
672673

673-
tagpporesults = stats_dict["tagresults"]["ppos"]
674-
tagsporesults = stats_dict["tagresults"]["spos"]
675-
lines.append(proofobligation_stats_tostring(tagpporesults, tagsporesults))
674+
tagpporesults = stats_dict["tagresults"]["ppos"]
675+
tagsporesults = stats_dict["tagresults"]["spos"]
676+
lines.append(proofobligation_stats_tostring(tagpporesults, tagsporesults))
677+
678+
else:
679+
lines.append("Zero primary proof obligations")
676680

677681
return "\n".join(lines)
678682

0 commit comments

Comments
 (0)