chc.cmdline.kendra.TestManager module

exception chc.cmdline.kendra.TestManager.AnalyzerMissingError(msg: str)

Bases: Exception

exception chc.cmdline.kendra.TestManager.FileParseError(msg: str)

Bases: chc.util.fileutil.CHCError

exception chc.cmdline.kendra.TestManager.FunctionPEVError(msg: str)

Bases: Exception

exception chc.cmdline.kendra.TestManager.FunctionPPOError(msg: str)

Bases: Exception

exception chc.cmdline.kendra.TestManager.FunctionSEVError(msg: str)

Bases: Exception

exception chc.cmdline.kendra.TestManager.FunctionSPOError(msg: str)

Bases: Exception

class chc.cmdline.kendra.TestManager.TestManager(projectpath: str, targetpath: str, testname: str, saveref: bool = False, verbose: bool = True)

Bases: object

Provide utility functions to support regression and platform tests.

Parameters

• projectpath – directory that holds the source code

• targetpath – directory that holds the chc artifacts directory

• testname – name of the test directory

• saveref – adds missing ppos to functions in the json spec file and overwrites the json file with the result

property analysisresultspath: str

property cchpath: str

check_ppo_proofs(cfilename: str, cfun: chc.cmdline.kendra.TestCFunctionRef.TestCFunctionRef, funppos: List[CFunctionPO], refppos: List[chc.cmdline.kendra.TestPPORef.TestPPORef]) → None

Check if ppo analysis results match the expected results.

check_ppos(cfilename: str, cfun: str, ppos: List[CFunctionPO], refppos: List[chc.cmdline.kendra.TestPPORef.TestPPORef]) → None

Check if all required primary proof obligations are created.

check_spo_proofs(cfilename: str, cfun: chc.cmdline.kendra.TestCFunctionRef.TestCFunctionRef, funspos: List[CFunctionPO], refspos: List[chc.cmdline.kendra.TestSPORef.TestSPORef]) → None

Check if spo analysis results match the expected results.

check_spos(cfilename: str, cfun: str, spos: List[CFunctionPO], refspos: List[chc.cmdline.kendra.TestSPORef.TestSPORef]) → None

Check if spos created match reference spos.

clean() → None

property config: chc.util.Config.Config

property contractpath: str

create_reference_ppos(cfilename: str, fname: str, ppos: List[CFunctionPO]) → None

Create reference ppos from actual analysis results.

create_reference_spos(cfilename: str, fname: str, spos: List[CFunctionPO]) → None

Create reference spos from actual analysis results.

property cref_filenames: List[str]

property cref_files: List[chc.cmdline.kendra.TestCFileRef.TestCFileRef]

get_cref_file(cfilename: str) → Optional[chc.cmdline.kendra.TestCFileRef.TestCFileRef]

property is_linux_only: bool

property ismac: bool

property parsemanager: chc.cmdline.ParseManager.ParseManager

print_test_results() → None

print_test_results_line_summary() → None

print_test_results_summary() → None

property projectpath: str

property savedsourcepath: str

property saveref: bool

property targetpath: str

test_parser(savesemantics: bool = False) → bool

test_ppo_proofs(delaytest: bool = False) → None

Run analysis and check if analysis results match expected results.

Skip checking results if delaytest is true.

test_ppos() → None

Create primary proof obligations and check if created as expected.

test_spo_proofs(delaytest: bool = False) → None

Run analysis and check analysis results against the expected results.

Skip the checking if delaytest is True.

test_spos(delaytest: bool = False) → None

Run analysis and check if all expected spos are created.

property testname: str

property testresults: chc.cmdline.kendra.TestResults.TestResults

property testsetref: chc.cmdline.kendra.TestSetRef.TestSetRef

property verbose: bool

xcfile_exists(cfilename: str) → bool

Checks existence of xml file for cfilename.

xffile_exists(cfilename: str, funname: str) → bool

Checks existence of xml file for function funname in cfilename.

exception chc.cmdline.kendra.TestManager.XmlFileNotFoundError(msg: str)

Bases: Exception