Project

General

Profile

« Previous | Next » 

Revision 2dd3d358

Added by Teme Kahsai about 5 years ago

making library statically link to horn backend

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 translate fmt basename prog machines=
72 97
  (* We print typedef *)
98
  print_dep fmt prog;
73 99
  print_type_definitions fmt;
74 100
  List.iter (print_machine machines fmt) (List.rev machines);
75 101
  main_print machines fmt

Also available in: Unified diff