From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Constprop.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'backend/Constprop.v') diff --git a/backend/Constprop.v b/backend/Constprop.v index f85405d6..0575079f 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -47,6 +47,7 @@ Module Approx <: SEMILATTICE_WITH_TOP. decide equality. apply Int.eq_dec. apply Float.eq_dec. + apply Int64.eq_dec. apply Int.eq_dec. apply ident_eq. apply Int.eq_dec. @@ -139,6 +140,10 @@ Fixpoint eval_load_init (chunk: memory_chunk) (pos: Z) (il: list init_data): app if zeq pos 0 then match chunk with Mint32 => I n | _ => Unknown end else eval_load_init chunk (pos - 4) il' + | Init_int64 n :: il' => + if zeq pos 0 + then match chunk with Mint64 => L n | _ => Unknown end + else eval_load_init chunk (pos - 8) il' | Init_float32 n :: il' => if zeq pos 0 then match chunk with -- cgit