From 71c58a8d494eafd847776446b0c246229b2bc9cf Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 2 Sep 2019 18:30:25 +0200 Subject: avancement (il faut utiliser Vundef visiblement) --- backend/RTLgen.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/RTLgen.v') diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 9d7a8506..a0ca0f17 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -436,7 +436,7 @@ Fixpoint transl_expr (map: mapping) (a: expr) (rd: reg) (nd: node) transl_exprlist map al rl no | Eload chunk addr al => do rl <- alloc_regs map al; - do no <- add_instr (Iload chunk addr rl rd nd); + do no <- add_instr (Iload TRAP chunk addr rl rd nd); transl_exprlist map al rl no | Econdition a b c => do nfalse <- transl_expr map c rd nd; -- cgit