chc.proof.CproofDependencies module

Dependencies of proof on assumptions and invariants.

class chc.proof.CProofDependencies.CProofDependencies(cproofs: CFunctionProofs, xnode: xml.etree.ElementTree.Element)[source]

Bases: object

Extent of dependency of a closed proof obligation.

levels:

  • ‘s’: dependent on statement itself only

  • ‘f’: dependent on function context

  • ‘r’: reduced to local spo in function context

  • ‘a’: dependent on other functions in the application

  • ‘x’: dead code

ids: list of api assumption id’s on which the proof is dependent

invs: list of invariants indices used to establish dependencies or validity

property cproofs: CFunctionProofs
has_external_dependencies() → bool[source]
property ids: List[int]
property invs: List[int]
property is_deadcode: bool
property is_local: bool
property is_stmt: bool
property level: str
write_xml(cnode: xml.etree.ElementTree.Element) → None[source]