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/RTLPargenproof.v | |
| parent | f3e95ff03f1dc9a9de57721eb1c9c93c19329613 (diff) | |
| download | vericert-2e232deb0aed4af2448eb9f1031e8084181174b7.tar.gz vericert-2e232deb0aed4af2448eb9f1031e8084181174b7.zip | |
Add list of bb to semantics
Diffstat (limited to 'src/hls/RTLPargenproof.v')
| -rw-r--r-- | src/hls/RTLPargenproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index 4e88b13..215aef5 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -812,8 +812,8 @@ Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop := (STACKS: list_forall2 match_stackframes sf sf') (REG: forall x, rs !! x = rs' !! x) (REG: forall x, ps !! x = ps' !! x), - match_states (State sf f sp pc rs ps m) - (State sf' tf sp pc rs' ps' m) + match_states (State sf f sp pc nil rs ps m) + (State sf' tf sp pc nil rs' ps' m) | match_returnstate: forall stack stack' v m (STACKS: list_forall2 match_stackframes stack stack'), |