|
49 | 49 | ids=[spec.stem for spec in PROVE_FILES], |
50 | 50 | ) |
51 | 51 | def test_prove(rs_file: Path, kmir: KMIR, update_expected_output: bool) -> None: |
52 | | - should_fail = rs_file.stem.endswith('fail') or rs_file.stem.endswith('unsupported') |
| 52 | + should_fail = rs_file.stem.endswith('fail') |
| 53 | + should_show = should_fail or rs_file.stem.endswith('unsupported') |
53 | 54 | is_smir = rs_file.suffix == '.json' |
54 | 55 |
|
55 | | - if update_expected_output and not should_fail: |
| 56 | + start_symbols = ['main'] |
| 57 | + if rs_file.stem in PROVE_START_SYMBOLS: |
| 58 | + start_symbols = PROVE_START_SYMBOLS[rs_file.stem] |
| 59 | + |
| 60 | + if update_expected_output and not should_show: |
| 61 | + for start_symbol in start_symbols: |
| 62 | + expected_file = PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.expected' |
| 63 | + assert not expected_file.is_file() |
56 | 64 | pytest.skip() |
57 | 65 |
|
58 | 66 | prove_opts = ProveOpts(rs_file, smir=is_smir, terminate_on_thunk=True) |
59 | 67 | printer = PrettyPrinter(kmir.definition) |
60 | 68 | cterm_show = CTermShow(printer.print) |
61 | 69 |
|
62 | | - start_symbols = ['main'] |
63 | | - if rs_file.stem in PROVE_START_SYMBOLS: |
64 | | - start_symbols = PROVE_START_SYMBOLS[rs_file.stem] |
65 | | - |
66 | 70 | for start_symbol in start_symbols: |
67 | 71 | prove_opts.start_symbol = start_symbol |
68 | 72 | apr_proof = kmir.prove_program(prove_opts) |
| 73 | + expected_file = PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.expected' |
69 | 74 |
|
70 | | - if should_fail: |
71 | | - assert apr_proof.failed |
| 75 | + if should_show: |
72 | 76 | display_opts = ShowOpts( |
73 | 77 | rs_file.parent, apr_proof.id, full_printer=False, smir_info=None, omit_current_body=False |
74 | 78 | ) |
75 | 79 | shower = APRProofShow(kmir.definition, node_printer=KMIRAPRNodePrinter(cterm_show, apr_proof, display_opts)) |
76 | 80 | show_res = '\n'.join(shower.show(apr_proof)) |
77 | | - assert_or_update_show_output( |
78 | | - show_res, PROVE_DIR / f'show/{rs_file.stem}.{start_symbol}.expected', update=update_expected_output |
79 | | - ) |
| 81 | + assert_or_update_show_output(show_res, expected_file, update=update_expected_output) |
80 | 82 | else: |
| 83 | + assert not expected_file.is_file() |
81 | 84 | assert apr_proof.passed |
82 | 85 |
|
| 86 | + if should_fail: |
| 87 | + assert apr_proof.failed |
| 88 | + |
83 | 89 |
|
84 | 90 | VERIFY_RUST_STD_DIR = (Path(__file__).parent / 'data' / 'verify-rust-std').resolve(strict=True) |
85 | 91 | VERIFY_RUST_STD_FILES = list(VERIFY_RUST_STD_DIR.glob('**/*.rs')) |
|
0 commit comments