chc.invariants.CFunInvariantTable module

Table of invariant facts for an individual function.

class chc.invariants.CFunInvariantTable.CFunInvariantTable(cfun: CFunction, xnode: xml.etree.ElementTree.Element)[source]

Bases: object

Function-level invariants.

property cfile: CFile

property cfun: CFunction

context_invariants(context: ProgramContext) → List[chc.invariants.CInvariantFact.CInvariantFact][source]

property ctxtd: CContextDictionary

get_po_invariants(context: ProgramContext, poId: int) → List[chc.invariants.CInvariantFact.CInvariantFact][source]

get_sorted_invariants(context: ProgramContext) → List[chc.invariants.CInvariantFact.CInvariantFact][source]

property invariants: Dict[int, List[chc.invariants.CInvariantFact.CInvariantFact]]

property invd: CFunInvDictionary

property vard: CFunVarDictionary