From abe2bb5c40260a31ce5ee27b841bcbd647ff8b88 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 9 Apr 2011 16:59:13 +0000 Subject: Merge of branch "unsigned-offsets": - In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/CminorSel.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend/CminorSel.v') diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 29f7178..8a82c42 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -164,7 +164,7 @@ Inductive eval_expr: letenv -> expr -> val -> Prop := eval_expr le (Evar id) v | eval_Eop: forall le op al vl v, eval_exprlist le al vl -> - eval_operation ge sp op vl = Some v -> + eval_operation ge sp op vl m = Some v -> eval_expr le (Eop op al) v | eval_Eload: forall le chunk addr al vl vaddr v, eval_exprlist le al vl -> @@ -190,7 +190,7 @@ with eval_condexpr: letenv -> condexpr -> bool -> Prop := eval_condexpr le CEfalse false | eval_CEcond: forall le cond al vl b, eval_exprlist le al vl -> - eval_condition cond vl = Some b -> + eval_condition cond vl m = Some b -> eval_condexpr le (CEcond cond al) b | eval_CEcondition: forall le a b c vb1 vb2, eval_condexpr le a vb1 -> -- cgit v1.2.3