Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
bc3b1ccc
Commit
bc3b1ccc
authored
Jun 11, 2010
by
Francois Bobot
Browse files
cmdline : remplacement des options -t -> -T -g -> -G -T -> -t -M -> -m
parent
af6fdb6d
Changes
2
Hide whitespace changes
Inline
Side-by-side
Makefile.in
View file @
bc3b1ccc
...
...
@@ -493,11 +493,11 @@ BENCH_PLUGINS_CMXS := $(BENCH_PLUGINS_CMO:.cmo=.cmxs)
bench_plugins
::
$(BENCH_PLUGINS_CMO) $(BENCH_PLUGINS_CMXS) byte $(TOOLS)
bin/why.byte
-D
bench/plugins/helloworld.drv
\
tests/test-jcf.why
-
t
Test
-
g
G
tests/test-jcf.why
-
T
Test
-
G
G
bin/why.
$(OCAMLBEST)
-D
bench/plugins/helloworld.drv
\
tests/test-jcf.why
-
t
Test
-
g
G
tests/test-jcf.why
-
T
Test
-
G
G
bin/why.
$(OCAMLBEST)
-D
bench/plugins/simplify_array.drv
\
tests/test-jcf.why
-
t
Test_simplify_array
-
g
G
tests/test-jcf.why
-
T
Test_simplify_array
-
G
G
###############
# test targets
...
...
@@ -509,9 +509,9 @@ test2: bin/why.byte $(TOOLS)
test
:
bin/why.byte $(TOOLS)
mkdir
-p
output_why3
bin/why.byte
-D
drivers/why3.drv
-o
output_why3 tests/test-jcf.why
bin/why.byte
-D
drivers/alt_ergo.drv tests/test-jcf.why
-
t
Test
-
g
G
bin/why.byte
-P
alt-ergo
--timelimit
3 tests/test-jcf.why
-
t
Test
-
g
G
bin/why.byte
-D
drivers/coq.drv tests/test-jcf.why
-
t
Test
-
g
G
bin/why.byte
-D
drivers/alt_ergo.drv tests/test-jcf.why
-
T
Test
-
G
G
bin/why.byte
-P
alt-ergo
--timelimit
3 tests/test-jcf.why
-
T
Test
-
G
G
bin/why.byte
-D
drivers/coq.drv tests/test-jcf.why
-
T
Test
-
G
G
echo
bin/why.byte
-P
alt-ergo
--timelimit
1
--prove
theories/real.why
@
printf
"*** Checking Coq file generation ***
\\
n"
@
mkdir
-p
output_coq
...
...
@@ -521,7 +521,7 @@ test: bin/why.byte $(TOOLS)
floating_point.Test array.TestBv32
\
;
do
\
printf
"Generating Coq file for
$$
i
\\
n"
&&
\
bin/why.byte
-P
coq
-o
output_coq
-
t
$$
i
;
done
bin/why.byte
-P
coq
-o
output_coq
-
T
$$
i
;
done
@
printf
"*** Checking Coq compilation ***
\\
n"
@
for
i
in
output_coq/
*
.v
;
do
printf
"coq
$$
i
\\
n"
&&
coqc
$$
i
;
done
...
...
src/main.ml
View file @
bc3b1ccc
...
...
@@ -29,7 +29,7 @@ open Trans
let
usage_msg
=
sprintf
"Usage: %s [options] [[file|-] \
[-a <transform> -
t
<theory> [-
g
<goal>]...]...]..."
[-a <transform> -
T
<theory> [-
G
<goal>]...]...]..."
(
Filename
.
basename
Sys
.
argv
.
(
0
))
let
opt_queue
=
Queue
.
create
()
...
...
@@ -52,7 +52,7 @@ let add_opt_theory =
in
match
!
opt_input
,
p
with
|
None
,
[]
->
eprintf
"Option '-
t
'/'--theory' with a non-qualified \
eprintf
"Option '-
T
'/'--theory' with a non-qualified \
argument requires an input file.@."
;
exit
1
|
Some
tlist
,
[]
->
...
...
@@ -69,7 +69,7 @@ let add_opt_theory =
let
add_opt_goal
x
=
match
!
opt_theory
with
|
None
->
eprintf
"Option '-
g
'/'--goal' requires a theory.@."
;
eprintf
"Option '-
G
'/'--goal' requires a theory.@."
;
exit
1
|
Some
glist
->
let
l
=
Str
.
split
(
Str
.
regexp
"
\\
."
)
x
in
...
...
@@ -101,14 +101,14 @@ let opt_debug = ref false
let
option_list
=
Arg
.
align
[
"-"
,
Arg
.
Unit
(
fun
()
->
add_opt_file
"-"
)
,
" Read the input file from stdin"
;
"-
t
"
,
Arg
.
String
add_opt_theory
,
"-
T
"
,
Arg
.
String
add_opt_theory
,
"<theory> Select <theory> in the input file or in the library"
;
"--theory"
,
Arg
.
String
add_opt_theory
,
" same as -
t
"
;
"-
g
"
,
Arg
.
String
add_opt_goal
,
" same as -
T
"
;
"-
G
"
,
Arg
.
String
add_opt_goal
,
"<goal> Select <goal> in the last selected theory"
;
"--goal"
,
Arg
.
String
add_opt_goal
,
" same as -
g
"
;
" same as -
G
"
;
"-C"
,
Arg
.
String
(
fun
s
->
opt_config
:=
Some
s
)
,
"<file> Read configuration from <file>"
;
"--config"
,
Arg
.
String
(
fun
s
->
opt_config
:=
Some
s
)
,
...
...
@@ -127,14 +127,14 @@ let option_list = Arg.align [
"<format> Input format (default:
\"
why
\"
)"
;
"--format"
,
Arg
.
String
(
fun
s
->
opt_parser
:=
Some
s
)
,
" same as -F"
;
"-
T
"
,
Arg
.
Int
(
fun
i
->
opt_timelimit
:=
Some
i
)
,
"-
t
"
,
Arg
.
Int
(
fun
i
->
opt_timelimit
:=
Some
i
)
,
"<sec> Set the prover's time limit (default=10, no limit=0)"
;
"--timelimit"
,
Arg
.
Int
(
fun
i
->
opt_timelimit
:=
Some
i
)
,
" same as -
T
"
;
"-
M
"
,
Arg
.
Int
(
fun
i
->
opt_memlimit
:=
Some
i
)
,
" same as -
t
"
;
"-
m
"
,
Arg
.
Int
(
fun
i
->
opt_memlimit
:=
Some
i
)
,
"<MiB> Set the prover's memory limit (default: no limit)"
;
"--memlimit"
,
Arg
.
Int
(
fun
i
->
opt_timelimit
:=
Some
i
)
,
" same as -
M
"
;
" same as -
m
"
;
"-D"
,
Arg
.
String
(
fun
s
->
opt_driver
:=
Some
s
)
,
"<file> Specify a prover's driver (conflicts with -P)"
;
"--driver"
,
Arg
.
String
(
fun
s
->
opt_driver
:=
Some
s
)
,
...
...
@@ -219,11 +219,11 @@ let () =
exit
1
end
;
if
!
opt_timelimit
<>
None
then
begin
eprintf
"Option '-
T
'/'--timelimit' requires a prover.@."
;
eprintf
"Option '-
t
'/'--timelimit' requires a prover.@."
;
exit
1
end
;
if
!
opt_memlimit
<>
None
then
begin
eprintf
"Option '-
M
'/'--memlimit' requires a prover.@."
;
eprintf
"Option '-
m
'/'--memlimit' requires a prover.@."
;
exit
1
end
;
if
!
opt_driver
=
None
&&
not
!
opt_print_namespace
then
...
...
Write
Preview
Supports
Markdown
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