Project

General

Profile

Revision 86ae18b7 src/backends/Horn/horn_backend.ml

View differences:

src/backends/Horn/horn_backend.ml
48 48
    )
49 49
end
50 50

  
51

  
52
let load_file f =
53
  let ic = open_in f in
54
  let n = in_channel_length ic in
55
  let s = String.create n in
56
  really_input ic s 0 n;
57
  close_in ic;
58
  (s)
59

  
51 60
let print_type_definitions fmt =
52 61
  let cpt_type = ref 0 in
53 62
  Hashtbl.iter (fun typ decl ->
......
68 77
    | _        -> ()) type_table
69 78

  
70 79

  
71
let translate fmt basename prog machines =
80

  
81

  
82
let print_dep fmt prog =
83
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. extracting Horn libraries@,");
84
  fprintf fmt "; Statically linked libraries@";
85
  let dependencies = Corelang.get_dependencies prog in
86
  List.iter
87
    (fun dep ->
88
      let (local, s) = Corelang.dependency_of_top dep in
89
      let basename = ((if local then !Options.dest_dir else !Options.include_dir)) ^ s ^ ".smt2" in
90
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@[<v 0> Horn Library %s@," basename);
91
      let horn = load_file basename in
92
      fprintf fmt "@.%s@." horn;
93
    )
94
    dependencies
95

  
96
let check_sfunction mannot =
97
 (*Check if its an sfunction*)
98
  match mannot with
99
    [] -> false
100
  | [x] ->
101
     begin
102
       match x.annots with
103
         [] -> false
104
        |[(key,va)] ->
105
          begin
106
            match key with
107
              [] -> false
108
            | [x]  -> x == "c_code" || x =="matlab"
109
            | _ -> false
110
          end
111
        |(_,_)::_ -> false
112
     end
113
  | _::_ -> false
114

  
115
let translate fmt basename prog machines=
72 116
  (* We print typedef *)
117
  print_dep fmt prog; (*print static library e.g. math*)
73 118
  print_type_definitions fmt;
74
  List.iter (print_machine machines fmt) (List.rev machines);
119
  (*List.iter (print_machine machines fmt) (List.rev machines);*)
120
  List.iter(fun m ->
121
      let is_sfunction = check_sfunction m.mannot in
122
      if is_sfunction then(
123
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. detected sfunction: %s@," m.mname.node_id);
124
        print_sfunction machines fmt m
125
      ) else (
126
         print_machine machines fmt m)
127
         )
128
           (List.rev machines);
75 129
  main_print machines fmt
76 130

  
77 131
(* Local Variables: *)

Also available in: Unified diff