diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2022-03-26 15:48:47 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-26 15:48:47 +0000 |
| commit | dd8d4ae9c320668ac5fd70f72ea76b768edf8165 (patch) | |
| tree | a7c6fa3f15ab227516b00b8186789aeb420b642e /src/hls/HTLPargen.v | |
| parent | 30baa719fb15c45b13cb869056e51ec7446c0207 (diff) | |
| download | vericert-dd8d4ae9c320668ac5fd70f72ea76b768edf8165.tar.gz vericert-dd8d4ae9c320668ac5fd70f72ea76b768edf8165.zip | |
Remove literal files again
Diffstat (limited to 'src/hls/HTLPargen.v')
| -rw-r--r-- | src/hls/HTLPargen.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index 8c85701..8960ef9 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -405,7 +405,10 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg) | _, _ => error (Errors.msg "HTLPargen: translate_eff_addressing unsuported addressing") end. -(** Translate an instruction to a statement. FIX mulhs mulhu *) +(*| +Translate an instruction to a statement. FIX mulhs mulhu +|*) + Definition translate_instr (op : Op.operation) (args : list reg) : mon expr := match op, args with | Op.Omove, r::nil => ret (Vvar r) |