From fecf2472ee5c2f6da25eb1ea340e0f07dcdaec69 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 6 Oct 2016 09:49:50 +0200 Subject: Regression: compile-time evaluation of ((struct s *)0)->field This somewhat useful idiom was broken when Val.add was replaced by Val.offset_ptr in the Efield case. This commit restores the previous behavior. This used to be supported (and is useful --- cfrontend/Initializers.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'cfrontend/Initializers.v') diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index 5b7e52c8..19518aea 100644 --- a/cfrontend/Initializers.v +++ b/cfrontend/Initializers.v @@ -119,7 +119,9 @@ Fixpoint constval (ce: composite_env) (a: expr) : res val := do co <- lookup_composite ce id; do delta <- field_offset ce f (co_members co); do v <- constval ce l; - OK (Val.offset_ptr v (Ptrofs.repr delta)) + OK (if Archi.ptr64 + then Val.addl v (Vlong (Int64.repr delta)) + else Val.add v (Vint (Int.repr delta))) | Tunion id _ => constval ce l | _ => -- cgit