Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
d7320259
Commit
d7320259
authored
Oct 09, 2017
by
Guillaume Melquiond
Browse files
Compile with -safe-string to help transition toward OCaml 4.06.0.
parent
d6bd47f9
Changes
16
Hide whitespace changes
Inline
Side-by-side
Makefile.in
View file @
d7320259
...
...
@@ -98,8 +98,8 @@ INCLUDES = @ZIPINCLUDE@ @MENHIRINCLUDE@
WARNINGS
=
A-4-9-41-44-45-50-52@5@48
OFLAGS
=
-w
$(WARNINGS)
-keep-locs
-bin-annot
-dtypes
-g
-I
lib/why3
$(INCLUDES)
BFLAGS
=
-w
$(WARNINGS)
-keep-locs
-bin-annot
-dtypes
-g
-I
lib/why3
$(INCLUDES)
OFLAGS
=
-w
$(WARNINGS)
-safe-string
-keep-locs
-bin-annot
-dtypes
-g
-I
lib/why3
$(INCLUDES)
BFLAGS
=
-w
$(WARNINGS)
-safe-string
-keep-locs
-bin-annot
-dtypes
-g
-I
lib/why3
$(INCLUDES)
OLINKFLAGS
=
-linkall
$(EXTCMXA)
BLINKFLAGS
=
-linkall
$(EXTCMA)
...
...
src/driver/prove_client.ml
View file @
d7320259
...
...
@@ -55,12 +55,12 @@ let send_request_string msg =
let
to_write
=
String
.
length
msg
in
let
rec
write
pointer
=
if
pointer
<
to_write
then
let
written
=
Unix
.
write
sock
msg
pointer
(
to_write
-
pointer
)
in
let
written
=
Unix
.
write
_substring
sock
msg
pointer
(
to_write
-
pointer
)
in
write
(
pointer
+
written
)
in
write
0
let
read_from_client
=
let
buf
=
String
.
make
1024
'
'
in
let
buf
=
Bytes
.
make
1024
'
'
in
fun
blocking
->
match
!
socket
with
|
None
->
raise
NotConnected
...
...
@@ -73,7 +73,7 @@ let read_from_client =
in
if
do_read
then
let
read
=
Unix
.
read
sock
buf
0
1024
in
String
.
sub
buf
0
read
Bytes
.
sub_string
buf
0
read
else
""
(* TODO/FIXME: should we be able to change this setting when
...
...
src/ide/wserver.ml
View file @
d7320259
...
...
@@ -9,7 +9,6 @@
(* *)
(********************************************************************)
open
Why3
.
Strings
open
Format
let
blocking
=
false
...
...
@@ -51,28 +50,29 @@ let decode s =
match
s
.
[
i
]
with
'
%
'
when
i
+
2
<
String
.
length
s
->
let
v
=
hexa_val
s
.
[
i
+
1
]
*
16
+
hexa_val
s
.
[
i
+
2
]
in
set
s1
i1
(
Char
.
chr
v
);
i
+
3
|
'
+
'
->
set
s1
i1
'
'
;
succ
i
|
x
->
set
s1
i1
x
;
succ
i
Bytes
.
set
s1
i1
(
Char
.
chr
v
);
i
+
3
|
'
+
'
->
Bytes
.
set
s1
i1
'
'
;
succ
i
|
x
->
Bytes
.
set
s1
i1
x
;
succ
i
in
copy_decode_in
s1
i
(
succ
i1
)
else
s1
in
let
rec
strip_heading_and_trailing_spaces
s
=
if
String
.
length
s
>
0
then
if
s
.
[
0
]
==
'
'
then
let
sl
=
Bytes
.
length
s
in
if
sl
>
0
then
if
Bytes
.
get
s
0
==
'
'
then
strip_heading_and_trailing_spaces
(
String
.
sub
s
1
(
String
.
length
s
-
1
))
else
if
s
.
[
String
.
length
s
-
1
]
==
'
'
then
(
Bytes
.
sub
s
1
(
s
l
-
1
))
else
if
Bytes
.
get
s
(
sl
-
1
)
==
'
'
then
strip_heading_and_trailing_spaces
(
String
.
sub
s
0
(
String
.
length
s
-
1
))
(
Bytes
.
sub
s
0
(
s
l
-
1
))
else
s
else
s
in
if
need_decode
0
then
let
len
=
compute_len
0
0
in
let
s1
=
create
len
in
strip_heading_and_trailing_spaces
(
copy_decode_in
s1
0
0
)
let
s1
=
Bytes
.
create
len
in
Bytes
.
to_string
(
strip_heading_and_trailing_spaces
(
copy_decode_in
s1
0
0
)
)
else
s
let
special
=
...
...
@@ -101,22 +101,23 @@ let encode s =
if
i
<
String
.
length
s
then
let
i1
=
match
s
.
[
i
]
with
'
'
->
set
s1
i1
'
+
'
;
succ
i1
'
'
->
Bytes
.
set
s1
i1
'
+
'
;
succ
i1
|
c
->
if
special
c
then
begin
set
s1
i1
'
%
'
;
set
s1
(
i1
+
1
)
(
hexa_digit
(
Char
.
code
c
/
16
));
set
s1
(
i1
+
2
)
(
hexa_digit
(
Char
.
code
c
mod
16
));
Bytes
.
set
s1
i1
'
%
'
;
Bytes
.
set
s1
(
i1
+
1
)
(
hexa_digit
(
Char
.
code
c
/
16
));
Bytes
.
set
s1
(
i1
+
2
)
(
hexa_digit
(
Char
.
code
c
mod
16
));
i1
+
3
end
else
begin
set
s1
i1
c
;
succ
i1
end
else
begin
Bytes
.
set
s1
i1
c
;
succ
i1
end
in
copy_code_in
s1
(
succ
i
)
i1
else
s1
in
if
need_code
0
then
let
len
=
compute_len
0
0
in
copy_code_in
(
create
len
)
0
0
let
len
=
compute_len
0
0
in
Bytes
.
to_string
(
copy_code_in
(
Bytes
.
create
len
)
0
0
)
else
s
let
nl
=
"
\013\010
"
...
...
@@ -176,7 +177,8 @@ let print_exc exc =
let
print_err_exc
exc
=
print_exc
exc
;
flush
stderr
let
case_unsensitive_eq
s1
s2
=
lowercase
s1
=
lowercase
s2
let
case_unsensitive_eq
s1
s2
=
Why3
.
Strings
.
lowercase
s1
=
Why3
.
Strings
.
lowercase
s2
let
rec
extract_param
name
stop_char
=
function
...
...
@@ -196,26 +198,25 @@ let rec extract_param name stop_char =
else
extract_param
name
stop_char
l
|
[]
->
""
let
buff
=
ref
(
create
80
)
let
store
len
x
=
if
len
>=
String
.
length
!
buff
then
buff
:=
!
buff
^
create
(
String
.
length
!
buff
);
set
!
buff
len
x
;
succ
len
let
get_buff
len
=
String
.
sub
!
buff
0
len
let
get_request
strm
=
let
rec
loop
len
(
strm__
:
_
Stream
.
t
)
=
let
buff
=
Buffer
.
create
80
in
let
rec
loop
(
strm__
:
_
Stream
.
t
)
=
match
Stream
.
peek
strm__
with
Some
'\010'
->
Stream
.
junk
strm__
;
let
s
=
strm__
in
if
len
==
0
then
[]
else
let
str
=
get_buff
len
in
str
::
loop
0
s
|
Some
'\013'
->
Stream
.
junk
strm__
;
loop
len
strm__
|
Some
c
->
Stream
.
junk
strm__
;
loop
(
store
len
c
)
strm__
|
_
->
if
len
==
0
then
[]
else
[
get_buff
len
]
|
Some
'\010'
->
Stream
.
junk
strm__
;
if
Buffer
.
length
buff
=
0
then
[]
else
let
str
=
Buffer
.
contents
buff
in
let
()
=
Buffer
.
clear
buff
in
str
::
loop
strm__
|
Some
'\013'
->
Stream
.
junk
strm__
;
loop
strm__
|
Some
c
->
Stream
.
junk
strm__
;
Buffer
.
add_char
buff
c
;
loop
strm__
|
_
->
if
Buffer
.
length
buff
=
0
then
[]
else
[
Buffer
.
contents
buff
]
in
loop
0
strm
loop
strm
let
get_request_and_content
strm
=
let
request
=
get_request
strm
in
...
...
@@ -223,15 +224,11 @@ let get_request_and_content strm =
match
extract_param
"content-length: "
'
'
request
with
""
->
""
|
x
->
let
str
=
create
(
int_of_string
x
)
in
for
i
=
0
to
String
.
length
str
-
1
do
set
str
i
(
let
(
strm__
:
_
Stream
.
t
)
=
strm
in
match
Stream
.
peek
strm__
with
Some
x
->
Stream
.
junk
strm__
;
x
|
_
->
'
'
)
done
;
str
String
.
init
(
int_of_string
x
)
(
fun
_
->
let
(
strm__
:
_
Stream
.
t
)
=
strm
in
match
Stream
.
peek
strm__
with
|
Some
x
->
Stream
.
junk
strm__
;
x
|
_
->
'
'
)
in
request
,
content
...
...
@@ -244,9 +241,9 @@ let sockaddr_of_string s = Unix.ADDR_UNIX s
let
treat_connection
_tmout
callback
addr
fd
fmt
=
let
(
request
,
contents__
)
=
let
strm
=
let
c
=
" "
in
let
c
=
Bytes
.
create
1
in
Stream
.
from
(
fun
_
->
if
Unix
.
read
fd
c
0
1
=
1
then
Some
c
.
[
0
]
else
None
)
(
fun
_
->
if
Unix
.
read
fd
c
0
1
=
1
then
Some
(
Bytes
.
get
c
0
)
else
None
)
in
get_request_and_content
strm
in
...
...
src/printer/coq.ml
View file @
d7320259
...
...
@@ -489,10 +489,10 @@ let read_old_proof =
Vernacular
end
in
let
len
=
pos_in
ch
-
!
start
in
let
s
=
String
s
.
create
len
in
let
s
=
Byte
s
.
create
len
in
seek_in
ch
!
start
;
really_input
ch
s
0
len
;
Query
(
name
,
k
,
s
)
Query
(
name
,
k
,
Bytes
.
unsafe_to_string
s
)
with
StringValue
s
->
Other
s
(* Load old-style proofs where users were confined to a few sections. *)
...
...
src/session/compress.mli
View file @
d7320259
...
...
@@ -11,7 +11,7 @@
val
compression_supported
:
bool
module
type
S
=
sig
module
type
S
=
sig
type
out_channel
...
...
@@ -19,7 +19,7 @@ val open_out: string -> out_channel
val
output_char
:
out_channel
->
char
->
unit
val
output
:
out_channel
->
string
->
int
->
int
->
unit
val
output
_substring
:
out_channel
->
string
->
int
->
int
->
unit
val
output_string
:
out_channel
->
string
->
unit
...
...
@@ -29,9 +29,9 @@ type in_channel
val
open_in
:
string
->
in_channel
val
input
:
in_channel
->
string
->
int
->
int
->
int
val
input
:
in_channel
->
bytes
->
int
->
int
->
int
val
really_input
:
in_channel
->
string
->
int
->
int
->
unit
val
really_input
:
in_channel
->
bytes
->
int
->
int
->
unit
val
input_char
:
in_channel
->
char
...
...
src/session/compress_none.ml
View file @
d7320259
...
...
@@ -9,9 +9,10 @@
(* *)
(********************************************************************)
#
13
"src/session/compress_none.ml"
let
compression_supported
=
false
module
type
S
=
sig
module
type
S
=
sig
type
out_channel
...
...
@@ -19,7 +20,7 @@ val open_out: string -> out_channel
val
output_char
:
out_channel
->
char
->
unit
val
output
:
out_channel
->
string
->
int
->
int
->
unit
val
output
_substring
:
out_channel
->
string
->
int
->
int
->
unit
val
output_string
:
out_channel
->
string
->
unit
...
...
@@ -29,9 +30,9 @@ type in_channel
val
open_in
:
string
->
in_channel
val
input
:
in_channel
->
string
->
int
->
int
->
int
val
input
:
in_channel
->
bytes
->
int
->
int
->
int
val
really_input
:
in_channel
->
string
->
int
->
int
->
unit
val
really_input
:
in_channel
->
bytes
->
int
->
int
->
unit
val
input_char
:
in_channel
->
char
...
...
src/session/compress_z.ml
View file @
d7320259
...
...
@@ -9,9 +9,10 @@
(* *)
(********************************************************************)
#
13
"src/session/compress_z.ml"
let
compression_supported
=
true
module
type
S
=
sig
module
type
S
=
sig
type
out_channel
...
...
@@ -19,7 +20,7 @@ val open_out: string -> out_channel
val
output_char
:
out_channel
->
char
->
unit
val
output
:
out_channel
->
string
->
int
->
int
->
unit
val
output
_substring
:
out_channel
->
string
->
int
->
int
->
unit
val
output_string
:
out_channel
->
string
->
unit
...
...
@@ -29,9 +30,9 @@ type in_channel
val
open_in
:
string
->
in_channel
val
input
:
in_channel
->
string
->
int
->
int
->
int
val
input
:
in_channel
->
bytes
->
int
->
int
->
int
val
really_input
:
in_channel
->
string
->
int
->
int
->
unit
val
really_input
:
in_channel
->
bytes
->
int
->
int
->
unit
val
input_char
:
in_channel
->
char
...
...
@@ -50,9 +51,9 @@ let open_out fn = Gzip.open_out ~level:6 fn
let
output_char
=
Gzip
.
output_char
let
output
=
Gzip
.
output
let
output
_substring
=
Gzip
.
output
_substring
let
output_string
ch
s
=
output
ch
s
0
(
String
.
length
s
)
let
output_string
ch
s
=
output
_substring
ch
s
0
(
String
.
length
s
)
let
close_out
=
Gzip
.
close_out
...
...
src/session/session_itp.ml
View file @
d7320259
...
...
@@ -1182,9 +1182,9 @@ exception ShapesFileError of string
module
ReadShapes
(
C
:
Compress
.
S
)
=
struct
let
shape
=
Buffer
.
create
97
let
sum
=
Strings
.
create
32
let
read_sum_and_shape
ch
=
let
sum
=
Bytes
.
create
32
in
let
nsum
=
C
.
input
ch
sum
0
32
in
if
nsum
=
0
then
raise
End_of_file
;
if
nsum
<>
32
then
...
...
@@ -1195,7 +1195,7 @@ let read_sum_and_shape ch =
raise
(
ShapesFileError
(
"shapes files corrupted (checksum '"
^
(
String
.
sub
sum
0
nsum
)
^
(
Bytes
.
sub_string
sum
0
nsum
)
^
"' too short), ignored"
))
end
;
if
try
C
.
input_char
ch
<>
'
'
with
End_of_file
->
true
then
...
...
@@ -1211,7 +1211,7 @@ let read_sum_and_shape ch =
with
|
End_of_file
->
raise
(
ShapesFileError
"shapes files corrupted (premature end of file), ignored"
);
|
Exit
->
Strings
.
copy
sum
,
Buffer
.
contents
shape
|
Exit
->
Bytes
.
unsafe_to_string
sum
,
Buffer
.
contents
shape
let
use_shapes
=
ref
true
...
...
src/util/cmdline.ml
View file @
d7320259
...
...
@@ -43,10 +43,7 @@ let cmdline_split s =
|
'\\'
->
cstate
:=
Escape
|
c
when
is_blank
c
->
let
n
=
Queue
.
length
cur_arg
in
let
s
=
Strings
.
create
n
in
for
i
=
0
to
pred
n
do
Strings
.
set
s
i
(
Queue
.
take
cur_arg
)
done
;
let
s
=
String
.
init
n
(
fun
_
->
Queue
.
take
cur_arg
)
in
argv
:=
s
::
!
argv
;
cstate
:=
Blank
|
c
->
Queue
.
add
c
cur_arg
...
...
src/util/lexlib.mll
View file @
d7320259
...
...
@@ -98,10 +98,10 @@ and string = parse
let
nb
=
ref
0
in
String
.
iter
(
fun
c
->
if
c
=
'
_'
then
incr
nb
)
s
;
!
nb
in
let
t
=
String
s
.
create
(
String
.
length
s
-
count
)
in
let
t
=
Byte
s
.
create
(
String
.
length
s
-
count
)
in
let
i
=
ref
0
in
String
.
iter
(
fun
c
->
if
c
<>
'
_'
then
(
String
s
.
set
t
!
i
c
;
incr
i
))
s
;
t
String
.
iter
(
fun
c
->
if
c
<>
'
_'
then
(
Byte
s
.
set
t
!
i
c
;
incr
i
))
s
;
Bytes
.
unsafe_to_string
t
end
else
s
}
src/util/number.ml
View file @
d7320259
...
...
@@ -156,9 +156,11 @@ let force_support support do_it v =
let
simplify_max_int
=
BigInt
.
of_string
"2147483646"
let
remove_minus
e
=
if
e
.
[
0
]
=
'
-
'
then
(
let
e'
=
Strings
.
copy
e
in
Strings
.
set
e'
0
'
m'
;
e'
)
else
e
if
e
.
[
0
]
=
'
-
'
then
begin
let
e
=
Bytes
.
of_string
e
in
Bytes
.
set
e
0
'
m'
;
Bytes
.
unsafe_to_string
e
end
else
e
let
print_dec_int
support
fmt
i
=
let
fallback
i
=
...
...
src/util/rc.mll
View file @
d7320259
...
...
@@ -64,20 +64,20 @@ let escape_string s =
| _ -> 1)
done;
if !n = String.length s then s else begin
let s' =
String
s.create !n in
let s' =
Byte
s.create !n in
n := 0;
for i = 0 to String.length s - 1 do
let c = String.unsafe_get s i in
begin match c with
| ('"
'
|
'\\'
|
'\n'
|
'\r'
|
'\t'
)
->
String
s
.
set
s'
!
n
'\\'
;
incr
n
Byte
s
.
set
s'
!
n
'\\'
;
incr
n
|
_
->
()
end
;
String
s
.
set
s'
!
n
Byte
s
.
set
s'
!
n
(
match
c
with
'\n'
->
'
n'
|
'\r'
->
'
r'
|
'\t'
->
'
t'
|
_
->
c
);
incr
n
done
;
s'
Bytes
.
unsafe_to_string
s'
end
let
print_rc_value
fmt
=
function
...
...
src/util/strings.ml
View file @
d7320259
...
...
@@ -9,12 +9,6 @@
(* *)
(********************************************************************)
let
create
=
String
.
create
let
copy
=
String
.
copy
let
set
=
String
.
set
let
lowercase
=
String
.
lowercase
let
capitalize
=
String
.
capitalize
let
uncapitalize
=
String
.
uncapitalize
...
...
@@ -60,10 +54,10 @@ let ends_with s suf =
let
pad_right
c
s
i
=
let
sl
=
String
.
length
s
in
if
sl
<
i
then
let
p
=
create
i
in
String
.
blit
s
0
p
0
sl
;
String
.
fill
p
sl
(
i
-
sl
)
c
;
p
let
p
=
Bytes
.
create
i
in
Bytes
.
blit_string
s
0
p
0
sl
;
Bytes
.
fill
p
sl
(
i
-
sl
)
c
;
Bytes
.
unsafe_to_string
p
else
if
sl
>
i
then
String
.
sub
s
0
i
else
s
...
...
src/util/strings.mli
View file @
d7320259
...
...
@@ -13,10 +13,6 @@
(** {2 Wrappers for deprecated string functions of OCaml stdlib} *)
val
create
:
int
->
string
val
copy
:
string
->
string
val
set
:
string
->
int
->
char
->
unit
val
lowercase
:
string
->
string
val
capitalize
:
string
->
string
val
uncapitalize
:
string
->
string
...
...
src/util/sysutil.ml
View file @
d7320259
...
...
@@ -17,22 +17,22 @@ let backup_file f =
end
let
channel_contents_fmt
cin
fmt
=
let
buff
=
String
.
mak
e
1024
'
'
in
let
buff
=
Bytes
.
creat
e
1024
in
let
n
=
ref
0
in
while
n
:=
input
cin
buff
0
1024
;
!
n
<>
0
do
Format
.
pp_print_string
fmt
(
if
!
n
=
1024
then
buff
Bytes
.
unsafe_to_string
buff
else
String
.
sub
buff
0
!
n
)
Bytes
.
sub_string
buff
0
!
n
)
done
let
channel_contents_buf
cin
=
let
buf
=
Buffer
.
create
1024
and
buff
=
String
.
mak
e
1024
'
'
in
let
buf
=
Buffer
.
create
1024
in
let
buff
=
Bytes
.
creat
e
1024
in
let
n
=
ref
0
in
while
n
:=
input
cin
buff
0
1024
;
!
n
<>
0
do
Buffer
.
add_sub
string
buf
buff
0
!
n
Buffer
.
add_sub
bytes
buf
buff
0
!
n
done
;
buf
...
...
@@ -83,7 +83,7 @@ let open_temp_file ?(debug=false) filesuffix usefile =
let
copy_file
from
to_
=
let
cin
=
open_in
from
in
let
cout
=
open_out
to_
in
let
buff
=
String
.
mak
e
1024
'
'
in
let
buff
=
Bytes
.
creat
e
1024
in
let
n
=
ref
0
in
while
n
:=
input
cin
buff
0
1024
;
!
n
<>
0
do
output
cout
buff
0
!
n
...
...
src/why3session/why3session_lib.ml
View file @
d7320259
...
...
@@ -279,7 +279,7 @@ let rec ask_yn () =
let
ask_yn_nonblock
~
callback
=
let
b
=
Buffer
.
create
3
in
let
s
=
String
s
.
create
1
in
let
s
=
Byte
s
.
create
1
in
Format
.
printf
"(y/n)@."
;
fun
()
->
match
Unix
.
select
[
Unix
.
stdin
]
[]
[]
0
.
with
...
...
@@ -288,8 +288,9 @@ let ask_yn_nonblock ~callback =
if
Unix
.
read
Unix
.
stdin
s
1
0
=
0
then
begin
(* EndOfFile *)
callback
false
;
false
end
else
begin
if
s
.
[
0
]
<>
'\n'
then
(
Buffer
.
add_char
b
s
.
[
0
];
true
)
let
c
=
Bytes
.
get
s
0
in
if
c
<>
'\n'
then
(
Buffer
.
add_char
b
c
;
true
)
else
match
Buffer
.
contents
b
with
|
"y"
->
callback
true
;
false
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment