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
d3e8aed3
Commit
d3e8aed3
authored
3 years ago
by
Patrick Baudin
Browse files
Options
Downloads
Patches
Plain Diff
[Ptests] Adds SCRIPT directive
parent
b52baf87
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
ptests/ptests.ml
+47
-43
47 additions, 43 deletions
ptests/ptests.ml
with
47 additions
and
43 deletions
ptests/ptests.ml
+
47
−
43
View file @
d3e8aed3
...
...
@@ -297,9 +297,10 @@ let example_msg =
DONTRUN: @[<v 0># Ignores the file.@]@ \
EXECNOW: ([LOG|BIN] <file>)+ <command> @[<v 0># Defines the command to execute to build a 'LOG' (textual) 'BIN' (binary) targets.@ \
# Note: the textual targets are compared to oracles.@]@ \
MODULE: <module>... @[<v 0># Compile the module and set the @PTEST_MODULE@ macro@]@ \
LIBS: <module>... @[<v 0># Don't compile the module but set the @PTEST_LIBS@ macro@]@ \
MODULE: <module>... @[<v 0># Compile the module and set the @PTEST_MODULE@ macro
.
@]@ \
LIBS: <module>... @[<v 0># Don't compile the module but set the @PTEST_LIBS@ macro
.
@]@ \
PLUGIN: <plugin>... @[<v 0># Set the @PTEST_PLUGIN@ macro.@]@ \
SCRIPT: <script>... @[<v 0># Set the @PTEST_SCRIPT@ macro.@]@ \
LOG: <file>... @[<v 0># Defines targets built by the next sub-test command.@]@ \
CMD: <command> @[<v 0># Defines the command to execute for all tests in order to get results to be compared to oracles.@]@ \
OPT: <options> @[<v 0># Defines a sub-test using the 'CMD' definition: <command> <options>@]@ \
...
...
@@ -333,16 +334,18 @@ let example_msg =
@@PTEST_CONFIG@@ # Test configuration suffix.@ \
@@PTEST_RESULT@@ # Shorthand alias to '@@PTEST_DIR@@/result@@PTEST_CONFIG@@' (the result directory dedicated to the tested configuration).@ \
@@PTEST_ORACLE@@ # Basename of the current oracle file (macro only usable in FILTER directives).@ \
@@PTEST_LIBS@@ # Current list of module defined by the LIBS directive.@ \
@@PTEST_MODULE@@ # Current list of module defined by the MODULE directive.@ \
@@PTEST_LIBS@@ # Current list of module
s
defined by the LIBS directive.@ \
@@PTEST_MODULE@@ # Current list of module
s
defined by the MODULE directive.@ \
@@PTEST_PLUGIN@@ # Current list of plugins defined by the PLUGIN directive.@ \
@@PTEST_SCRIPT@@ # Current list of ML scripts defined by the SCRIPT directive.@ \
@]@ \
Other macros can only be used in test commands (CMD and EXECNOW directives):@ \
@@PTEST_DEFAULT_OPTIONS@@ # The default option list: %s@ \
@@PTEST_LOAD_LIBS@@ # The '-load-module' option related to the LIBS directive.@ \
@@PTEST_LOAD_MODULE@@ # The '-load-module' option related to the MODULE directive.@ \
@@PTEST_LOAD_PLUGIN@@ # The '-load-module' option related to the PLUGIN directive.@ \
@@PTEST_LOAD_OPTIONS@@ # Shorthand alias to '@@PTEST_LOAD_PLUGIN@@ @@PTEST_LOAD_LIBS@@ @@PTEST_LOAD_MODULE@@' .@ \
@@PTEST_LOAD_SCRIPT@@ # The '-load-script' option related to the SCRIPT directive.@ \
@@PTEST_LOAD_OPTIONS@@ # Shorthand alias to '@@PTEST_LOAD_PLUGIN@@ @@PTEST_LOAD_LIBS@@ @@PTEST_LOAD_MODULE@@ @@PTEST_LOAD_SCRIPT@@' .@ \
@@PTEST_OPTIONS@@ # The current list of options related to OPT and STDOPT directives (for CMD directives).@ \
@@frama-c@@ # Shortcut defined as follow: %s@ \
@@frama-c-cmd@@ # Shortcut defined as follow: %s@ \
...
...
@@ -643,8 +646,8 @@ struct
let
has_ptest_opt
=
ref
false
in
let
has_ptest_options
=
ref
false
in
let
has_frama_c_exe
=
ref
false
in
if
!
verbosity
>=
3
then
lock_printf
"%% Expand: %s@."
s
;
if
!
verbosity
>=
4
then
print_macros
macros
;
if
!
verbosity
>=
4
then
lock_printf
"%% Expand: %s@."
s
;
if
!
verbosity
>=
5
then
print_macros
macros
;
let
rec
aux
s
=
let
expand_macro
=
function
|
Str
.
Text
s
->
s
...
...
@@ -658,9 +661,9 @@ struct
|
"PTEST_OPTIONS"
->
has_ptest_options
:=
true
|
"frama-c-exe"
->
has_frama_c_exe
:=
true
|
_
->
()
);
if
!
verbosity
>=
4
then
lock_printf
"%% - macro is %s
\n
%!"
macro
;
if
!
verbosity
>=
5
then
lock_printf
"%% - macro is %s
\n
%!"
macro
;
let
replacement
=
find
macro
macros
in
if
!
verbosity
>=
3
then
if
!
verbosity
>=
4
then
lock_printf
"%% - replacement for %s is %s
\n
%!"
macro
replacement
;
aux
replacement
with
...
...
@@ -674,7 +677,7 @@ struct
Mutex
.
lock
str_mutex
;
let
r
=
aux
s
in
Mutex
.
unlock
str_mutex
;
if
!
verbosity
>=
3
then
lock_printf
"%% Expansion result: %s@."
r
;
if
!
verbosity
>=
4
then
lock_printf
"%% Expansion result: %s@."
r
;
{
has_ptest_file
=
!
has_ptest_file
;
has_ptest_opt
=
!
has_ptest_opt
;
has_frama_c_exe
=
!
has_frama_c_exe
;
...
...
@@ -692,7 +695,7 @@ struct
let
add_list
l
map
=
List
.
fold_left
(
fun
acc
(
k
,
v
)
->
if
!
verbosity
>=
3
then
if
!
verbosity
>=
4
then
lock_printf
"%% - Adds macro %s with definition %s@."
k
v
;
add
k
v
acc
)
map
l
...
...
@@ -738,6 +741,7 @@ type config =
dc_execnow
:
execnow
list
;
(** command to be launched before
the toplevel(s)
*)
dc_load_script
:
string
;
(** load libs options. *)
dc_load_libs
:
string
;
(** load libs options. *)
dc_load_module
:
string
;
(** load module options. *)
dc_cmxs_module
:
StringSet
.
t
;
(** compiled modules. *)
...
...
@@ -804,6 +808,7 @@ end = struct
"PTEST_LIBS"
,
""
;
"PTEST_MODULE"
,
""
;
"PTEST_PLUGIN"
,
""
;
"PTEST_SCRIPT"
,
""
;
]
in
Macros
.
add_list
l
Macros
.
empty
...
...
@@ -819,6 +824,7 @@ end = struct
dc_dont_run
=
false
;
dc_load_module
=
""
;
dc_load_libs
=
""
;
dc_load_script
=
""
;
dc_cmxs_module
=
StringSet
.
empty
;
dc_framac
=
true
;
dc_default_log
=
[]
;
...
...
@@ -932,7 +938,7 @@ end = struct
try
Str
.
matched_group
3
s
with
Not_found
->
(* empty text *)
""
in
Mutex
.
unlock
str_mutex
;
if
!
verbosity
>=
3
then
if
!
verbosity
>=
4
then
lock_printf
"%% - New macro %s with definition %s
\n
%!"
name
def
;
{
current
with
dc_macros
=
Macros
.
add_expand
name
def
current
.
dc_macros
}
end
else
begin
...
...
@@ -941,12 +947,12 @@ end = struct
current
end
let
update_module_libs
s
=
let
update_module_libs
_name
s
=
"@PTEST_DIR@/"
^
(
Filename
.
remove_extension
s
)
^
(
if
!
use_byte
then
".cmo"
else
".cmxs"
)
let
add_make_modules
~
file
dir
deps
current
=
let
deps
,
current
=
List
.
fold_left
(
fun
((
deps
,
curr
)
as
acc
)
s
->
let
s
=
update_module_libs
s
in
let
s
=
update_module_libs
_name
s
in
if
StringSet
.
mem
s
curr
.
dc_cmxs_module
then
acc
else
(
deps
^
" "
^
s
)
,
...
...
@@ -959,44 +965,40 @@ end = struct
config_exec
~
warn
:
false
~
once
:
true
~
file
dir
(
make_cmd
^
deps
)
current
end
let
update_m
odule_libs_
macro
s
p
def
p
load_def
modules
macro
s
=
let
update_m
acros
update_name
load_option
macro
_
def
macro_
load_def
current
module
s
=
let
def
=
String
.
concat
","
modules
in
let
load_def
=
if
String
.(
def
=
""
)
then
""
else
"-
load
-module="
^
(
String
.
concat
","
(
List
.
map
update_
module_libs
modules
))
load
_option
^
(
String
.
concat
","
(
List
.
map
update_
name
modules
))
in
Macros
.
add_list
[
pdef
,
def
;
pload_def
,
load_def
;
]
macros
if
!
verbosity
>=
3
then
Format
.
printf
"%% %s: %s@."
macro_def
def
;
let
dc_macros
=
Macros
.
add_list
[
macro_def
,
def
;
macro_load_def
,
load_def
;
]
current
.
dc_macros
in
{
current
with
dc_macros
}
let
update_script_name
s
=
"@PTEST_DIR@/"
^
(
Filename
.
remove_extension
s
)
^
".ml"
let
update_module_macros
=
update_m
odule_libs_macros
"PTEST_MODULE"
"PTEST_LOAD_MODULE"
update_m
acros
update_module_libs_name
"-load-module="
"PTEST_MODULE"
"PTEST_LOAD_MODULE"
let
update_libs_macros
=
update_module_libs_macros
"PTEST_LIBS"
"PTEST_LOAD_LIBS"
update_macros
update_module_libs_name
"-load-module="
"PTEST_LIBS"
"PTEST_LOAD_LIBS"
let
update_script_macros
=
update_macros
update_script_name
"-load-script="
"PTEST_SCRIPT"
"PTEST_LOAD_SCRIPT"
let
update_plugin_macros
=
update_macros
(
fun
name
->
name
)
"-load-module="
"PTEST_PLUGIN"
"PTEST_LOAD_PLUGIN"
let
config_module
~
file
dir
s
current
=
let
deps
=
str_split_list
(
Macros
.
expand
current
.
dc_macros
s
)
in
let
current
=
{
current
with
dc_macros
=
update_module_macros
deps
current
.
dc_macros
}
in
let
current
=
update_module_macros
current
deps
in
add_make_modules
~
file
dir
deps
current
let
config_libs
~
file
dir
s
current
=
let
config_libs
_script_plugin
update
~
file
dir
s
current
=
let
deps
=
str_split_list
(
Macros
.
expand
current
.
dc_macros
s
)
in
let
current
=
{
current
with
dc_macros
=
update_libs_macros
deps
current
.
dc_macros
}
in
current
let
update_plugin_macros
plugins
macros
=
let
def
=
String
.
concat
","
plugins
in
let
load_def
=
if
String
.(
def
=
""
)
then
""
else
(* the option "-load-plugin" will be used in a future version for PLUGIN *)
"-load-module="
^
def
in
Macros
.
add_list
[
"PTEST_PLUGIN"
,
def
;
"PTEST_LOAD_PLUGIN"
,
load_def
;
]
macros
let
config_plugins
~
file
dir
s
current
=
let
deps
=
str_split_list
(
Macros
.
expand
current
.
dc_macros
s
)
in
{
current
with
dc_macros
=
update_plugin_macros
deps
current
.
dc_macros
}
update
current
deps
let
config_options
=
[
"CMD"
,
...
...
@@ -1073,9 +1075,9 @@ end = struct
"MODULE"
,
config_module
;
"LIBS"
,
config_libs
;
"PLUGIN"
,
config_
plugin
s
;
"LIBS"
,
config_libs
_script_plugin
update_libs_macros
;
"SCRIPT"
,
config_libs_script_plugin
update_script_macros
;
"PLUGIN"
,
config_
libs_script_plugin
update_plugin_macro
s
;
"LOG"
,
(
fun
~
file
:_
_
s
current
->
{
current
with
dc_default_log
=
s
::
current
.
dc_default_log
});
...
...
@@ -1320,6 +1322,7 @@ end = struct
let
ptest_load_plugin
=
Macros
.
get
"PTEST_LOAD_PLUGIN"
cmd
.
macros
in
let
ptest_load_module
=
Macros
.
get
"PTEST_LOAD_MODULE"
cmd
.
macros
in
let
ptest_load_libs
=
Macros
.
get
"PTEST_LOAD_LIBS"
cmd
.
macros
in
let
ptest_load_script
=
Macros
.
get
"PTEST_LOAD_SCRIPT"
cmd
.
macros
in
let
macros
=
[
"PTEST_CONFIG"
,
ptest_config
;
"PTEST_DIR"
,
SubDir
.
get
cmd
.
directory
;
...
...
@@ -1332,7 +1335,8 @@ end = struct
"PTEST_LOAD_OPTIONS"
,
(
String
.
concat
" "
[
ptest_load_plugin
;
ptest_load_libs
;
ptest_load_module
])
ptest_load_module
;
ptest_load_script
;
])
]
in
let
macros
=
Macros
.
add_list
macros
cmd
.
macros
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