chc.api.GlobalAssumption module

Assumption on a global variable at a particular location.

class chc.api.GlobalAssumption.GlobalAssumption(capi: CFunctionApi, id: int, predicate: XPredicate, ppos: List[int], spos: List[int])[source]

Bases: object

Assumption on the value of a global variable at a particular location.

Parameters

  • capi (CFunctionApi) – the function api of the function that requests the assumption

  • id (int) – the identification number of the assumption

  • predicate (XPredicate) – predicate on global variable representing the assumption

  • ppos (List[int]) – id’s of the primary proof obligations that require this assumption for discharge

  • spos (List[int]) – id’s of the supporting proof obligations that require this assumption for discharge

property capi: CFunctionApi
property cfun: CFunction
get_open_ppos() → List[int][source]
get_open_spos() → List[int][source]
has_open_pos() → bool[source]
property id: int
property ppos: List[int]
property predicate: XPredicate
property spos: List[int]