chc.api.CGlobalContract module

Holds assumptions that transcend the file level.

The global contract is held by two files at the top directory of the contractpath:

  • globaldefs.json:

    • directions to the linker about hidden data structures and hidden fields

  • globaldefs.xml:

    • assumptions relevant to the CodeHawk analyzer

    • library function summaries that override the standard library function summaries

Examples:

  • abstraction of interfile data structures by hiding fields

  • abstraction of interfile data structures by complete hiding

class chc.api.CGlobalContract.CGlobalContract(capp: CApplication)[source]

Bases: object

add_no_free() → None[source]
property capp: CApplication
property contractpath: str
property globalassumptions: List[str]
property hiddenfields: Dict[str, Any]
property hiddenstructs: Dict[str, Any]
is_hidden_field(compname: str, fieldname: str) → bool[source]
is_hidden_struct(filename: str, compname: str) → bool[source]
save_global_xml_contract() → None[source]