Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
Lustrec - public version
Manage
Activity
Members
Labels
Plan
Issues
0
Issue boards
Milestones
Iterations
Wiki
Requirements
Code
Merge requests
0
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Locked files
Build
Pipelines
Jobs
Pipeline schedules
Test cases
Artifacts
Deploy
Releases
Package Registry
Container Registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Code review analytics
Issue analytics
Insights
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Terms and privacy
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
LustreC
Lustrec - public version
Commits
ba8ebd50
Commit
ba8ebd50
authored
2 years ago
by
BRUN Lelio
Browse files
Options
Downloads
Patches
Plain Diff
formatting
parent
9e3867be
No related branches found
No related tags found
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
lustrec_tests/dune
+7
-4
7 additions, 4 deletions
lustrec_tests/dune
lustrec_tests/test.ml
+30
-24
30 additions, 24 deletions
lustrec_tests/test.ml
with
37 additions
and
28 deletions
lustrec_tests/dune
+
7
−
4
View file @
ba8ebd50
(env
(dev
(flags (:standard -w -32))))
(dev
(flags
(:standard -w -32))))
(test
(name test)
(libraries re unix yojson)
(deps
(:lus (glob_files *.lus))
(:lus
(glob_files *.lus))
(:cfg config.json)
(glob_files *)) ; to include `ignored` if its present
(glob_files *))
; to include `ignored` if its present
(action
(run %{test} %{project_root} %{bin:lustrec} %{cfg} "%{lus}")))
This diff is collapsed.
Click to expand it.
lustrec_tests/test.ml
+
30
−
24
View file @
ba8ebd50
open
Format
open
Unix
module
Y
=
Yojson
.
Basic
module
S
=
struct
...
...
@@ -55,10 +54,10 @@ let empty_report =
}
type
config
=
{
initial_timeout
:
int
;
optimization_level
:
int
;
ignored_file
:
string
option
;
results_directory
:
string
;
initial_timeout
:
int
;
optimization_level
:
int
;
ignored_file
:
string
option
;
results_directory
:
string
;
}
let
frama_c
=
"frama-c"
...
...
@@ -109,9 +108,7 @@ let wp_strategy_args =
let
frama_c_args
f
=
wp_args
@
(
f
::
"-then"
::
wp_strategy_args
)
let
frama_c_cmd
f
=
frama_c
::
frama_c_args
f
let
report_file
cfg
=
Filename
.
concat
cfg
.
results_directory
"report"
let
section
h
=
"# "
^
h
let
end_section
=
"##"
let
config_section
=
section
"CONFIG"
...
...
@@ -246,7 +243,9 @@ let parse_report cfg =
with
_
->
empty_report
let
pp_config
fmt
cfg
=
fprintf
fmt
"%s@;Optimization level: %s@;Frama-C options: %s@;%s@;"
fprintf
fmt
"%s@;Optimization level: %s@;Frama-C options: %s@;%s@;"
config_section
(
"O"
^
(
cfg
.
optimization_level
|>
string_of_int
))
(
String
.
concat
" "
wp_strategy_args
)
...
...
@@ -336,9 +335,11 @@ let print_results ok ko w n =
let
lustrec_params
cfg
f
=
[
"-acsl-spec"
;
"-d"
;
cfg
.
results_directory
;
"-O"
;
cfg
.
optimization_level
|>
string_of_int
;
f
"-d"
;
cfg
.
results_directory
;
"-O"
;
cfg
.
optimization_level
|>
string_of_int
;
f
;
]
let
compile
cfg
report
lustrec
fs
=
...
...
@@ -371,7 +372,10 @@ let compile cfg report lustrec fs =
else
if
is_ninit
report
f
then
ninit
report
else
let
cmd
=
Filename
.
quote_command
~
stderr
:
err_f
lustrec
(
lustrec_params
cfg
f
)
Filename
.
quote_command
~
stderr
:
err_f
lustrec
(
lustrec_params
cfg
f
)
in
let
ic
=
open_process_in
cmd
in
let
b
=
...
...
@@ -528,11 +532,12 @@ let read_config root =
let
tests_directory
=
Sys
.
getcwd
()
|>
Filename
.
basename
in
let
optimization_level
=
get_default
"optimization_level"
to_int
2
in
let
result_dir
=
root
^
"/../../results/"
in
(
try
Unix
.
mkdir
result_dir
0o755
with
_
->
()
);
(
try
Unix
.
mkdir
result_dir
0o755
with
_
->
()
);
let
results_directory
=
result_dir
^
tests_directory
^
"_"
^
(
if
optimization_level
<
0
then
"wo_optimization"
else
"O"
^
string_of_int
optimization_level
)
result_dir
^
tests_directory
^
"_"
^
if
optimization_level
<
0
then
"wo_optimization"
else
"O"
^
string_of_int
optimization_level
in
(
try
Unix
.
mkdir
results_directory
0o755
with
_
->
()
);
{
...
...
@@ -548,15 +553,16 @@ let () =
let
cfg
=
read_config
root
in
let
lus_fs
=
Sys
.
argv
.
(
4
)
|>
Re
.
Str
.(
split
(
regexp_string
" "
))
in
let
ignored_fs
=
Option
.
fold
~
none
:
[]
Option
.
fold
~
none
:
[]
~
some
:
(
fun
ignored_f
->
let
ic
=
open_in
ignored_f
in
let
rec
read
fs
=
try
read
(
input_line
ic
::
fs
)
with
End_of_file
->
fs
in
let
fs
=
read
[]
in
close_in
ic
;
fs
)
let
ic
=
open_in
ignored_f
in
let
rec
read
fs
=
try
read
(
input_line
ic
::
fs
)
with
End_of_file
->
fs
in
let
fs
=
read
[]
in
close_in
ic
;
fs
)
cfg
.
ignored_file
in
let
report
=
parse_report
cfg
in
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
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