Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
dfa1e773
Commit
dfa1e773
authored
4 years ago
by
Patrick Baudin
Browse files
Options
Downloads
Patches
Plain Diff
[Tests] adds EXIT directive to ptests
parent
c6a5b7bd
No related branches found
Branches containing commit
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
ptests/ptests.ml
+83
-37
83 additions, 37 deletions
ptests/ptests.ml
with
83 additions
and
37 deletions
ptests/ptests.ml
+
83
−
37
View file @
dfa1e773
...
@@ -596,7 +596,14 @@ end
...
@@ -596,7 +596,14 @@ end
(** configuration of a directory/test. *)
(** configuration of a directory/test. *)
type
cmd
=
{
toplevel
:
string
;
opts
:
string
;
macros
:
Macros
.
t
;
logs
:
string
list
;
timeout
:
string
}
type
cmd
=
{
toplevel
:
string
;
opts
:
string
;
macros
:
Macros
.
t
;
exit_code
:
string
option
;
logs
:
string
list
;
timeout
:
string
}
type
config
=
type
config
=
{
{
...
@@ -609,7 +616,8 @@ type config =
...
@@ -609,7 +616,8 @@ type config =
(** full path of the default toplevel. *)
(** full path of the default toplevel. *)
dc_filter
:
string
option
;
(** optional filter to apply to
dc_filter
:
string
option
;
(** optional filter to apply to
standard output *)
standard output *)
dc_commands
:
cmd
list
;
dc_exit_code
:
string
option
;
(** required exit code *)
dc_commands
:
cmd
list
;
(** toplevel full path, options to launch the toplevel on, and list
(** toplevel full path, options to launch the toplevel on, and list
of output files to monitor beyond stdout and stderr. *)
of output files to monitor beyond stdout and stderr. *)
dc_dont_run
:
bool
;
dc_dont_run
:
bool
;
...
@@ -630,8 +638,9 @@ let default_config () =
...
@@ -630,8 +638,9 @@ let default_config () =
dc_macros
=
default_macros
()
;
dc_macros
=
default_macros
()
;
dc_execnow
=
[]
;
dc_execnow
=
[]
;
dc_filter
=
None
;
dc_filter
=
None
;
dc_exit_code
=
None
;
dc_default_toplevel
=
!
toplevel_path
;
dc_default_toplevel
=
!
toplevel_path
;
dc_commands
=
[
{
toplevel
=
!
toplevel_path
;
opts
=
default_options
;
macros
=
Macros
.
empty
;
logs
=
[]
;
timeout
=
""
}
];
dc_commands
=
[
{
toplevel
=
!
toplevel_path
;
opts
=
default_options
;
macros
=
Macros
.
empty
;
exit_code
=
None
;
logs
=
[]
;
timeout
=
""
}
];
dc_dont_run
=
false
;
dc_dont_run
=
false
;
dc_framac
=
true
;
dc_framac
=
true
;
dc_default_log
=
[]
;
dc_default_log
=
[]
;
...
@@ -785,11 +794,11 @@ let config_options =
...
@@ -785,11 +794,11 @@ let config_options =
{
toplevel
=
current
.
dc_default_toplevel
;
{
toplevel
=
current
.
dc_default_toplevel
;
opts
=
s
;
opts
=
s
;
logs
=
current
.
dc_default_log
;
logs
=
current
.
dc_default_log
;
exit_code
=
current
.
dc_exit_code
;
macros
=
current
.
dc_macros
;
macros
=
current
.
dc_macros
;
timeout
=
current
.
dc_timeout
}
timeout
=
current
.
dc_timeout
}
in
in
{
current
with
{
current
with
(* dc_default_toplevel = !current_default_toplevel;*)
dc_default_log
=
!
default_parsing_env
.
current_default_log
;
dc_default_log
=
!
default_parsing_env
.
current_default_log
;
dc_commands
=
t
::
current
.
dc_commands
});
dc_commands
=
t
::
current
.
dc_commands
});
...
@@ -801,6 +810,7 @@ let config_options =
...
@@ -801,6 +810,7 @@ let config_options =
{
command
with
opts
=
make_custom_opts
command
.
opts
s
;
{
command
with
opts
=
make_custom_opts
command
.
opts
s
;
logs
=
command
.
logs
@
current
.
dc_default_log
;
logs
=
command
.
logs
@
current
.
dc_default_log
;
macros
=
current
.
dc_macros
;
macros
=
current
.
dc_macros
;
exit_code
=
current
.
dc_exit_code
;
timeout
=
current
.
dc_timeout
timeout
=
current
.
dc_timeout
})
})
!
default_parsing_env
.
current_default_cmds
!
default_parsing_env
.
current_default_cmds
...
@@ -814,6 +824,9 @@ let config_options =
...
@@ -814,6 +824,9 @@ let config_options =
"FILTER"
,
"FILTER"
,
(
fun
_
s
current
->
{
current
with
dc_filter
=
Some
s
});
(
fun
_
s
current
->
{
current
with
dc_filter
=
Some
s
});
"EXIT"
,
(
fun
_
s
current
->
{
current
with
dc_exit_code
=
Some
s
});
"GCC"
,
"GCC"
,
(
fun
_
_
acc
->
acc
);
(
fun
_
_
acc
->
acc
);
...
@@ -923,6 +936,7 @@ type toplevel_command =
...
@@ -923,6 +936,7 @@ type toplevel_command =
options
:
string
;
options
:
string
;
toplevel
:
string
;
toplevel
:
string
;
filter
:
string
option
;
filter
:
string
option
;
exit_code
:
int
;
directory
:
SubDir
.
t
;
directory
:
SubDir
.
t
;
n
:
int
;
n
:
int
;
execnow
:
bool
;
execnow
:
bool
;
...
@@ -941,7 +955,7 @@ type diff =
...
@@ -941,7 +955,7 @@ type diff =
|
Log_error
of
SubDir
.
t
(** directory *)
*
string
(** file *)
|
Log_error
of
SubDir
.
t
(** directory *)
*
string
(** file *)
type
cmps
=
type
cmps
=
|
Cmp_Toplevel
of
toplevel_command
|
Cmp_Toplevel
of
toplevel_command
*
bool
(** returns with the required exit_code *)
|
Cmp_Log
of
SubDir
.
t
(** directory *)
*
string
(** file *)
|
Cmp_Log
of
SubDir
.
t
(** directory *)
*
string
(** file *)
type
shared
=
type
shared
=
...
@@ -959,6 +973,7 @@ type shared =
...
@@ -959,6 +973,7 @@ type shared =
mutable
commands_finished
:
bool
;
mutable
commands_finished
:
bool
;
mutable
cmp_finished
:
bool
;
mutable
cmp_finished
:
bool
;
mutable
summary_time
:
float
;
mutable
summary_time
:
float
;
mutable
summary_ret
:
int
;
(* number of run with the required exit code *)
mutable
summary_run
:
int
;
mutable
summary_run
:
int
;
mutable
summary_ok
:
int
;
mutable
summary_ok
:
int
;
mutable
summary_log
:
int
;
mutable
summary_log
:
int
;
...
@@ -978,6 +993,7 @@ let shared =
...
@@ -978,6 +993,7 @@ let shared =
cmp_finished
=
false
;
cmp_finished
=
false
;
summary_time
=
(
Unix
.
times
()
)
.
Unix
.
tms_cutime
;
summary_time
=
(
Unix
.
times
()
)
.
Unix
.
tms_cutime
;
summary_run
=
0
;
summary_run
=
0
;
summary_ret
=
0
;
summary_ok
=
0
;
summary_ok
=
0
;
summary_log
=
0
}
summary_log
=
0
}
...
@@ -1167,7 +1183,7 @@ let command_string command =
...
@@ -1167,7 +1183,7 @@ let command_string command =
let
command_string
=
match
filter
with
let
command_string
=
match
filter
with
|
None
->
command_string
|
None
->
command_string
|
Some
filter
->
|
Some
filter
->
Printf
.
sprintf
"%s && %s < %s >%s && rm -f %s"
Printf
.
sprintf
"%s && %s < %s >%s && rm -f %s"
(* exit code ? *)
command_string
command_string
filter
filter
(
Filename
.
sanitize
stderr
)
(
Filename
.
sanitize
stderr
)
...
@@ -1243,34 +1259,38 @@ end
...
@@ -1243,34 +1259,38 @@ end
module
Report_run
=
Make_Report
(
struct
type
t
=
int
*
float
module
Report_run
=
Make_Report
(
struct
type
t
=
int
*
float
(* At some point will contain the running time*)
(* At some point will contain the running time*)
end
)
end
)
let
report_run
cmd
r
=
Report_run
.
record
cmd
r
let
report_run
cmp
r
=
Report_run
.
record
cmp
r
type
cmp
=
{
res
:
int
;
err
:
int
;
ret
:
bool
}
module
Report_cmp
=
Make_Report
(
struct
type
t
=
int
*
int
end
)
module
Report_cmp
=
Make_Report
(
struct
type
t
=
cmp
end
)
let
report_cmp
=
Report_cmp
.
record
let
report_cmp
=
Report_cmp
.
record
let
pretty_report
fmt
=
let
pretty_report
fmt
=
Report_run
.
iter
Report_run
.
iter
(
fun
test
(
_
run_result
,
time_result
)
->
(
fun
test
(
run_result
,
time_result
)
->
Format
.
fprintf
fmt
Format
.
fprintf
fmt
"<testcase classname=%S name=%S time=
\"
%f
\"
>%s</testcase>@."
"<testcase classname=%S name=%S time=
\"
%f
\"
>%s</testcase>@."
(
Filename
.
basename
(
SubDir
.
get
test
.
directory
))
test
.
file
time_result
(
Filename
.
basename
(
SubDir
.
get
test
.
directory
))
test
.
file
time_result
(
let
res
,
err
=
Report_cmp
.
find
test
in
(
let
{
res
;
err
;
ret
}
=
Report_cmp
.
find
test
in
Report_cmp
.
remove
test
;
Report_cmp
.
remove
test
;
(
if
res
=
0
&&
err
=
0
then
""
else
(
if
res
=
0
&&
err
=
0
&&
ret
then
""
else
Format
.
sprintf
"<failure type=
\"
Regression
\"
>%s</failure>"
Format
.
sprintf
"<failure type=
\"
Regression
\"
>%s</failure>"
(
if
res
=
1
then
"Stdout oracle difference"
(
if
not
ret
then
Format
.
sprintf
"Unexpected return code (returns %d instead of %d)"
run_result
test
.
exit_code
else
if
res
=
1
then
"Stdout oracle difference"
else
if
res
=
2
then
"Stdout System Error (missing oracle?)"
else
if
res
=
2
then
"Stdout System Error (missing oracle?)"
else
if
err
=
1
then
"Stderr oracle difference"
else
if
err
=
1
then
"Stderr oracle difference"
else
if
err
=
2
then
"Stderr System Error (missing oracle?)"
else
if
err
=
2
then
"Stderr System Error (missing oracle?)"
else
"Unexpected errror"
))));
else
"Unexpected errror"
))));
(* Test that were compared but not runned *)
(* Test that were compared but not runned *)
Report_cmp
.
iter
Report_cmp
.
iter
(
fun
test
(
res
,
err
)
->
(
fun
test
{
res
;
err
;
ret
}
->
Format
.
fprintf
fmt
Format
.
fprintf
fmt
"<testcase classname=%S name=%S>%s</testcase>@."
"<testcase classname=%S name=%S>%s</testcase>@."
(
Filename
.
basename
(
SubDir
.
get
test
.
directory
))
test
.
file
(
Filename
.
basename
(
SubDir
.
get
test
.
directory
))
test
.
file
(
if
res
=
0
&&
err
=
0
then
""
else
(
if
res
=
0
&&
err
=
0
&&
ret
then
""
else
Format
.
sprintf
"<failure type=
\"
Regression
\"
>%s</failure>"
Format
.
sprintf
"<failure type=
\"
Regression
\"
>%s</failure>"
(
if
res
=
1
then
"Stdout oracle difference"
(
if
not
ret
then
"Unexpected return code"
else
if
res
=
1
then
"Stdout oracle difference"
else
if
res
=
2
then
"Stdout System Error (missing oracle?)"
else
if
res
=
2
then
"Stdout System Error (missing oracle?)"
else
if
err
=
1
then
"Stderr oracle difference"
else
if
err
=
1
then
"Stderr oracle difference"
else
if
err
=
2
then
"Stderr System Error (missing oracle?)"
else
if
err
=
2
then
"Stderr System Error (missing oracle?)"
...
@@ -1281,8 +1301,9 @@ let xunit_report () =
...
@@ -1281,8 +1301,9 @@ let xunit_report () =
let
fmt
=
Format
.
formatter_of_out_channel
out
in
let
fmt
=
Format
.
formatter_of_out_channel
out
in
Format
.
fprintf
fmt
Format
.
fprintf
fmt
"<?xml version=
\"
1.0
\"
encoding=
\"
UTF-8
\"
?>\
"<?xml version=
\"
1.0
\"
encoding=
\"
UTF-8
\"
?>\
@
\n
<testsuite errors=
\"
0
\"
failures=
\"
%d
\"
name=
\"
%s
\"
tests=
\"
%d
\"
time=
\"
%f
\"
timestamp=
\"
%f
\"
>\
@
\n
<testsuite errors=
\"
%d
\"
failures=
\"
%d
\"
name=
\"
%s
\"
tests=
\"
%d
\"
time=
\"
%f
\"
timestamp=
\"
%f
\"
>\
@
\n
%t</testsuite>@."
@
\n
%t</testsuite>@."
(
shared
.
summary_run
-
shared
.
summary_ret
)
(
shared
.
summary_log
-
shared
.
summary_ok
)
(
shared
.
summary_log
-
shared
.
summary_ok
)
"Frama-C"
"Frama-C"
shared
.
summary_log
shared
.
summary_log
...
@@ -1315,18 +1336,29 @@ let do_command command =
...
@@ -1315,18 +1336,29 @@ let do_command command =
(* command string also replaces macros in logfiles names, which
(* command string also replaces macros in logfiles names, which
is useful for Examine as well. *)
is useful for Examine as well. *)
let
command_string
=
command_string
command
in
let
command_string
=
command_string
command
in
if
!
behavior
<>
Examine
let
summary_ret
=
then
begin
if
!
behavior
<>
Examine
if
!
verbosity
>=
1
then
begin
then
lock_printf
"%% launch %s@."
command_string
;
if
!
verbosity
>=
1
let
launch_result
=
launch
command_string
in
then
lock_printf
"%% launch %s@."
command_string
;
let
time
=
0
.
(* Individual time is difficult to compute correctly
let
launch_result
=
launch
command_string
in
for now, and currently unused *)
in
let
time
=
0
.
(* Individual time is difficult to compute correctly
report_run
command
(
launch_result
,
time
)
for now, and currently unused *)
in
end
;
report_run
command
(
launch_result
,
time
)
;
let
summary_ret
=
(
launch_result
=
command
.
exit_code
)
||
(
command
.
filter
<>
None
)
(* cannot checks exit code *)
in
if
not
summary_ret
then
lock_printf
"%% Unexpected code (returns %d instead of %d) for command: %s@."
launch_result
command
.
exit_code
command_string
;
summary_ret
end
else
false
in
lock
()
;
lock
()
;
if
summary_ret
then
shared
.
summary_ret
<-
succ
shared
.
summary_ret
;
shared
.
summary_run
<-
succ
shared
.
summary_run
;
shared
.
summary_run
<-
succ
shared
.
summary_run
;
Queue
.
push
(
Cmp_Toplevel
command
)
shared
.
cmps
;
Queue
.
push
(
Cmp_Toplevel
(
command
,
summary_ret
)
)
shared
.
cmps
;
List
.
iter
List
.
iter
(
fun
f
->
Queue
.
push
(
Cmp_Log
(
command
.
directory
,
f
))
shared
.
cmps
)
(
fun
f
->
Queue
.
push
(
Cmp_Log
(
command
.
directory
,
f
))
shared
.
cmps
)
command
.
log_files
;
command
.
log_files
;
...
@@ -1354,11 +1386,13 @@ let do_command command =
...
@@ -1354,11 +1386,13 @@ let do_command command =
else
begin
else
begin
let
rec
treat_cmd
=
function
let
rec
treat_cmd
=
function
Toplevel
cmd
->
Toplevel
cmd
->
shared
.
summary_run
<-
shared
.
summary_run
+
1
;
shared
.
summary_run
<-
succ
shared
.
summary_run
;
shared
.
summary_ret
<-
succ
shared
.
summary_ret
;
let
log_prefix
=
log_prefix
cmd
in
let
log_prefix
=
log_prefix
cmd
in
unlink
(
log_prefix
^
".res.log "
)
unlink
(
log_prefix
^
".res.log "
)
|
Target
(
execnow
,
cmds
)
->
|
Target
(
execnow
,
cmds
)
->
shared
.
summary_run
<-
succ
shared
.
summary_run
;
shared
.
summary_run
<-
succ
shared
.
summary_run
;
shared
.
summary_ret
<-
succ
shared
.
summary_ret
;
remove_execnow_results
execnow
;
remove_execnow_results
execnow
;
Queue
.
iter
treat_cmd
cmds
Queue
.
iter
treat_cmd
cmds
in
in
...
@@ -1391,6 +1425,7 @@ let do_command command =
...
@@ -1391,6 +1425,7 @@ let do_command command =
lock_printf
"%% launch %s@."
cmd
;
lock_printf
"%% launch %s@."
cmd
;
end
;
end
;
shared
.
summary_run
<-
succ
shared
.
summary_run
;
shared
.
summary_run
<-
succ
shared
.
summary_run
;
shared
.
summary_ret
<-
succ
shared
.
summary_ret
;
let
r
=
launch
cmd
in
let
r
=
launch
cmd
in
(* mark as already executed. For EXECNOW in test_config files,
(* mark as already executed. For EXECNOW in test_config files,
other instances (for example another test of the same
other instances (for example another test of the same
...
@@ -1490,12 +1525,15 @@ let compare_one_log_file dir file =
...
@@ -1490,12 +1525,15 @@ let compare_one_log_file dir file =
~
cmp_string
~
log_file
~
oracle_file
)
~
cmp_string
~
log_file
~
oracle_file
)
let
do_cmp
=
function
let
do_cmp
=
function
|
Cmp_Toplevel
cmp
->
|
Cmp_Toplevel
(
cmd
,
ret
)
->
let
log_prefix
=
log_prefix
cmp
in
let
log_prefix
=
log_prefix
cmd
in
let
oracle_prefix
=
oracle_prefix
cmp
in
let
oracle_prefix
=
oracle_prefix
cmd
in
let
res
=
compare_one_file
cmp
log_prefix
oracle_prefix
Res
in
let
cmp
=
{
res
=
compare_one_file
cmd
log_prefix
oracle_prefix
Res
;
let
err
=
compare_one_file
cmp
log_prefix
oracle_prefix
Err
in
err
=
compare_one_file
cmd
log_prefix
oracle_prefix
Err
;
report_cmp
cmp
(
res
,
err
)
ret
}
in
report_cmp
cmd
cmp
|
Cmp_Log
(
dir
,
f
)
->
|
Cmp_Log
(
dir
,
f
)
->
ignore
(
compare_one_log_file
dir
f
)
ignore
(
compare_one_log_file
dir
f
)
...
@@ -1741,10 +1779,17 @@ let dispatcher () =
...
@@ -1741,10 +1779,17 @@ let dispatcher () =
let
i
=
ref
0
in
let
i
=
ref
0
in
let
e
=
ref
0
in
let
e
=
ref
0
in
let
nb_files
=
List
.
length
config
.
dc_commands
in
let
nb_files
=
List
.
length
config
.
dc_commands
in
let
make_toplevel_cmd
{
toplevel
;
opts
=
options
;
logs
=
log_files
;
macros
;
timeout
}
=
let
make_toplevel_cmd
{
toplevel
;
opts
=
options
;
logs
=
log_files
;
macros
;
exit_code
;
timeout
}
=
let
n
=
!
i
in
let
n
=
!
i
in
{
file
;
options
;
toplevel
;
nb_files
;
directory
;
n
;
log_files
;
{
file
;
options
;
toplevel
;
nb_files
;
directory
;
n
;
log_files
;
filter
=
config
.
dc_filter
;
macros
;
filter
=
config
.
dc_filter
;
macros
;
exit_code
=
begin
match
exit_code
with
|
None
->
0
|
Some
exit_code
->
try
int_of_string
exit_code
with
|
_
->
Format
.
eprintf
"@[%s: integer required for directive EXIT: %s (defaults to 0)@]@."
file
exit_code
;
0
end
;
execnow
=
false
;
timeout
;
execnow
=
false
;
timeout
;
}
}
in
in
...
@@ -1755,6 +1800,7 @@ let dispatcher () =
...
@@ -1755,6 +1800,7 @@ let dispatcher () =
log_files
=
[]
;
log_files
=
[]
;
options
=
""
;
options
=
""
;
toplevel
=
s
;
toplevel
=
s
;
exit_code
=
0
;
n
=
!
e
;
n
=
!
e
;
directory
=
directory
;
directory
=
directory
;
filter
=
config
.
dc_filter
;
filter
=
config
.
dc_filter
;
...
@@ -1848,12 +1894,12 @@ let () =
...
@@ -1848,12 +1894,12 @@ let () =
Thread
.
join
diff_id
;
Thread
.
join
diff_id
;
if
!
behavior
=
Run
if
!
behavior
=
Run
then
then
lock_printf
"%% Diffs finished. Summary:@
\n
Run
=
%d@
\n
Ok = %d of %d@
\n
Time = %f s.@."
lock_printf
"%% Diffs finished. Summary:@
\n
Run
= %d of
%d@
\n
Ok = %d of %d@
\n
Time = %f s.@."
shared
.
summary_run
shared
.
summary_ok
shared
.
summary_log
shared
.
summary_ret
shared
.
summary_run
shared
.
summary_ok
shared
.
summary_log
((
Unix
.
times
()
)
.
Unix
.
tms_cutime
-.
shared
.
summary_time
);
((
Unix
.
times
()
)
.
Unix
.
tms_cutime
-.
shared
.
summary_time
);
xunit_report
()
;
xunit_report
()
;
let
error_code
=
let
error_code
=
if
!
do_error_code
&&
shared
.
summary_log
<>
shared
.
summary_ok
if
!
do_error_code
&&
((
shared
.
summary_log
<>
shared
.
summary_ok
)
||
(
shared
.
summary_ret
<>
shared
.
summary_run
))
then
1
then
1
else
0
else
0
in
in
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment