From be4d6e42dfa287b93b1a35ec820ab2a5aaf8c7ec Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 19 May 2013 09:54:40 +0000 Subject: Merge of the float32 branch: - added RTL type "Tsingle" - ABI-compatible passing of single-precision floats on ARM and x86 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Linear.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/Linear.v') diff --git a/backend/Linear.v b/backend/Linear.v index bdb08b43..3c524368 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -160,7 +160,7 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f sp b rs' m) | exec_Lsetstack: forall s f sp src sl ofs ty b rs m rs', - rs' = Locmap.set (S sl ofs ty) (rs (R src)) (undef_regs (destroyed_by_op Omove) rs) -> + rs' = Locmap.set (S sl ofs ty) (rs (R src)) (undef_regs (destroyed_by_setstack ty) rs) -> step (State s f sp (Lsetstack src sl ofs ty :: b) rs m) E0 (State s f sp b rs' m) | exec_Lop: -- cgit