Project

General

Profile

Revision 58a463e7

View differences:

src/backends/C/c_backend.ml
64 64
    end
65 65
  )
66 66

  
67
let translate_to_c header source_lib source_main makefile basename prog machines dependencies =
67
let translate_to_c header source_lib source_main makefile basename prog machines dependencies  =
68 68

  
69 69
  match !Options.spec with
70 70
  | "no" -> begin
......
78 78
    let module SourceMain = C_backend_main.Main (SourceMainMod) in
79 79
    let module Makefile = C_backend_makefile.Main (MakefileMod) in
80 80
        
81
    let funs = Header.print_alloc_header, Source.print_lib_c, SourceMain.print_main_c, Makefile.print_makefile in
82
    gen_files funs basename prog machines dependencies header source_lib source_main makefile machines
81
    let funs = 
82
      Header.print_alloc_header, 
83
      Source.print_lib_c, 
84
      SourceMain.print_main_c, 
85
      Makefile.print_makefile 
86
    in
87
    gen_files 
88
      funs basename prog machines dependencies 
89
      header source_lib source_main makefile machines
83 90

  
84 91
  end
85 92
  | "acsl" -> begin
......
94 101
    let module SourceMain = C_backend_main.Main (SourceMainMod) in
95 102
    let module Makefile = C_backend_makefile.Main (MakefileMod) in
96 103
        
97
    let funs = Header.print_alloc_header, Source.print_lib_c, SourceMain.print_main_c, Makefile.print_makefile in
98
    gen_files funs basename prog machines dependencies header source_lib source_main makefile machines
104
    let funs = 
105
      Header.print_alloc_header, 
106
      Source.print_lib_c,
107
      SourceMain.print_main_c,
108
      Makefile.print_makefile 
109
    in
110
    gen_files
111
      funs basename prog machines dependencies
112
      header source_lib source_main makefile machines
99 113

  
100 114
  end
101 115
  | "c" -> begin
src/backends/C/c_backend_common.ml
343 343
    
344 344
    
345 345

  
346
let print_import_prototype fmt (_, s, _) =
346
let print_import_prototype fmt (Dep (_, s, _, _)) =
347 347
  fprintf fmt "#include \"%s.h\"@," s
348 348

  
349
let print_import_alloc_prototype fmt (_, s, _) =
350
  fprintf fmt "#include \"%s_alloc.h\"@," s
349
let print_import_alloc_prototype fmt (Dep (_, s, _, stateful)) =
350
  if stateful then
351
    fprintf fmt "#include \"%s_alloc.h\"@," s
351 352

  
352
let print_extern_alloc_prototypes fmt (_,_, header) =
353
let print_extern_alloc_prototypes fmt (Dep (_,_, header,_)) =
353 354
  List.iter (fun decl -> match decl.top_decl_desc with
354 355
  | ImportedNode ind when not ind.nodei_stateless ->
355 356
    let static = List.filter (fun v -> v.var_dec_const) ind.nodei_inputs
src/backends/C/c_backend_header.ml
294 294
    (* Import the header *)
295 295
    fprintf header_fmt "/* Import header from %s */@." basename;
296 296
    fprintf header_fmt "@[<v>";
297
    print_import_prototype header_fmt (true, basename, []);
297
    print_import_prototype header_fmt (Dep (true, basename, [], true (* assuming it is staful *) ));
298 298
    fprintf header_fmt "@]@.";
299 299
    fprintf header_fmt "/* Import dependencies */@.";
300 300
    fprintf header_fmt "@[<v>";
......
336 336
    fprintf header_fmt "/* Import dependencies */@.";
337 337
    fprintf header_fmt "@[<v>";
338 338
    List.iter
339
      (fun dep -> let (local, s) = dependency_of_top dep in print_import_prototype header_fmt (local, s, []))
339
      (fun dep -> 
340
	let (local, s) = dependency_of_top dep in 
341
	print_import_prototype header_fmt (Dep (local, s, [], true (* assuming it is stateful *))))
340 342
      dependencies;
341 343
    fprintf header_fmt "@]@.";
342 344
    fprintf header_fmt "/* Types definitions */@.";
src/backends/C/c_backend_main.ml
110 110
  fprintf fmt "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.h\"@." Version.include_path 
111 111

  
112 112

  
113
let print_main_c main_fmt main_machine basename prog machines dependencies =
113
let print_main_c main_fmt main_machine basename prog machines _ (*dependencies*) =
114 114
  print_main_header main_fmt;
115 115
  fprintf main_fmt "#include <stdlib.h>@.#include <assert.h>@.";
116
  print_import_alloc_prototype main_fmt (true, basename, []);
116
  print_import_alloc_prototype main_fmt (Dep (true, basename, [], true (* assuming it is stateful*) ));
117 117
  pp_print_newline main_fmt ();
118 118

  
119 119
  (* Print the svn version number and the supported C standard (C90 or C99) *)
src/backends/C/c_backend_makefile.ml
34 34
    
35 35

  
36 36
let compiled_dependencies dep = 
37
  List.filter (fun (_, _, header) -> header_has_code header) dep
37
  List.filter (fun (Dep (_, _, header, _)) -> header_has_code header) dep
38 38

  
39 39
let lib_dependencies dep = 
40 40
  List.fold_left 
41
    (fun accu (_, _, header) -> Utils.list_union (header_libs header) accu) [] dep
41
    (fun accu (Dep (_, _, header, _)) -> Utils.list_union (header_libs header) accu) [] dep
42 42
    
43
let fprintf_dependencies fmt dep =
43
let fprintf_dependencies fmt (dep: dep_t list) =
44 44
  let compiled_dep = compiled_dependencies dep in
45 45
  List.iter (fun s -> (* Format.eprintf "Adding dependency: %s@." s;  *)
46 46
    fprintf fmt "\t${GCC} -I${INC} -c %s@." s)
47 47
    (("${INC}/io_frontend.c"):: (* IO functions when a main function is computed *)
48 48
	(List.map 
49
	   (fun (local, s, _) -> 
49
	   (fun (Dep (local, s, _, _)) -> 
50 50
	     (if local then s else Version.include_path ^ "/" ^ s) ^ ".c")
51 51
	   compiled_dep))
52 52

  
53 53
module type MODIFIERS_MKF =
54
sig
55
  val other_targets: Format.formatter -> string -> string -> (bool * string * top_decl list) list -> unit
54
sig (* dep was (bool * ident * top_decl list) *)
55
  val other_targets: Format.formatter -> string -> string -> dep_t list -> unit
56 56
end
57 57

  
58 58
module EmptyMod =
59
struct
59
(struct
60 60
  let other_targets _ _ _ _ = ()
61
end
61
end: MODIFIERS_MKF)
62 62

  
63 63
module Main = functor (Mod: MODIFIERS_MKF) -> 
64 64
struct
65 65

  
66 66

  
67
let print_makefile basename nodename dependencies fmt =
67
let print_makefile basename nodename (dependencies:  dep_t list) fmt =
68 68
  fprintf fmt "GCC=gcc@.";
69 69
  fprintf fmt "LUSTREC=%s@." Sys.executable_name;
70 70
  fprintf fmt "LUSTREC_BASE=%s@." (Filename.dirname (Filename.dirname Sys.executable_name));
......
77 77
  fprintf fmt "\t${GCC} -I${INC} -I. -c %s_main.c@." basename;   
78 78
  fprintf_dependencies fmt dependencies;    
79 79
  fprintf fmt "\t${GCC} -o %s_%s io_frontend.o %a %s.o %s_main.o %a@." basename nodename 
80
    (Utils.fprintf_list ~sep:" " (fun fmt (_, s, _) -> Format.fprintf fmt "%s.o" s)) (compiled_dependencies dependencies)
80
    (Utils.fprintf_list ~sep:" " (fun fmt (Dep (_, s, _, _)) -> Format.fprintf fmt "%s.o" s)) 
81
    (compiled_dependencies dependencies)
81 82
    basename (* library .o *)
82 83
    basename (* main function . o *) 
83 84
    (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib)) (lib_dependencies dependencies)
src/backends/C/c_backend_spec.ml
158 158
  C_backend_makefile.fprintf_dependencies fmt dependencies; 
159 159
  fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@." 
160 160
    basename 
161
    (Utils.fprintf_list ~sep:" " (fun fmt (_, s, _) -> Format.fprintf fmt "%s.o" s)) 
161
    (Utils.fprintf_list ~sep:" " (fun fmt (Dep (_, s, _, _)) -> Format.fprintf fmt "%s.o" s)) 
162 162
    (C_backend_makefile.compiled_dependencies dependencies)
163 163
    ("${FRAMACEACSL}/e_acsl.c " 
164 164
     ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c " 
src/backends/C/c_backend_src.ml
212 212
			       The order of evaluation of dependencies should be
213 213
			       compatible with overloading. (Not checked yet) *) 
214 214
      List.fold_left
215
	(fun res (_, _, decls) -> 
215
	(fun res (Dep (_, _, decls, _)) -> 
216 216
	  match res with
217 217
	  | Some _ -> res
218 218
	  | None -> 
......
421 421
    begin
422 422
      fprintf source_fmt "#include <stdlib.h>@.";
423 423
    end;
424
  print_import_prototype source_fmt (true, basename, []);
424
  print_import_prototype source_fmt (Dep (true, basename, [], true (* assuming it is stateful *)));
425 425
  pp_print_newline source_fmt ();
426 426
  (* Print the svn version number and the supported C standard (C90 or C99) *)
427 427
  print_version source_fmt;
src/compiler_common.ml
188 188
      Stateless.pp_error err;
189 189
    raise exc
190 190

  
191
let is_stateful topdecl =
192
  match topdecl.top_decl_desc with
193
  | Node nd -> (match nd.node_stateless with Some b -> not b | None -> not nd.node_dec_stateless)
194
  | ImportedNode nd -> not nd.nodei_stateless 
195
  | _ -> false
191 196

  
192 197

  
193 198
let import_dependencies prog =
......
202 207
      let lusic = Modules.import_dependency dep.top_decl_loc (local, s) in
203 208
      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]@ ");
204 209
      let (lusi_type_env, lusi_clock_env) = get_envs_from_top_decls lusic.Lusic.contents in
205
      (local, s, lusic.Lusic.contents)::compilation_dep,
210
      let is_stateful = List.exists is_stateful lusic.Lusic.contents in
211
      let new_dep = Dep (local, s, lusic.Lusic.contents, is_stateful ) in
212
      new_dep::compilation_dep,
206 213
      Env.overwrite type_env lusi_type_env,
207 214
      Env.overwrite clock_env lusi_clock_env)
208 215
    ([], Basic_library.type_env, Basic_library.clock_env)
src/lustreSpec.ml
75 75

  
76 76
type quantifier_type = Exists | Forall
77 77

  
78

  
79

  
80 78
(* The tag of an expression is a unique identifier used to distinguish
81 79
   different instances of the same node *)
82 80
type expr =
......
209 207

  
210 208
type program = top_decl list
211 209

  
210
type dep_t = Dep of 
211
    bool 
212
  * ident
213
  * (top_decl list) 
214
  * bool (* is stateful *)
215

  
212 216
type error =
213 217
    Main_not_found
214 218
  | Main_wrong_kind

Also available in: Unified diff