chc.api.CFileContracts module

User-provided contracts for variables and functions in a c-file.

class chc.api.CFileContracts.CFileContractGlobalVar(gvinfo: CVarInfo, gvalue: Optional[int] = None, gconst: bool = False)[source]

Bases: object

User assertion about global variable.

class chc.api.CFileContracts.CFileContracts(cfile: CFile, contractpath: str)[source]

Bases: object

User-provided contracts for the functions in a c-file.

property cfile: CFile

property contractpath: str

count_postconditions() → int[source]

count_preconditions() → int[source]

function_contract(name: str) → chc.api.CFunctionContract.CFunctionContract[source]

property functions: Dict[str, chc.api.CFunctionContract.CFunctionContract]

property globalvariables: Dict[str, chc.api.CFileContracts.CFileContractGlobalVar]

has_assertions() → bool[source]

has_function_contract(name: str) → bool[source]: Returns true if this contract contains a function contract for name.

has_postconditions() → bool[source]

has_preconditions() → bool[source]

iter_functions(f: Callable[[chc.api.CFunctionContract.CFunctionContract], None]) → None[source]

report_postconditions() → str[source]

report_preconditions() → str[source]