diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-05-27 19:02:23 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-05-27 19:02:47 +0100 |
commit | f6cccc2eea3f0d8dea8f4f5a1ca8b86fe74c13c7 (patch) | |
tree | 9bef7e806e407ad9c763771753c59cd8c4e2a652 /src/hls/Partition.ml | |
parent | 0a44da6a7037d9eb270386eeef4f929177c4ec0d (diff) | |
download | vericert-f6cccc2eea3f0d8dea8f4f5a1ca8b86fe74c13c7.tar.gz vericert-f6cccc2eea3f0d8dea8f4f5a1ca8b86fe74c13c7.zip |
Fix code generation in partitioning and scheduling
Diffstat (limited to 'src/hls/Partition.ml')
-rw-r--r-- | src/hls/Partition.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml index 3b7cdd7..07b1be9 100644 --- a/src/hls/Partition.ml +++ b/src/hls/Partition.ml @@ -68,14 +68,14 @@ let rec next_bblock_from_RTL is_start e (c : RTL.code) s i = match trans_inst, succ with | (None, Some i'), _ -> if List.exists (fun x -> x = s) (snd e) && not is_start then - Errors.OK [RBnop; RBexit (None, (RBgoto s))] + Errors.OK [RBexit (None, (RBgoto s))] else Errors.OK [RBnop; RBexit (None, i')] | (Some i', None), (s', Some i_n)::[] -> if List.exists (fun x -> x = s) (fst e) then Errors.OK [i'; RBexit (None, (RBgoto s'))] else if List.exists (fun x -> x = s) (snd e) && not is_start then - Errors.OK [RBnop; RBexit (None, (RBgoto s))] + Errors.OK [RBexit (None, (RBgoto s))] else begin match next_bblock_from_RTL false e c s' i_n with | Errors.OK bb -> |