Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 1 addition & 3 deletions Makefile.in
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ ocamlbuild:
META:
@rm -f $@
@printf "description = \"C Intermediate Language\"\n" >>$@
@printf "requires = \"unix str num dynlink\"\n" >>$@
@printf "requires = \"unix str num dynlink findlib\"\n" >>$@
@printf "version = \"$(CIL_VERSION)\"\n\n" >>$@
@printf "archive(byte) = \"cil.cma\"\n" >>$@
@printf "archive(native) = \"cil.cmxa\"\n\n" >>$@
Expand Down Expand Up @@ -344,7 +344,6 @@ else
endif

install-findlib: META $(CILLIB_FILES) $(CILLIB_TARGETS) uninstall-findlib
mkdir -p $(OCAMLFIND_INSTALLDIR)
OCAMLFIND_DESTDIR=$(OCAMLFIND_INSTALLDIR) \
$(OCAMLFIND) install cil META $(CILLIB_TARGETS) `cat $(CILLIB_FILES)`

Expand All @@ -353,7 +352,6 @@ uninstall-findlib:

.PHONY: install-data uninstall-data
install-data:
mkdir -p $(DESTDIR)$(datadir)
ifneq ($(CYGPATH),)
printf $(shell $(CYGPATH) -ma "$(OCAMLFIND_DESTDIR)") > ocamlpath
else
Expand Down
2 changes: 1 addition & 1 deletion _tags
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
# Traverse only subdirectories containing source code
true: -traverse
true: -traverse, package(zarith)
<src>: include
# build every cmo in debug mode (for cil.cma)
<**/*.cmo>: debug
Expand Down
28 changes: 14 additions & 14 deletions configure
Original file line number Diff line number Diff line change
Expand Up @@ -3703,20 +3703,6 @@ $as_echo "version differs from ocamlc; ocamlopt.opt discarded." >&6; }



# checking for native dynlink
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for dynlink.cmxa" >&5
$as_echo_n "checking for dynlink.cmxa... " >&6; }
if test -f "$OCAMLLIB/dynlink.cmxa" ; then
OCAMLNATDYNLINK=yes
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
$as_echo "yes" >&6; }
else
OCAMLNATDYNLINK=no
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
$as_echo "no" >&6; }
fi



# checking for ocaml toplevel
if test -n "$ac_tool_prefix"; then
Expand Down Expand Up @@ -4684,6 +4670,20 @@ if test "$OCAMLFIND" = "no"; then
as_fn_error $? "You must install OCaml findlib (the ocamlfind command)" "$LINENO" 5
fi

# checking for native dynlink
{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for dynlink.cmxa" >&5
$as_echo_n "checking for dynlink... " >&6; }
$OCAMLFIND query dynlink
case $? in
0) OCAMLNATDYNLINK=yes
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
$as_echo "yes" >&6; };;
*) OCAMLNATDYNLINK=no
{ $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
$as_echo "no" >&6; };;
esac


# ------------------- Perl ----------------

if test -n "$ac_tool_prefix"; then
Expand Down
16 changes: 7 additions & 9 deletions opam
Original file line number Diff line number Diff line change
@@ -1,18 +1,15 @@
opam-version: "1.2"
opam-version: "2.0"
authors: ["gabriel@kerneis.info"]
maintainer: "gabriel@kerneis.info"
homepage: "https://cil-project.github.io/cil/"
bug-reports: "https://github.com/cil-project/cil/issues/"
description: "Cil"
dev-repo: "git+https://github.com/cil-project/cil/"
build: [
["env" "FORCE_PERL_PREFIX=1" "./configure" "--prefix" prefix]
[make]
]
build-test: [
["env" "VERBOSE=1" make "test"]
]
build-doc: [
[make "doc"]
["env" "VERBOSE=1" make "test"] {with-test}
[make "doc"] {with-doc}
]
install: [
make "install"
Expand All @@ -22,8 +19,9 @@ remove: [
[make "uninstall"]
]
depends: [
"ocaml"
"ocamlfind"
"ocamlbuild" {build}
"hevea" {build & doc}
"hevea" {build & test}
"hevea" {build & with-doc}
"hevea" {build & with-test}
]
Empty file added share/.gitkeep
Empty file.
2 changes: 1 addition & 1 deletion src/_tags
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
<ext> or <ext/*> or <frontc> or <ocamlutil>: include

<feature.ml>: package(findlib)
<main.{byte,native}>: use_unix, use_str, use_nums, use_dynlink, use_cil, linkall, package(findlib)
<main.{byte,native}>: use_unix, use_str, use_dynlink, use_cil, linkall, package(findlib)
2 changes: 1 addition & 1 deletion src/check.ml
Original file line number Diff line number Diff line change
Expand Up @@ -646,7 +646,7 @@ and checkInit (i: init) : typ =
| (Index(Const(CInt64(i', _, _)), NoOffset), ei) :: rest ->
if i' <> i then
ignore (warn "Initializer for index %s when %s was expected"
(Int64.format "%d" i') (Int64.format "%d" i));
(Int64.to_string i') (Int64.to_string i));
checkInitType ei bt;
loopIndex (Int64.succ i) rest
| _ :: rest ->
Expand Down
26 changes: 13 additions & 13 deletions src/cil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1696,7 +1696,7 @@ let d_const () c =
* integers in negative form. -- Gabriel *)
E.s (E.bug "unexpected negative unsigned integer (please report this bug)")
else
text (prefix ^ "0x" ^ Int64.format "%x" i ^ suffix)
text (Format.sprintf "%s0x%Lx%s" prefix i suffix)
else (
if (i = mostNeg32BitInt) then
(* sm: quirk here: if you print -2147483648 then this is two tokens *)
Expand Down Expand Up @@ -2713,7 +2713,7 @@ let parseInt (str: string) : exp =
let l = String.length str in
fun s ->
let ls = String.length s in
l >= ls && s = String.uppercase (String.sub str (l - ls) ls)
l >= ls && s = String.uppercase_ascii (String.sub str (l - ls) ls)
in
let l = String.length str in
(* See if it is octal or hex *)
Expand Down Expand Up @@ -4643,12 +4643,12 @@ class plainCilPrinterClass =
Const(c) ->
let d_plainconst () c =
match c with
CInt64(i, ik, so) ->
let fmt = if isSigned ik then "%d" else "%x" in
dprintf "Int64(%s,%a,%s)"
(Int64.format fmt i)
d_ikind ik
(match so with Some s -> s | _ -> "None")
CInt64(i, ik, so) ->
let sos = match so with Some s -> s | _ -> "None" in
if isSigned ik then
dprintf "Int64(%Ld,%a,%s)" i d_ikind ik sos
else
dprintf "Int64(%Lx,%a,%s)" i d_ikind ik sos
| CStr(s) ->
text ("CStr(\"" ^ escape_string s ^ "\")")
| CWStr(s) ->
Expand Down Expand Up @@ -5080,19 +5080,19 @@ let loadBinaryFile (filename : string) : file =
(* Take the name of a file and make a valid symbol name out of it. There are
* a few characters that are not valid in symbols *)
let makeValidSymbolName (s: string) =
let s = String.copy s in (* So that we can update in place *)
let l = String.length s in
let s = Bytes.of_string s in (* So that we can update in place *)
let l = Bytes.length s in
for i = 0 to l - 1 do
let c = String.get s i in
let c = Bytes.get s i in
let isinvalid =
match c with
'-' | '.' -> true
| _ -> false
in
if isinvalid then
String.set s i '_';
Bytes.set s i '_';
done;
s
Bytes.to_string s

let rec addOffset (toadd: offset) (off: offset) : offset =
match off with
Expand Down
5 changes: 3 additions & 2 deletions src/cilint.ml
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,9 @@
bitwise operations on big_ints, and bug-fixed versions of int64_of_big_int
and big_int_of_int64. *)

open Big_int

type big_int = Z.t
open Big_int_Z

type cilint = Small of int | Big of big_int
type truncation = NoTruncation | ValueTruncation | BitTruncation

Expand Down
7 changes: 4 additions & 3 deletions src/cilint.mli
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,8 @@
(** The cilint type is public and not just big_int to make life with ocamldebug
easier. Please do not rely on this representation, use the ..._of_cilint
functions to get at a cilint's value. *)
type cilint = Small of int | Big of Big_int.big_int
type big_int = Z.t
type cilint = Small of int | Big of big_int

(** 0 as a cilint *)
val zero_cilint : cilint
Expand Down Expand Up @@ -85,7 +86,7 @@ val int_of_cilint : cilint -> int
val int64_of_cilint : cilint -> int64

(** Return the cilint's value as a big_int *)
val big_int_of_cilint : cilint -> Big_int.big_int
val big_int_of_cilint : cilint -> big_int

(** Return the cilint's value as a string *)
val string_of_cilint : cilint -> string
Expand All @@ -97,7 +98,7 @@ val cilint_of_int : int -> cilint
val cilint_of_int64 : int64 -> cilint

(** Make a cilint from a big_int *)
val cilint_of_big_int : Big_int.big_int -> cilint
val cilint_of_big_int : big_int -> cilint

(** Make a cilint from a string *)
val cilint_of_string : string -> cilint
Expand Down
2 changes: 1 addition & 1 deletion src/dominators.ml
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ let debug = false
(* For each statement we maintain a set of statements that dominate it *)
module BS = Set.Make(struct
type t = Cil.stmt
let compare v1 v2 = Pervasives.compare v1.sid v2.sid
let compare v1 v2 = Stdlib.compare v1.sid v2.sid
end)


Expand Down
2 changes: 1 addition & 1 deletion src/ext/partial/heap.ml
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ type ('a) t = {
}

let create size = {
elements = Array.create (size+1) (max_int,None) ;
elements = Array.make (size+1) (max_int,None) ;
size = 0 ;
capacity = size ;
}
Expand Down
10 changes: 5 additions & 5 deletions src/ext/pta/golf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,7 @@ struct
type 'a t = 'a bound
let compare (x : 'a t) (y : 'a t) =
if U.equal (x.info, y.info) then x.index - y.index
else Pervasives.compare (U.deref x.info) (U.deref y.info)
else Stdlib.compare (U.deref x.info) (U.deref y.info)
end

module Path =
Expand All @@ -113,12 +113,12 @@ struct
if U.equal (x.tail, y.tail) then
begin
if x.reached_global = y.reached_global then
Pervasives.compare x.kind y.kind
else Pervasives.compare x.reached_global y.reached_global
Stdlib.compare x.kind y.kind
else Stdlib.compare x.reached_global y.reached_global
end
else Pervasives.compare (U.deref x.tail) (U.deref y.tail)
else Stdlib.compare (U.deref x.tail) (U.deref y.tail)
end
else Pervasives.compare (U.deref x.head) (U.deref y.head)
else Stdlib.compare (U.deref x.head) (U.deref y.head)
end

module B = S.Make (Bound)
Expand Down
2 changes: 1 addition & 1 deletion src/ext/pta/olf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ module Bound =
struct
type 'a t = 'a bound
let compare (x : 'a t) (y : 'a t) =
Pervasives.compare (U.deref x.info) (U.deref y.info)
Stdlib.compare (U.deref x.info) (U.deref y.info)
end

module B = S.Make (Bound)
Expand Down
4 changes: 2 additions & 2 deletions src/ext/pta/steensgaard.ml
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ module Bound =
struct
type 'a t = 'a bound
let compare (x : 'a t) (y : 'a t) =
Pervasives.compare x y
Stdlib.compare x y
end

module B = S.Make(Bound)
Expand All @@ -92,7 +92,7 @@ struct
type t = constant

let compare ((xid,_) : t) ((yid,_) : t) =
Pervasives.compare xid yid
Stdlib.compare xid yid
end

module C = Set.Make(Constant)
Expand Down
2 changes: 1 addition & 1 deletion src/ext/zrapp/reachingdefs.ml
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ module IOS =
type t = int option
let compare io1 io2 =
match io1, io2 with
Some i1, Some i2 -> Pervasives.compare i1 i2
Some i1, Some i2 -> Stdlib.compare i1 i2
| Some i1, None -> 1
| None, Some i2 -> -1
| None, None -> 0
Expand Down
2 changes: 1 addition & 1 deletion src/ext/zrapp/rmciltmps.ml
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ module S = Stats
module IS =
Set.Make(struct
type t = int
let compare = Pervasives.compare
let compare = Stdlib.compare
end)

let debug = RD.debug
Expand Down
6 changes: 3 additions & 3 deletions src/formatlex.mll
Original file line number Diff line number Diff line change
Expand Up @@ -145,11 +145,11 @@ let scan_oct_escape str =
* We convert L"Hi" to "H\000i\000" *)
let wbtowc wstr =
let len = String.length wstr in
let dest = String.make (len * 2) '\000' in
let dest = Bytes.make (len * 2) '\000' in
for i = 0 to len-1 do
dest.[i*2] <- wstr.[i] ;
Bytes.set dest (i*2) wstr.[i] ;
done ;
dest
Bytes.to_string dest

(* This function converst the "Hi" in L"Hi" to { L'H', L'i', L'\0' } *)
let wstr_to_warray wstr =
Expand Down
4 changes: 2 additions & 2 deletions src/frontc/cabs2cil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1924,7 +1924,7 @@ let rec setOneInit (this: preInit)
let pMaxIdx, pArray =
match this with
NoInitPre -> (* No initializer so far here *)
ref idx, ref (Array.create (max 32 (idx + 1)) NoInitPre)
ref idx, ref (Array.make (max 32 (idx + 1)) NoInitPre)

| CompoundPre (pMaxIdx, pArray) ->
if !pMaxIdx < idx then begin
Expand Down Expand Up @@ -3417,7 +3417,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *)
let l = String.length str in
fun s ->
let ls = String.length s in
l >= ls && s = String.uppercase (String.sub str (l - ls) ls)
l >= ls && s = String.uppercase_ascii (String.sub str (l - ls) ls)
in
match ct with
A.CONST_INT str -> begin
Expand Down
2 changes: 1 addition & 1 deletion src/ocamlutil/bitmap.ml
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ type t = { mutable nrWords : int;
let enlarge b newWords =
let newbitmap =
if newWords > b.nrWords then
let a = Array.create newWords Int32.zero in
let a = Array.make newWords Int32.zero in
Array.blit b.bitmap 0 a 0 b.nrWords;
a
else
Expand Down
14 changes: 7 additions & 7 deletions src/ocamlutil/errormsg.ml
Original file line number Diff line number Diff line change
Expand Up @@ -209,18 +209,18 @@ let rem_quotes str = String.sub str 1 ((String.length str) - 2)
let cleanFileName str =
let str1 =
if str <> "" && String.get str 0 = '"' (* '"' ( *)
then rem_quotes str else str in
let l = String.length str1 in
then Bytes.of_string (rem_quotes str) else Bytes.of_string str in
let l = Bytes.length str1 in
let rec loop (copyto: int) (i: int) =
if i >= l then
String.sub str1 0 copyto
Bytes.sub_string str1 0 copyto
else
let c = String.get str1 i in
let c = Bytes.get str1 i in
if c <> '\\' then begin
String.set str1 copyto c; loop (copyto + 1) (i + 1)
Bytes.set str1 copyto c; loop (copyto + 1) (i + 1)
end else begin
String.set str1 copyto '/';
if i < l - 2 && String.get str1 (i + 1) = '\\' then
Bytes.set str1 copyto '/';
if i < l - 2 && Bytes.get str1 (i + 1) = '\\' then
loop (copyto + 1) (i + 2)
else
loop (copyto + 1) (i + 1)
Expand Down
2 changes: 1 addition & 1 deletion src/ocamlutil/inthash.ml
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ let resize tbl =
let osize = Array.length odata in
let nsize = min (2 * osize + 1) Sys.max_array_length in
if nsize <> osize then begin
let ndata = Array.create nsize Empty in
let ndata = Array.make nsize Empty in
let rec insert_bucket = function
Empty -> ()
| Cons(key, data, rest) ->
Expand Down
Loading