diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-04-23 09:37:02 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-04-23 09:37:02 +0100 |
| commit | 6f9d16bb67f32463d98771f3f155297c4ea4b3b7 (patch) | |
| tree | 1d04c6794b53981a340af2d3b72971d8c9a02d8e /src/hls/RTLBlock.v | |
| parent | 1dce00e3afe9398a84239cc5f5d44c68b0b5c474 (diff) | |
| download | vericert-6f9d16bb67f32463d98771f3f155297c4ea4b3b7.tar.gz vericert-6f9d16bb67f32463d98771f3f155297c4ea4b3b7.zip | |
Fix translation passes with new semantics
Diffstat (limited to 'src/hls/RTLBlock.v')
| -rw-r--r-- | src/hls/RTLBlock.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index b9e9914..19ac4f5 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -93,9 +93,10 @@ function. | exec_bblock: forall s f sp pc rs rs' m m' bb pr pr' t state, f.(fn_code) ! pc = Some bb -> - step_instr_list sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') -> + step_instr_list sp (mk_instr_state rs pr m) bb.(bb_body) + (mk_instr_state rs' pr' m') -> step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t state -> - step (State s f sp pc rs pr m) E0 state + step (State s f sp pc rs pr m) t state | exec_function_internal: forall s f args m m' stk bb cf, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> |