diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 12:09:03 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 12:09:03 +0100 |
commit | 86e64fd05cea7b1da996701cd3653db5f471f8d1 (patch) | |
tree | 5cee338b89c4b1b2906cbf8e62d8f8dffdff0abb /src/hls/IfConversion.v | |
parent | 4d62c7f35533ebd36ae4a0bdef6cd64fcc0be375 (diff) | |
download | vericert-86e64fd05cea7b1da996701cd3653db5f471f8d1.tar.gz vericert-86e64fd05cea7b1da996701cd3653db5f471f8d1.zip |
Finish final forward simulation correctness
Diffstat (limited to 'src/hls/IfConversion.v')
-rw-r--r-- | src/hls/IfConversion.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 8ca9cb6..ecafc13 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -247,7 +247,7 @@ Definition ifconv_list (headers: list node) (c: code) := Definition if_convert_code (c: code) iflist := fold_left (fun s n => if_convert c s (fst n) (snd n)) iflist c. -Definition transf_function (l: option if_conv_t) (f: function) : function := +Definition transf_function (f: function) : function := let (b, _) := build_bourdoncle f in let b' := get_loops b in let iflist := ifconv_list b' f.(fn_code) in @@ -274,8 +274,8 @@ Section TRANSF_PROGRAM. End TRANSF_PROGRAM. -Definition transf_fundef (l: option if_conv_t) (fd: fundef) : fundef := - transf_fundef (transf_function l) fd. +Definition transf_fundef (fd: fundef) : fundef := + transf_fundef transf_function fd. -Definition transf_program (l: PTree.t if_conv_t) (p: program) : program := - transform_program_data transf_fundef l p. +Definition transf_program (p: program) : program := + transform_program transf_fundef p. |