chc.api.CFunctionContract module

User-provided function contract with assumptions and guarantees.

class chc.api.CFunctionContract.CFunctionContract(cfilecontracts: CFileContracts, xnode: xml.etree.ElementTree.Element)[source]

Bases: object

add_postrequest(req: XPredicate) → None[source]: Add post request from caller’s function api

property api: CFunctionApi

property cfile: CFile

property cfilecontracts: CFileContracts

property cfun: CFunction

has_assertions() → bool[source]

has_postconditions() → bool[source]

has_preconditions() → bool[source]

property ifd: InterfaceDictionary

property ignore: bool

property name: str

property postconditions: Dict[int, XPredicate]

property postrequests: Dict[int, XPredicate]

property preconditions: Dict[int, XPredicate]

report_postconditions() → str[source]

report_preconditions() → str[source]

property rsignature: Dict[int, str]

property sideeffects: Dict[int, XPredicate]

property signature: Dict[str, int]