CristalCaveGem » LustreC

    end

  )

  match !Options.spec with

  | "no" -> begin

    let module SourceMain = C_backend_main.Main (SourceMainMod) in

    let module Makefile = C_backend_makefile.Main (MakefileMod) in

  end

  | "acsl" -> begin

    let module SourceMain = C_backend_main.Main (SourceMainMod) in

    let module Makefile = C_backend_makefile.Main (MakefileMod) in

  end

  | "c" -> begin

  fprintf fmt "#include \"%s.h\"@," s

  List.iter (fun decl -> match decl.top_decl_desc with

  | ImportedNode ind when not ind.nodei_stateless ->

    let static = List.filter (fun v -> v.var_dec_const) ind.nodei_inputs

    (* Import the header *)

    fprintf header_fmt "/* Import header from %s */@." basename;

    fprintf header_fmt "@[<v>";

    fprintf header_fmt "@]@.";

    fprintf header_fmt "/* Import dependencies */@.";

    fprintf header_fmt "@[<v>";

    fprintf header_fmt "/* Import dependencies */@.";

    fprintf header_fmt "@[<v>";

    List.iter

      dependencies;

    fprintf header_fmt "@]@.";

    fprintf header_fmt "/* Types definitions */@.";

  fprintf fmt "#include <stdio.h>@.#include <unistd.h>@.#include \"%s/io_frontend.h\"@." Version.include_path 

  print_main_header main_fmt;

  fprintf main_fmt "#include <stdlib.h>@.#include <assert.h>@.";

  pp_print_newline main_fmt ();

  (* Print the svn version number and the supported C standard (C90 or C99) *)

let compiled_dependencies dep = 

let lib_dependencies dep = 

  List.fold_left 

  let compiled_dep = compiled_dependencies dep in

  List.iter (fun s -> (* Format.eprintf "Adding dependency: %s@." s;  *)

    fprintf fmt "\t${GCC} -I${INC} -c %s@." s)

    (("${INC}/io_frontend.c"):: (* IO functions when a main function is computed *)

	(List.map 

	     (if local then s else Version.include_path ^ "/" ^ s) ^ ".c")

	   compiled_dep))

module type MODIFIERS_MKF =

end

module EmptyMod =

  let other_targets _ _ _ _ = ()

module Main = functor (Mod: MODIFIERS_MKF) -> 

struct

  fprintf fmt "GCC=gcc@.";

  fprintf fmt "LUSTREC=%s@." Sys.executable_name;

  fprintf fmt "LUSTREC_BASE=%s@." (Filename.dirname (Filename.dirname Sys.executable_name));

  fprintf fmt "\t${GCC} -I${INC} -I. -c %s_main.c@." basename;   

  fprintf_dependencies fmt dependencies;    

  fprintf fmt "\t${GCC} -o %s_%s io_frontend.o %a %s.o %s_main.o %a@." basename nodename 

    basename (* library .o *)

    basename (* main function . o *) 

    (Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib)) (lib_dependencies dependencies)

  C_backend_makefile.fprintf_dependencies fmt dependencies; 

  fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@." 

    basename 

    (C_backend_makefile.compiled_dependencies dependencies)

    ("${FRAMACEACSL}/e_acsl.c " 

     ^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c " 

			       The order of evaluation of dependencies should be

			       compatible with overloading. (Not checked yet) *) 

      List.fold_left

	  match res with

	  | Some _ -> res

	  | None -> 

    begin

      fprintf source_fmt "#include <stdlib.h>@.";

    end;

  pp_print_newline source_fmt ();

  (* Print the svn version number and the supported C standard (C90 or C99) *)

  print_version source_fmt;

      Stateless.pp_error err;

    raise exc

let import_dependencies prog =

      let lusic = Modules.import_dependency dep.top_decl_loc (local, s) in

      Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]@ ");

      let (lusi_type_env, lusi_clock_env) = get_envs_from_top_decls lusic.Lusic.contents in

      Env.overwrite type_env lusi_type_env,

      Env.overwrite clock_env lusi_clock_env)

    ([], Basic_library.type_env, Basic_library.clock_env)

type quantifier_type = Exists | Forall

(* The tag of an expression is a unique identifier used to distinguish

   different instances of the same node *)

type expr =

type program = top_decl list

type error =

    Main_not_found

  | Main_wrong_kind