package frama-c-luncov

  1. Overview
  2. Docs

Source file register.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

let add_label_support () =
  let hfile = Format.asprintf "%a" Filepath.pretty_abs
      (Options.Share.get_file "labels.h")
  in
  Kernel.CppExtraArgs.append_before ["-include "^hfile]

let main () =
  if Kernel.Files.is_empty () then Options.abort "no input file";
  (* initialize labels data and get labels filename *)
  let data = Data_labels.create () in
  let file = Filepath.to_string_rel (List.hd (Kernel.Files.get ())) in

  let labelsfile =
    if Options.LabelsFile.is_set () then
      Options.LabelsFile.get ()
    else
      (Filename.chop_suffix file ".c")^".labels"
  in

  (* initialize hyperlabels data and get hyperlabels filename *)
  let hdata = Data_hyperlabels.create () in
  let hyperlabelsfile =
    if Options.HyperlabelsFile.is_set () then
      Options.HyperlabelsFile.get ()
    else
      (Filename.chop_suffix file ".c")^".hyperlabels"
  in

  (* load label data if any *)
  let labels_before_stats =
    if Sys.file_exists labelsfile then
      (Data_labels.load data labelsfile; Some (Data_labels.get_stats data))
    else
      None
  in

  (* load hyperlabel data if any *)
  let hyperlabels_before_stats =
    if Sys.file_exists hyperlabelsfile then begin
      Options.result "hyperlabel file %s found.@." hyperlabelsfile;
      Data_hyperlabels.load hdata hyperlabelsfile;
      Some (Data_hyperlabels.get_stats hdata)
    end
    else begin
      Options.result "hyperlabel file %s NOT found. Hyp. coverage not measured @." hyperlabelsfile;
      None
    end
  in

  let force = Options.Force.get () in

  (* handle the actions *)
  if Options.Init.get () || Options.ForceInit.get () then
    Init.compute ~force:(Options.ForceInit.get ()) data;

  if Options.EVA.get () then
    (EVA.compute ~force data hdata);

  if Options.WP.get () then
    if Options.Multicore.get () <= 1 then
      Wp_singlecore.compute ~force data hdata
    else
      Wp_multicore.compute_multicore ~force data;

  if Options.VWAP.get () then
    (* Options.warning "WIP : TURNED OFF FOR NOW"; *)
    Vwap.compute ~force data hdata;

  begin
    match labels_before_stats with
    | None ->
      Options.feedback "label statistics@.%a" Data_labels.pp_stats (Data_labels.get_stats data)
    | Some before_stats ->
      Options.feedback "label statistics@.%a" Data_labels.pp_diff_stats (before_stats, Data_labels.get_stats data)
  end;

  begin
    match hyperlabels_before_stats with
    | None -> ()
    | Some before_stats ->
      Options.feedback "hyperlabel statistics@.%a" Data_hyperlabels.pp_diff_stats
        (before_stats, Data_hyperlabels.get_stats hdata);
      (* store hyperlabel data *)
      Data_hyperlabels.store hdata hyperlabelsfile;
      Options.feedback "hyperlabel data written to %s" hyperlabelsfile;
  end;

  (* store label data *)
  Data_labels.store data labelsfile;
  Options.feedback "label data written to %s" labelsfile;

  (* Store always true labels *)
  if Options.AlwaysTrue.get () then begin
    let dataAT = Data_labels.create () in
    let labelsfileAT = "AT" ^ labelsfile in
    if Options.Multicore.get() <= 1 then
      Wp_singlecore.computeAT ~force dataAT
    else
      Wp_multicore.compute_multicoreAT ~force data;
    Data_labels.storeAT dataAT labelsfileAT;
    Options.feedback "always true label data written to %s" labelsfileAT
  end;
  let t1 = Unix.gettimeofday () in
  if Options.Time.get() then
    Options.feedback "Execution time: %f s" (t1 -. !Commons.starting_time)
  else
    Options.feedback "Execution time: (disabled)"

let main_once, _ = State_builder.apply_once "LUncov.run" [] main

let run () =
  if Options.Enabled.get () then main_once ()

let turn_off_variadic () =
  if Kernel.VariadicTranslation.get () then begin
    Options.feedback "Turning off variadic translation.";
    Kernel.VariadicTranslation.off ()
  end

let setup_run () =
  if Options.Enabled.get () then begin
    Commons.starting_time := Unix.gettimeofday ();
    turn_off_variadic ();
    (* add header for labels *)
    add_label_support ();
  end

let setup_once, _ = State_builder.apply_once "LUncov.setup_run" [] setup_run

let () = Cmdline.run_after_configuring_stage setup_once

let () = Boot.Main.extend run