chc.proof.CFunctionCallsiteSPOs module

Supporting proof obligations related to a single call site.

class chc.proof.CFunctionCallsiteSPOs.CFunctionCallsiteSPOs(cproofs: CFunctionProofs, xnode: xml.etree.ElementTree.Element)

Bases: object

Represents the supporting proof obligations associated with a call site.

property call_arguments: List[CExp]

property callee: CVarInfo

property callee_exp: CExp

property callees: List[CVarInfo]

Resolved indirect call targets.

property calltarget: chc.proof.CFunctionCallsiteSPOs.CallsiteTarget

property cfgcontext: CfgContext

property cfile: CFile

property cfun: CFunction

collect_post_assumes() → None

Collect postconditions from callee’s contract and add as assume.

property context: ProgramContext

property contextdictionary: CContextDictionary

property cproofs: CFunctionProofs

distribute_post_guarantees() → None

get_context_string()

get_spo(id: int) → chc.proof.CFunctionCallsiteSPO.CFunctionCallsiteSPO

has_callee() → bool

has_callee_exp() → bool

has_spo(id: int) → bool

property header: str

property iargs: List[int]

property icallees: List[int]

Indices of indirect calls.

property is_direct_call: bool

property is_indirect_call: bool

iter(f: Callable[[chc.proof.CFunctionCallsiteSPO.CFunctionCallsiteSPO], None]) → None

property line: int

property location: chc.app.CLocation.CLocation

property podictionary: CFunPODictionary

property postassumes: List[int]

property spos: Dict[int, List[chc.proof.CFunctionCallsiteSPO.CFunctionCallsiteSPO]]

update() → None

Update the spo’s associated with the call site.

write_xml(cnode: xml.etree.ElementTree.Element) → None

class chc.proof.CFunctionCallsiteSPOs.CallsiteTarget(cproofs: CFunctionProofs, xnode: xml.etree.ElementTree.Element)

Bases: object

property callee: CVarInfo

property callee_exp: CExp

property callees: List[CVarInfo]

property cfile: CFile

property cproofs: CFunctionProofs

has_callee() → bool

has_callee_exp() → bool

has_callees() → bool