diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-03-31 15:39:18 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-31 15:39:18 +0100 |
commit | 2e232deb0aed4af2448eb9f1031e8084181174b7 (patch) | |
tree | 6dd781e24a2a260047a8fc9e0a177d1b81bc3b5c /src/hls/RTLBlockgenproof.v | |
parent | f3e95ff03f1dc9a9de57721eb1c9c93c19329613 (diff) | |
download | vericert-2e232deb0aed4af2448eb9f1031e8084181174b7.tar.gz vericert-2e232deb0aed4af2448eb9f1031e8084181174b7.zip |
Add list of bb to semantics
Diffstat (limited to 'src/hls/RTLBlockgenproof.v')
-rw-r--r-- | src/hls/RTLBlockgenproof.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v index 42d471c..f870278 100644 --- a/src/hls/RTLBlockgenproof.v +++ b/src/hls/RTLBlockgenproof.v @@ -117,7 +117,7 @@ Variant match_states : RTL.state -> RTLBlock.state -> Prop := (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' rs ps m). + (State stk' tf sp pc' nil 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. @@ -165,5 +165,6 @@ Section CORRECTNESS. apply senv_preserved. admit. eauto using transl_final_states. + Admitted. End CORRECTNESS. |