chc.api.ApiAssumption module

Assumption on the function api.

class chc.api.ApiAssumption.ApiAssumption(capi: CFunctionApi, id: int, predicate: CPOPredicate, ppos: List[int], spos: List[int], isglobal: bool = False, isfile: bool = False)

Bases: object

Assumption on the function api.

Parameters

• capi (CFunctionApi) – parent function api

• id (int) – identification number

• predicate (CPOPredicate) – expression of the assumption

• ppos (List[int]) – list of primary proof obligation id’s that depend on this assumption

• spos (List[int]) – list of supporting proof obligation id’s that depend on this assumption

• isglobal (bool=False) – assumption holds globally

• isfile (bool=False) – assumption holds for the entire c-file