chc.proof.CproofDiagnostic module

Diagnostic messages related to an open proof obligation.

class chc.proof.CProofDiagnostic.CProofDiagnostic(xnode: Optional[xml.etree.ElementTree.Element])[source]

Bases: object

property argument_indices: List[int]
property argument_msgs: Dict[int, List[str]]

Returns argument-specific diagnostic messages.

Note: argument index starts at 1.

get_invariant_ids(index: int) → List[int][source]
property invsmap: Dict[int, List[int]]

Returns a map from argument index to invariant indices.

Note: argument index starts at 1.

property keyword_msgs: Dict[str, List[str]]

Returns diagnostics with a known keyword (e.g., a domain name).

property msgs: List[str]

Returns general diagnostics pertaining to the proof obligation.

write_xml(dnode: xml.etree.ElementTree.Element) → None[source]