From ba8ebd50ecdc4b4227984bdeb076b69e1ffe7937 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lb@leliobrun.net>
Date: Tue, 14 Mar 2023 12:45:16 +0900
Subject: [PATCH] formatting
---
lustrec_tests/dune | 11 +++++----
lustrec_tests/test.ml | 54 ++++++++++++++++++++++++-------------------
2 files changed, 37 insertions(+), 28 deletions(-)
diff --git a/lustrec_tests/dune b/lustrec_tests/dune
index 5b79b1ca..9b655ddd 100644
--- a/lustrec_tests/dune
+++ b/lustrec_tests/dune
@@ -1,13 +1,16 @@
(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}")))
diff --git a/lustrec_tests/test.ml b/lustrec_tests/test.ml
index abf18833..f4386925 100644
--- a/lustrec_tests/test.ml
+++ b/lustrec_tests/test.ml
@@ -1,6 +1,5 @@
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
--
GitLab