chc.cmdline.juliet.JulietTestSetRef module

Access to the reference results for all Juliet Tests.

class chc.cmdline.juliet.JulietTestSetRef.JulietTestSetMacros(d: Dict[str, Any])[source]

Bases: object

Macro definitions of proof obligations.

expand_macro(m: str) → List[Dict[str, Any]][source]: Returns a list of proof obligation definitions.

property po_macros: Dict[str, Dict[str, Any]]: Returns a dictionary of proof obligation definitions.

property predicates: List[str]

property ps_macros: Dict[str, List[str]]: Returns a dictionary of lists of macro definitions.

class chc.cmdline.juliet.JulietTestSetRef.JulietTestSetRef(d: Dict[str, Any])[source]

Bases: object

Reference proof obligation results for a juliet test set.

expand_macro(m: str) → List[Dict[str, Any]][source]

get_predicate_safe_controls() → Dict[str, int][source]

get_predicate_violations() → Dict[str, int][source]

get_safe_controls() → List[chc.cmdline.juliet.JulietTestFileRef.JulietSafeControl][source]

get_violations() → List[chc.cmdline.juliet.JulietTestFileRef.JulietViolation][source]

iter(f: Callable[[str, chc.cmdline.juliet.JulietTestRef.JulietTestRef], None]) → None[source]

property macros: chc.cmdline.juliet.JulietTestSetRef.JulietTestSetMacros

property predicates: List[str]

property tests: Dict[str, chc.cmdline.juliet.JulietTestRef.JulietTestRef]