chc.reporting package
Utilities for creating text reports of analysis results.
Submodules
chc.reporting.ProofObligations module
- class chc.reporting.ProofObligations.FunctionDisplay(cfunction: CFunction, sourcecodeavailable: bool)[source]
Bases:
object- property cfile: CFile
- property cfinvd: CFunInvDictionary
- property cfunction: CFunction
- property fline: int
- pos_no_code_to_string(pos: Sequence[CFunctionPO], pofilter: Callable[[CFunctionPO], bool] = <function FunctionDisplay.<lambda>>) str[source]
- pos_on_code_tostring(pos: Sequence[CFunctionPO], pofilter: Callable[[CFunctionPO], bool] = <function FunctionDisplay.<lambda>>, showinvs: bool = False) str[source]
- property sourcecodeavailable: bool
- chc.reporting.ProofObligations.classifypo(po: CFunctionPO, d: Dict[str, int]) None[source]
Classify proof obligation wrt discharge method and update dictionary.
- Parameters
po – proof obligation (CFunctionPO)
d – dictionary, with discharge methods initialized (is updated)
- chc.reporting.ProofObligations.file_code_open_tostring(cfile: CFile, showinvs: bool = False) str[source]
- chc.reporting.ProofObligations.file_code_tostring(cfile: CFile, pofilter: Callable[[CFunctionPO], bool] = <function <lambda>>, showinvs: bool = False) str[source]
- chc.reporting.ProofObligations.file_proofobligation_stats_tostring(cfile: CFile, extradsmethods: List[str] = []) str[source]
- chc.reporting.ProofObligations.function_code_open_tostring(fn: CFunction, showinvs: bool = False) str[source]
- chc.reporting.ProofObligations.function_code_predicate_tostring(fn: CFunction, p: str, showinvs: bool = False) str[source]
- chc.reporting.ProofObligations.function_code_tostring(fn: CFunction, pofilter: Callable[[CFunctionPO], bool] = <function <lambda>>, showinvs: bool = False, showpreamble: bool = True) str[source]
- chc.reporting.ProofObligations.function_code_violation_tostring(fn: CFunction, showinvs: bool = False) str[source]
- chc.reporting.ProofObligations.function_pos_to_string(fn: CFunction, pofilter: Callable[[CFunctionPO], bool] = <function <lambda>>) str[source]
- chc.reporting.ProofObligations.function_proofobligation_stats_tostring(cfunction: CFunction, extradsmethods: List[str] = []) str[source]
- chc.reporting.ProofObligations.get_dsmethod_header(indent: int, dsmethods: List[str], header1: str = '') str[source]
- chc.reporting.ProofObligations.get_file_method_count(pos: Sequence[CFunctionPO], filefilter: Callable[[str], bool] = <function <lambda>>, extradsmethods: List[str] = []) Dict[str, Dict[str, int]][source]
Create file, discharge method count dictionary from proof obligation list.
- Parameters
pos – flat list of proof obligations (primary or secondary)
filefilter – predicate that specifies which c files to include
extradsmethods – additional discharge methods to include in classification
- Returns
dictionary that organizes proof obligations by file and discharge method
- chc.reporting.ProofObligations.get_function_method_count(pos: Sequence[CFunctionPO], extradsmethods: List[str] = []) Dict[str, Dict[str, int]][source]
Create function, discharge method count dictionary from proof obligation list.
- Parameters
pos – flat list of proof obligations (primary or supporting)
filefilter – predicate that specifies which c files to include
extradsmethods – additional discharge methods to include in classification
- Returns
dictionary that organizes proof obligations by function and discharge method
- chc.reporting.ProofObligations.get_method_count(pos: Sequence[CFunctionPO], filefilter: Callable[[str], bool] = <function <lambda>>, extradsmethods: List[str] = []) Dict[str, int][source]
Create dicharge method count dictionary from proof obligation list.
- Parameters
pos – flat list of proof obligations (primary or secondary)
filefilter – predicate that specifies which c files to include
extradsmethods – additional discharge methods to include in classification
- Returns
dictionary that organizes proof obligations by discharge method
- chc.reporting.ProofObligations.get_tag_method_count(pos: Sequence[CFunctionPO], filefilter: Callable[[str], bool] = <function <lambda>>, extradsmethods: List[str] = []) Dict[str, Dict[str, int]][source]
Create predicate tag, discharge method count dictionary.
- Parameters
pos – flat list of proof obligations (primary or secondary)
filefilter – predicate that specifies which c files to include
extradsmethods – additional discharge methods to include in classification
- Returns
dictionary that organizes proof obligations by predicate and discharge method
- chc.reporting.ProofObligations.get_totals_from_tagtotals(tagtotals: Dict[str, Dict[str, int]]) Dict[str, int][source]
- chc.reporting.ProofObligations.make_po_file_function_dict(pos: List[CFunctionPO], filefilter: Callable[[str], bool] = <function <lambda>>) Dict[str, Dict[str, List[CFunctionPO]]][source]
Create a file, function dictionary from a list of proof obligations.
- Parameters
pos – list of proof obligations (primary or supporting)
filefilter – predicate that specifies which c files to include
- Returns
dictionary that organizes the proof obligations by c file
- chc.reporting.ProofObligations.make_po_tag_dict(pos: List[CFunctionPO], pofilter: Callable[[CFunctionPO], bool] = <function <lambda>>) Dict[str, List[CFunctionPO]][source]
Create a predicate tag dictionary from a a list of proof obligations.
- Parameters
pos – list of proof obligations (primary or supporting)
pofilter – predicate that specifies which proof obligations to include
- Returns
dictionary that organizes the proof obligations by predicate tag
- chc.reporting.ProofObligations.project_proofobligation_stats_dict_to_string(stats_dict: Dict[str, Dict[str, Dict[str, Dict[str, int]]]]) str[source]
- chc.reporting.ProofObligations.project_proofobligation_stats_to_dict(capp: CApplication, filefilter: Callable[[str], bool] = <function <lambda>>, extradsmethods: List[str] = []) Dict[str, Any][source]
- chc.reporting.ProofObligations.project_proofobligation_stats_tostring(capp: CApplication, filefilter: Callable[[str], bool] = <function <lambda>>, extradsmethods: List[str] = []) str[source]
- chc.reporting.ProofObligations.proofobligation_stats_tostring(pporesults: Dict[str, Dict[str, int]], sporesults: Dict[str, Dict[str, int]], rhlen: int = 28, header1: str = '', extradsmethods: List[str] = []) str[source]
- chc.reporting.ProofObligations.row_method_count_tostring(d: Dict[str, Dict[str, int]], perc: bool = False, extradsmethods: List[str] = [], rhlen: int = 25, header1: str = '') str[source]
Display a dictionary with row-header - discharge method - count.
- Parameters
d – dictionary (row header -> discharge method -> count
perc – boolean that indicates whether to print discharge method percentages
extradsmethods – list of additional column headers (will be prepended)
rhlen – maximum length of the row header (default 25)
- Returns
table of discharge method counts represented as a string
- chc.reporting.ProofObligations.tag_file_function_pos_tostring(pos: List[CFunctionPO], filefilter: Callable[[str], bool] = <function <lambda>>, pofilter: Callable[[CFunctionPO], bool] = <function <lambda>>) str[source]