aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/RTLPar.v
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-11-09 19:33:52 +0000
committerYann Herklotz <git@yannherklotz.com>2020-11-09 19:33:52 +0000
commitf2f21f405ae0a1f457f7bc32d5053f0a92959e72 (patch)
tree86b73d98fee0c3b15ce0be02cc4d54f8946530c0 /src/hls/RTLPar.v
parent56ea621762c865c1c71bdc7ad99afc4f2c291d5c (diff)
downloadvericert-f2f21f405ae0a1f457f7bc32d5053f0a92959e72.tar.gz
vericert-f2f21f405ae0a1f457f7bc32d5053f0a92959e72.zip
Change and add back HTLgen
Diffstat (limited to 'src/hls/RTLPar.v')
-rw-r--r--src/hls/RTLPar.v6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index 0e94fd5..0d37985 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -67,9 +67,9 @@ Definition funsig (fd: fundef) :=
Definition successors_instr (i : control_flow_inst) : list node :=
match i with
- (*| RPcall sig ros args res s => s :: nil*)
- (*| RPtailcall sig ros args => nil*)
- (*| RPbuiltin ef args res s => s :: nil*)
+ | RPcall sig ros args res s => s :: nil
+ | RPtailcall sig ros args => nil
+ | RPbuiltin ef args res s => s :: nil
| RPcond cond args ifso ifnot => ifso :: ifnot :: nil
| RPjumptable arg tbl => tbl
| RPreturn optarg => nil