diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-20 07:54:52 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-20 07:54:52 +0000 |
| commit | 255cee09b71255051c2b40eae0c88bffce1f6f32 (patch) | |
| tree | 7951b1b13e8fd5e525b9223e8be0580e83550f55 /backend/Constprop.v | |
| parent | 6e5041958df01c56762e90770abd704b95a36e5d (diff) | |
| download | compcert-kvx-255cee09b71255051c2b40eae0c88bffce1f6f32.tar.gz compcert-kvx-255cee09b71255051c2b40eae0c88bffce1f6f32.zip | |
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
Diffstat (limited to 'backend/Constprop.v')
| -rw-r--r-- | backend/Constprop.v | 5 |
1 files changed, 5 insertions, 0 deletions
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 |