From c4cc75dc6abcb0eee6f3288e96fea4aec540fd68 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 5 Sep 2019 11:19:22 +0200 Subject: more proofs going through --- backend/Linearize.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend/Linearize.v') diff --git a/backend/Linearize.v b/backend/Linearize.v index 2cfa4d3c..4216958c 100644 --- a/backend/Linearize.v +++ b/backend/Linearize.v @@ -163,8 +163,8 @@ Fixpoint linearize_block (b: LTL.bblock) (k: code) : code := | nil => k | LTL.Lop op args res :: b' => Lop op args res :: linearize_block b' k - | LTL.Lload chunk addr args dst :: b' => - Lload chunk addr args dst :: linearize_block b' k + | LTL.Lload trap chunk addr args dst :: b' => + Lload trap chunk addr args dst :: linearize_block b' k | LTL.Lgetstack sl ofs ty dst :: b' => Lgetstack sl ofs ty dst :: linearize_block b' k | LTL.Lsetstack src sl ofs ty :: b' => -- cgit