From bdd3b6734690100a7c696cf57bfe52963ec2c6ef Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Tue, 26 May 2020 12:04:59 +0100 Subject: Finished second pass and fixed bug --- src/translation/HTLgen.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/translation/HTLgen.v') 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.") -- cgit