chc.api.PostAssume module

Assumption on the return value of a function.

class chc.api.PostAssume.PostAssume(ifd: InterfaceDictionary, ixval: chc.util.IndexedTable.IndexedTableValue)[source]

Bases: chc.api.InterfaceDictionaryRecord.InterfaceDictionaryRecord

Assumption on the postcondition of a function.

args[0]: function vid (callee)
args[1]: index of predicate in interface dictionary

property callee: CVarInfo

property postcondition: XPredicate