diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-30 16:07:43 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-30 16:07:43 +0100 |
| commit | 2c5f867a347637cf1b651da7d041d9670493f540 (patch) | |
| tree | e3d3501bb63c7c08f6567ee5b2a0ed581cc5a8d6 /src/hls/HTLgen.v | |
| parent | c4653db6279185a338e8b0d59a02fb7ff7ccc554 (diff) | |
| download | vericert-2c5f867a347637cf1b651da7d041d9670493f540.tar.gz vericert-2c5f867a347637cf1b651da7d041d9670493f540.zip | |
Fix map_externctrl double-incrementing freshreg
Diffstat (limited to 'src/hls/HTLgen.v')
| -rw-r--r-- | src/hls/HTLgen.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index aa1064b..5400e25 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -163,10 +163,9 @@ Next Obligation. constructor; simpl; auto with htlh. Qed. Program Definition map_externctrl (othermod : ident) (ctrl : controlsignal) : mon reg := do r <- create_reg None (controlsignal_sz ctrl); - fun s => let r := s.(st_freshreg) in - OK r (mkstate + fun s => OK r (mkstate s.(st_st) - (Pos.succ r) + (st_freshreg s) (st_freshstate s) (st_scldecls s) (st_arrdecls s) |