Merge pull request #53 from goblint/no_cilint

Use `Cilint` in `CInt64`

Author: michael-schwarz

.merlin

@@ -9,4 +9,4 @@ B _build/src/ext/
 B _build/src/ext/pta/
 B _build/src/frontc/
 B _build/src/ocamlutil/
-PKG findlib
+PKG findlib, zarith

src/check.ml

@@ -641,8 +641,8 @@ and checkInit  (i: init) : typ =
                 match elen with
                 | None -> 0L
                 | Some e -> (ignore (checkExp true e);
-                match isInteger (constFold true e) with
-                  Some len -> len
+                match getInteger (constFold true e) with
+                  Some len -> Z.to_int64 len (* Z on purpose, we don't want to ignore overflows here *)
                 | None ->
                     ignore (warn "Array length is not a constant");
                     0L)
@@ -652,10 +652,10 @@ and checkInit  (i: init) : typ =
                     if i > len then
                       ignore (warn "Wrong number of initializers in array")
 
-                | (Index(Const(CInt64(i', _, _)), NoOffset), ei) :: rest ->
-                    if i' <> i then
+                | (Index(Const(CInt(i', _, _)), NoOffset), ei) :: rest ->
+                    if Int64.compare (Z.to_int64 i') i <> 0 then
                       ignore (warn "Initializer for index %s when %s was expected"
-                                (Int64.format "%d" i') (Int64.format "%d" i));
+                                (Int64.format "%d" (Z.to_int64 i')) (Int64.format "%d" i));
                     checkInitType ei bt;
                     loopIndex (Int64.succ i) rest
                 | _ :: rest ->