diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-05-26 12:04:59 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-26 12:04:59 +0100 |
| commit | bdd3b6734690100a7c696cf57bfe52963ec2c6ef (patch) | |
| tree | 7e245bfc7fd0e9154e5f2ad5f1540850ec4b592f /src/translation/HTLgen.v | |
| parent | 43b078ba35aec32840f459d67de3fe6408184cea (diff) | |
| download | vericert-kvx-bdd3b6734690100a7c696cf57bfe52963ec2c6ef.tar.gz vericert-kvx-bdd3b6734690100a7c696cf57bfe52963ec2c6ef.zip | |
Finished second pass and fixed bug
Diffstat (limited to 'src/translation/HTLgen.v')
| -rw-r--r-- | src/translation/HTLgen.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v index 714cf98..670dcd4 100644 --- a/src/translation/HTLgen.v +++ b/src/translation/HTLgen.v @@ -272,7 +272,7 @@ Definition transf_instr (fin rtrn: reg) (ni: node * instruction) : mon unit := | Inop n' => add_instr n n' Vskip | Iop op args dst n' => do instr <- translate_instr op args; - add_instr n n' (block dst instr) + add_instr n n' (nonblock dst instr) | Iload _ _ _ _ _ => error (Errors.msg "Loads are not implemented.") | Istore _ _ _ _ _ => error (Errors.msg "Stores are not implemented.") | Icall _ _ _ _ _ => error (Errors.msg "Calls are not implemented.") |