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/RICtransf.v | |
| parent | f3e95ff03f1dc9a9de57721eb1c9c93c19329613 (diff) | |
| download | vericert-2e232deb0aed4af2448eb9f1031e8084181174b7.tar.gz vericert-2e232deb0aed4af2448eb9f1031e8084181174b7.zip | |
Add list of bb to semantics
Diffstat (limited to 'src/hls/RICtransf.v')
| -rw-r--r-- | src/hls/RICtransf.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/hls/RICtransf.v b/src/hls/RICtransf.v index 643a3a7..3b82b29 100644 --- a/src/hls/RICtransf.v +++ b/src/hls/RICtransf.v @@ -58,7 +58,7 @@ Definition add_bb (should_split: bool) (i: list (list instr)) | (a, b) => if should_split then (a, i::b) else (i::a, b) end. -Fixpoint first_split (saw_pred: bool) (bb: bb) := +Fixpoint first_split (saw_pred: bool) (bb: list bb) := match bb with | a :: b => match includes_setpred a with @@ -72,7 +72,7 @@ Fixpoint first_split (saw_pred: bool) (bb: bb) := | nil => (None, (nil, nil)) end. -Definition split_bb (fresh: node) (b: bb) : bb * bb * bb := +Definition split_bb (fresh: node) (b: list bb) : list bb * list bb * list bb := match first_split false b with | (Some p, (bb1, bb2)) => (bb1 ++ bb2, nil, nil) | (None, (bb1, bb2)) => (bb1 ++ bb2, nil, nil) |