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

1 files changed, 8 insertions, 0 deletions

diff --git a/checklink/Check.ml b/checklink/Check.ml
index 5821953..73a7310 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -2696,6 +2696,14 @@ let compare_data (l: init_data list) (bs: bitstring) (sfw: s_framework)
               else ERR("Wrong float64")
           | { _ } -> error
         )
+        | Init_int64(i) -> (
+          bitmatch bs with
+          | { j : 64 : int; bs : -1 : bitstring } ->
+              if z_int64 i = j
+              then compare_data_aux l bs (s + 8) sfw
+              else ERR("Wrong int64")
+          | { _ } -> error
+        )
         | Init_space(z) -> (
           let space_size = z_int z in
           bitmatch bs with