Aorai_test.ml 2.99 KB
Newer Older
1
2
3
4
5
6
(* Small script to test that the code generated by aorai can be parsed again
 * by frama-c.
 *)

open Kernel

7
8
module P = Plugin.Register
(struct
9
10
11
12
13
14
  let name = "aorai testing module"
  let shortname = "aorai-test"
  let help = "utility script for aorai regtests"
 end)

module TestNumber =
15
  P.Zero
16
17
18
19
20
21
22
    (struct
      let option_name = "-aorai-test-number"
      let help = "test number when multiple tests are run over the same file"
      let arg_name = "n"
     end)

module InternalWpShare =
23
  P.Filepath(
24
25
26
27
    struct
      let option_name = "-aorai-test-wp-share"
      let help = "use custom wp share dir (when in internal plugin mode)"
      let arg_name = "dir"
28
29
      let existence = Filepath.Must_exist
      let file_kind = "wp share directory"
30
31
32
    end)

module ProveAuxSpec =
33
  P.False(
34
35
36
37
38
39
40
41
42
    struct
      let option_name = "-aorai-test-prove-aux-spec"
      let help = "use WP + alt-ergo to prove that generated spec and body \
                  of auxiliary automata functions match"
    end)

let ok = ref false

let is_suffix suf str =
43
44
  let lsuf = String.length suf in
  let lstr = String.length str in
45
46
  if lstr <= lsuf then false
  else
47
    let estr = String.sub str (lstr - lsuf) lsuf in
48
49
50
51
52
53
54
    estr = suf

let extend () =
  let myrun =
    let run = !Db.Toplevel.run in
    fun f ->
      let my_project = Project.create "Reparsing" in
55
      let wp_compute_kf kf = Wp.VC.command (Wp.VC.generate_kf kf) in
56
57
58
59
60
      let check_auto_func kf =
        let name = Kernel_function.get_name kf in
        if Kernel_function.is_definition kf &&
           (is_suffix "_pre_func" name || is_suffix "_post_func" name)
        then
61
          wp_compute_kf kf
62
63
64
65
66
      in
      run f;
      let tmpfile =
        Filename.get_temp_dir_name () ^ "/aorai_" ^
        (Filename.chop_extension
67
           (Filename.basename (List.hd (Kernel.Files.get()):>string))) ^ "_" ^
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
        (string_of_int (TestNumber.get ())) ^ ".i"
      in
      let () =
        Extlib.safe_at_exit
          (fun () ->
             if Debug.get () >= 1 || not !ok then
               result "Keeping temp file %s" tmpfile
             else Extlib.safe_remove tmpfile)
      in
      let chan = open_out tmpfile in
      let fmt = Format.formatter_of_out_channel chan in
      File.pretty_ast ~prj:(Project.from_unique_name "aorai") ~fmt ();
      close_out chan;
      let selection =
        State_selection.of_list [ InternalWpShare.self; ProveAuxSpec.self ]
      in
      Project.copy ~selection my_project;
      Project.set_current my_project;
86
      Files.append_after [ Filepath.Normalized.of_string tmpfile ];
87
88
89
      Constfold.off ();
      Ast.compute();
      if ProveAuxSpec.get () then begin
90
91
92
        if InternalWpShare.is_set() then
          Wp.Wp_parameters.Share.set (InternalWpShare.get());
        Wp.Wp_parameters.Verbose.set 0;
93
        Globals.Functions.iter check_auto_func;
94
95
96
        Report.Register.print ();
      end else begin
        File.pretty_ast ();
97
98
99
100
101
102
      end;
      ok:=true (* no error, we can erase the file *)
  in
  Db.Toplevel.run := myrun

let () = extend ()