diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-04-05 14:37:11 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-04-05 14:37:11 +0100 |
| commit | dba20d6c8201c1271ebda9f228ad95c77c6ca8a6 (patch) | |
| tree | 6f7fd6d62ac726e1adbc6020f08310505b5431d7 /src/hls/RTLBlockgenproof.v | |
| parent | e0e291401dd98d4fb1c2a8ca16dc364b3ed6f836 (diff) | |
| download | vericert-dba20d6c8201c1271ebda9f228ad95c77c6ca8a6.tar.gz vericert-dba20d6c8201c1271ebda9f228ad95c77c6ca8a6.zip | |
Add basic blocks to the stackframe
Diffstat (limited to 'src/hls/RTLBlockgenproof.v')
| -rw-r--r-- | src/hls/RTLBlockgenproof.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v index f870278..f57af34 100644 --- a/src/hls/RTLBlockgenproof.v +++ b/src/hls/RTLBlockgenproof.v @@ -87,15 +87,15 @@ Variant transl_code_spec (c: RTL.code) (tc: code) := forall x x' i i', c ! x = Some i -> find_instr_spec tc x i x' i' -> - check_instr x i i' = true -> + Is_true (check_instr x i i') -> transl_code_spec c tc | transl_code_standard_cf : forall x x' i i' il, c ! x = Some i -> tc ! x' = Some il -> find_instr_spec tc x i x' i' -> - check_cf_instr_body i i' = true -> - check_cf_instr i il.(bb_exit) = true -> + Is_true (check_cf_instr_body i i') -> + Is_true (check_cf_instr i il.(bb_exit)) -> transl_code_spec c tc . @@ -112,12 +112,12 @@ Variant match_stackframe : RTL.stackframe -> stackframe -> Prop := Variant match_states : RTL.state -> RTLBlock.state -> Prop := | match_state : - forall stk stk' f tf sp pc rs m pc' ps + forall stk stk' f tf sp pc rs m pc' ps bb (TF: transl_function f = OK tf) (PC: find_block_spec tf.(fn_code) pc pc') (STK: Forall2 match_stackframe stk stk'), match_states (RTL.State stk f sp pc rs m) - (State stk' tf sp pc' nil rs ps m). + (State stk' tf sp pc' bb rs ps m). Definition match_prog (p: RTL.program) (tp: RTLBlock.program) := Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp. |