chc.api package

Functionality related to interaction between functions and files.

chc.api.ApiParameter	Object representation of api_parameter_t
chc.api.ApiAssumption	Assumption on the function api.
chc.api.CFileContracts	User-provided contracts for variables and functions in a c-file.
chc.api.CFunctionContract	User-provided function contract with assumptions and guarantees.
chc.api.CGlobalContract	Holds assumptions that transcend the file level.
chc.api.ContractAssumption	Assumption on the return value of a function represented by a predicate.
chc.api.FieldAssignment
chc.api.GlobalAssumption	Assumption on a global variable at a particular location.
chc.api.InterfaceDictionary	Dictionary of all non-local symbolic values.
chc.api.InterfaceDictionaryRecord	Base object value for the entries in the interface dictionary.
chc.api.PostAssume	Assumption on the return value of a function.
chc.api.PostConditionRequest
chc.api.PostRequest	Request for a particular postcondition predicate on a function.
chc.api.SOffset	Object representation of sumtype s_offset_t.
chc.api.STerm	Object representation of sum type s_term (term in an external predicate).
chc.api.XPredicate	Object representation of sum type xpredicate_t.

Submodules

• chc.api.ApiParameter module
  • Base class and subclasses:
• chc.api.ApiAssumption module
• chc.api.CFileContracts module
• chc.api.CFunctionContract module
• chc.api.CGlobalContract module
• chc.api.ContractAssumption module
• chc.api.FieldAssignment module
• chc.api.GlobalAssumption module
• chc.api.InterfaceDictionary module
• chc.api.InterfaceDictionaryRecord module
• chc.api.PostAssume module
• chc.api.PostConditionRequest module
• chc.api.PostRequest module
• chc.api.SOffset module
  • Base class and subclasses:
• chc.api.STerm
  • Base class and subclasses:
• chc.api.XPredicate
  • Base class and subclasses: