/ - Diff - LustreC

     exception Scope_clock of clock_expr
     exception Error of Location.t * error
     let print_ckset fmt s =
       match s with
       | CSet_all -> ()
       | CSet_pck (k,q) ->
           let (a,b) = simplify_rat q in
           if k = 1 && a = 0 then
             fprintf fmt "<:P"
           else
             fprintf fmt "<:P_(%i,%a)" k print_rat (a,b)
     let rec print_carrier fmt cr =
      (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
       match cr.carrier_desc with
       | Carry_const id -> fprintf fmt "%s" id
       | Carry_name ->
           fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
       | Carry_var ->
         fprintf fmt "'%s" (name_of_carrier cr.carrier_id)
       | Carry_link cr' ->
         print_carrier fmt cr'
     (* Simple pretty-printing, performs no simplifications. Linear
        complexity. For debug mainly. *)
     let rec print_ck_long fmt ck =
       match ck.cdesc with
       | Carrow (ck1,ck2) ->
           fprintf fmt "%a->%a" print_ck_long ck1 print_ck_long ck2
       | Ctuple cklist ->
         fprintf fmt "(%a)"
           (fprintf_list ~sep:" * " print_ck_long) cklist
       | Con (ck,c,l) ->
         fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
       | Pck_up (ck,k) ->
         fprintf fmt "%a*^%i" print_ck_long ck k
       | Pck_down (ck,k) ->
         fprintf fmt "%a/^%i" print_ck_long ck k
       | Pck_phase (ck,q) ->
         fprintf fmt "%a~>%a" print_ck_long ck print_rat (simplify_rat q)
       | Pck_const (n,p) ->
         fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
       | Cvar cset ->
         fprintf fmt "'_%i%a" ck.cid print_ckset cset
       | Cunivar cset ->
         fprintf fmt "'%i%a" ck.cid print_ckset cset
       | Clink ck' ->
         fprintf fmt "link %a" print_ck_long ck'
       | Ccarrying (cr,ck') ->
         fprintf fmt "(%a:%a)" print_carrier cr print_ck_long ck'
     let new_id = ref (-1)
     let new_ck desc scoped =
-...
      | Ccarrying (cr, _) -> Some cr
      | _                 -> None
     let rename_carrier_static rename cr =
       match (carrier_repr cr).carrier_desc with
       | Carry_const id -> { cr with carrier_desc = Carry_const (rename id) }
       | _              -> (Format.eprintf "internal error: Clocks.rename_carrier_static %a@." print_carrier cr; assert false)
     let rec rename_static rename ck =
      match (repr ck).cdesc with
      | Ccarrying (cr, ck') -> { ck with cdesc = Ccarrying (rename_carrier_static rename cr, rename_static rename ck') }
      | Con (ck', cr, l)    -> { ck with cdesc = Con (rename_static rename ck', rename_carrier_static rename cr, l) }
      | _                   -> ck
     let uncarrier ck =
      match ck.cdesc with
      | Ccarrying (_, ck') -> ck'
-...
       in
       aux [] ck
     let print_ckset fmt s =
       match s with
       | CSet_all -> ()
       | CSet_pck (k,q) ->
           let (a,b) = simplify_rat q in
           if k = 1 && a = 0 then
             fprintf fmt "<:P"
           else
             fprintf fmt "<:P_(%i,%a)" k print_rat (a,b)
     let rec print_carrier fmt cr =
      (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
       match cr.carrier_desc with
       | Carry_const id -> fprintf fmt "%s" id
       | Carry_name ->
           fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
       | Carry_var ->
         fprintf fmt "'%s" (name_of_carrier cr.carrier_id)
       | Carry_link cr' ->
         print_carrier fmt cr'
     (* Simple pretty-printing, performs no simplifications. Linear
        complexity. For debug mainly. *)
     let rec print_ck_long fmt ck =
       match ck.cdesc with
       | Carrow (ck1,ck2) ->
           fprintf fmt "%a->%a" print_ck_long ck1 print_ck_long ck2
       | Ctuple cklist ->
         fprintf fmt "(%a)"
           (fprintf_list ~sep:" * " print_ck_long) cklist
       | Con (ck,c,l) ->
         fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
       | Pck_up (ck,k) ->
         fprintf fmt "%a*^%i" print_ck_long ck k
       | Pck_down (ck,k) ->
         fprintf fmt "%a/^%i" print_ck_long ck k
       | Pck_phase (ck,q) ->
         fprintf fmt "%a~>%a" print_ck_long ck print_rat (simplify_rat q)
       | Pck_const (n,p) ->
         fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
       | Cvar cset ->
         fprintf fmt "'_%i%a" ck.cid print_ckset cset
       | Cunivar cset ->
         fprintf fmt "'%i%a" ck.cid print_ckset cset
       | Clink ck' ->
         fprintf fmt "link %a" print_ck_long ck'
       | Ccarrying (cr,ck') ->
         fprintf fmt "(%a:%a)" print_carrier cr print_ck_long ck'
     (** [period ck] returns the period of [ck]. Expects a constant pclock
         expression belonging to the correct clock set. *)
     let rec period ck =

      | Expr_ident id -> id
      | _             -> assert false
     (* Generate a new ident expression from a declared variable *)
     let expr_of_vdecl v =
       { expr_tag = Utils.new_tag ();
         expr_desc = Expr_ident v.var_id;
         expr_type = v.var_type;
         expr_clock = v.var_clock;
         expr_delay = Delay.new_var ();
         expr_annot = None;
         expr_loc = v.var_loc }
     (* Caution, returns an untyped and unclocked expression *)
     let expr_of_ident id loc =
       {expr_tag = Utils.new_tag ();
-...
          mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
      | Dlink dim'       -> expr_of_dimension dim'
      | Dvar
      | Dunivar          -> (Format.eprintf "internal error: expr_of_dimension %a@." Dimension.pp_dimension dim;
      | Dunivar          -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim;
     			assert false)
     let dimension_of_const loc const =
-...
     let get_node_vars nd =
       nd.node_inputs @ nd.node_locals @ nd.node_outputs
     let mk_new_node_name nd id =
       let used_vars = get_node_vars nd in
       let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in
       mk_new_name used id
     let get_var id var_list =
         List.find (fun v -> v.var_id = id) var_list

     val mktop_decl: Location.t -> ident -> bool -> top_decl_desc -> top_decl
     val mkpredef_call: Location.t -> ident -> expr list -> expr
     val mk_new_name: (ident -> bool) -> ident -> ident
     val mk_new_node_name: node_desc -> ident -> ident
     val node_table : (ident, top_decl) Hashtbl.t
     val print_node_table:  Format.formatter -> unit -> unit
-...
     (* Caution, returns an untyped, unclocked, etc, expression *)
     val is_tuple_expr : expr -> bool
     val ident_of_expr : expr -> ident
     val expr_of_vdecl : var_decl -> expr
     val expr_of_ident : ident -> Location.t -> expr
     val expr_list_of_expr : expr -> expr list
     val expr_of_expr_list : Location.t -> expr list -> expr

       in unif dim1 dim2
     let rec expr_replace_var fvar e =
      { e with dim_desc = expr_replace_desc fvar e.dim_desc }
     and expr_replace_desc fvar e =
      { e with dim_desc = expr_replace_var_desc fvar e.dim_desc }
     and expr_replace_var_desc fvar e =
       let re = expr_replace_var fvar in
       match e with
       | Dvar
-...
       | Dappl (id, el) -> Dappl (id, List.map re el)
       | Dite (g,t,e) -> Dite (re g, re t, re e)
       | Dlink e -> Dlink (re e)
     let rec expr_replace_expr fvar e =
      { e with dim_desc = expr_replace_expr_desc fvar e.dim_desc }
     and expr_replace_expr_desc fvar e =
       let re = expr_replace_expr fvar in
       match e with
       | Dvar
       | Dunivar
       | Dbool _
       | Dint _ -> e
       | Dident v -> (fvar v).dim_desc
       | Dappl (id, el) -> Dappl (id, List.map re el)
       | Dite (g,t,e) -> Dite (re g, re t, re e)
       | Dlink e -> Dlink (re e)

       | Node nd -> nd.node_id = id
       | _ -> false)
     let get_static_inputs node args =
       List.fold_right2 (fun vdecl arg static ->
         if vdecl.var_dec_const then (vdecl.var_id, Corelang.dimension_of_expr arg) :: static else static)
         node.node_inputs
         (Corelang.expr_list_of_expr args)
         []
     let get_carrier_inputs node args =
       List.fold_right2 (fun vdecl arg carrier ->
         if Types.get_clock_base_type vdecl.var_type <> None then (vdecl.var_id, ident_of_expr arg) :: carrier else carrier)
         node.node_inputs
         (Corelang.expr_list_of_expr args)
         []
     let is_node_var node v =
      try
        ignore (Corelang.get_node_var v node); true
      with Not_found -> false
     let rename_expr rename expr = expr_replace_var rename expr
     let rename_eq rename eq =
       { eq with
         eq_lhs = List.map rename eq.eq_lhs;
-...
+      }
     (*
         expr, locals', eqs = inline_call id args' reset locals nodes
         expr, locals', eqs = inline_call id args' reset locals node nodes
     We select the called node equations and variables.
        renamed_inputs = args
-...
     TODO: convert the specification/annotation/assert and inject them
     TODO: deal with reset
     *)
     let inline_call orig_expr args reset locals node =
     let inline_call node orig_expr args reset locals caller =
       let loc = orig_expr.expr_loc in
       let uid = orig_expr.expr_tag in
       let rename v =
         if v = tag_true || v = tag_false then v else
         (Format.fprintf Format.str_formatter "%s_%i_%s"
           node.node_id uid v;
         Format.flush_str_formatter ())
         if v = tag_true || v = tag_false || not (is_node_var node v) then v else
           Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v)
       in
       let eqs' = List.map (rename_eq rename) (get_node_eqs node)
       in
       let rename_var v = { v with var_id = rename v.var_id } in
       let static_inputs = get_static_inputs node args in
       let carrier_inputs = get_carrier_inputs node args in
       let rename_static v =
         try
           List.assoc v static_inputs
         with Not_found -> Dimension.mkdim_ident loc v
         (*Format.eprintf "Inliner.rename_static %s = %a@." v Dimension.pp_dimension res; res*)
       in
       let rename_carrier v =
         try
           List.assoc v carrier_inputs
         with Not_found -> v in
       let rename_var v =
       (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
         { v with
           var_id = rename v.var_id;
           var_type = Types.rename_static rename_static v.var_type;
           var_clock = Clocks.rename_static rename_carrier v.var_clock;
         } in
       let inputs' = List.map rename_var node.node_inputs in
       let outputs' = List.map rename_var node.node_outputs in
       let locals' = List.map rename_var node.node_locals in
       (* checking we are at the appropriate (early) step: node_checks and
          node_gencalls should be empty (not yet assigned) *)
       assert (node.node_checks = []);
-...
       assert (reset = None);
       let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', args) in
       let expr = expr_of_expr_list
         loc
         (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) outputs')
       let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')
       in
       let asserts' = (* We rename variables in assert expressions *)
         List.map
-...
     let inline_table = Hashtbl.create 23
     (*
        new_expr, new_locals, new_eqs = inline_expr expr locals nodes
        new_expr, new_locals, new_eqs = inline_expr expr locals node nodes
        Each occurence of a node in nodes in the expr should be replaced by fresh
        variables and the code of called node instance added to new_eqs
     *)
     let rec inline_expr ?(selection_on_annotation=false) expr locals nodes =
     let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes =
       let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
       let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in
       let inline_tuple el =
         List.fold_right (fun e (el_tail, locals, eqs, asserts) ->
           let e', locals', eqs', asserts' = inline_expr e locals nodes in
           let e', locals', eqs', asserts' = inline_expr e locals node nodes in
           e'::el_tail, locals', eqs'@eqs, asserts@asserts'
         ) el ([], locals, [], [])
       in
-...
       match expr.expr_desc with
       | Expr_appl (id, args, reset) ->
         let args', locals', eqs', asserts' = inline_expr args locals nodes in
         let args', locals', eqs', asserts' = inline_expr args locals node nodes in
         if List.exists (check_node_name id) nodes && (* the current node call is provided
     						    as arguments nodes *)
           (not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated,
     							      it is explicitely inlined here *)
         then
           (* The node should be inlined *)
            let _ =     Format.eprintf "Inlining call to %s@." id in
           let node = try List.find (check_node_name id) nodes
           (* let _ =     Format.eprintf "Inlining call to %s@." id in *)
           let called = try List.find (check_node_name id) nodes
     	with Not_found -> (assert false) in
           let node = node_of_top node in
           let node = inline_node node nodes in
           let called = node_of_top called in
           let called' = inline_node called nodes in
           let expr, locals', eqs'', asserts'' =
     	inline_call expr args' reset locals' node in
     	inline_call called' expr args' reset locals' node in
           expr, locals', eqs'@eqs'', asserts'@asserts''
         else
           (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)
-...
         let el', l', eqs', asserts' = inline_tuple el in
         { expr with expr_desc = Expr_array el' }, l', eqs', asserts'
       | Expr_access (e, dim) ->
         let e', l', eqs', asserts' = inline_expr e locals nodes in
         let e', l', eqs', asserts' = inline_expr e locals node nodes in
         { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts'
       | Expr_power (e, dim) ->
         let e', l', eqs', asserts' = inline_expr e locals nodes in
         let e', l', eqs', asserts' = inline_expr e locals node nodes in
         { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts'
       | Expr_pre e ->
         let e', l', eqs', asserts' = inline_expr e locals nodes in
         let e', l', eqs', asserts' = inline_expr e locals node nodes in
         { expr with expr_desc = Expr_pre e' }, l', eqs', asserts'
       | Expr_when (e, id, label) ->
         let e', l', eqs', asserts' = inline_expr e locals nodes in
         let e', l', eqs', asserts' = inline_expr e locals node nodes in
         { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts'
       | Expr_merge (id, branches) ->
         let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
         let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
         { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
     and inline_node ?(selection_on_annotation=false) nd nodes =
     and inline_node ?(selection_on_annotation=false) node nodes =
       try Hashtbl.find inline_table node.node_id
       with Not_found ->
       let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
       let new_locals, eqs, asserts =
         List.fold_left (fun (locals, eqs, asserts) eq ->
           let eq_rhs', locals', new_eqs', asserts' =
     	inline_expr eq.eq_rhs locals nodes
     	inline_expr eq.eq_rhs locals node nodes
           in
           locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts
         ) (nd.node_locals, [], nd.node_asserts) (get_node_eqs nd)
         ) (node.node_locals, [], node.node_asserts) (get_node_eqs node)
       in
       { nd with
       let inlined =
       { node with
         node_locals = new_locals;
         node_stmts = List.map (fun eq -> Eq eq) eqs;
         node_asserts = asserts;
+      }
       in
       begin
         (*Format.eprintf "inline node:<< %a@.>>@." Printers.pp_node inlined;*)
         Hashtbl.add inline_table node.node_id inlined;
         inlined
       end
     let inline_all_calls node nodes =
       let nd = match node.top_decl_desc with Node nd -> nd | _ -> assert false in
-...
       in
       let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in
       let new_prog = others@nodes_origs@nodes_inlined@main in
       let _ = Typing.type_prog type_env new_prog in
       let _ = Clock_calculus.clock_prog clock_env new_prog in

           exit 0
         end;
       (* Perform global inlining *)
       let prog =
         if !Options.global_inline &&
           (match !Options.main_node with | "" -> false | _ -> true) then
           Inliner.global_inline basename prog type_env clock_env
         else (* if !Option.has_local_inline *)
           Inliner.local_inline basename prog type_env clock_env
       in
       (* Delay calculus *)
       (* TO BE DONE LATER (Xavier)
         if(!Options.delay_calculus)
-...
       Typing.uneval_prog_generics prog;
       Clock_calculus.uneval_prog_generics prog;
       (* Perform global inlining *)
       let prog =
         if !Options.global_inline &&
           (match !Options.main_node with | "" -> false | _ -> true) then
           Inliner.global_inline basename prog type_env clock_env
         else (* if !Option.has_local_inline *)
           Inliner.local_inline basename prog type_env clock_env
       in
     (*Format.eprintf "Inliner.global_inline<<@.%a@.>>@." Printers.pp_prog prog;*)
       (* Computes and stores generic calls for each node,
          only useful for ANSI C90 compliant generic node compilation *)
       if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
-...
       if !Options.output = "lustre" then
         Normalization.unfold_arrow_active := false;
       let prog = Normalization.normalize_prog prog in
       Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
       (* Checking array accesses *)
       if !Options.check then

+      }
       in aux ()
     (* Generate a new ident expression from a declared variable *)
     let mk_ident_expr v =
       { expr_tag = new_tag ();
         expr_desc = Expr_ident v.var_id;
         expr_type = v.var_type;
         expr_clock = v.var_clock;
         expr_delay = Delay.new_var ();
         expr_annot = None;
         expr_loc = v.var_loc }
     (* Get the equation in [defs] with [expr] as rhs, if any *)
     let get_expr_alias defs expr =
      try Some (List.find (fun eq -> is_eq_expr eq.eq_rhs expr) defs)
-...
        expr_desc = Expr_ident v.var_id }
      | _   -> { expr with
        expr_tag = Utils.new_tag ();
        expr_desc = Expr_tuple (List.map mk_ident_expr locals) }
        expr_desc = Expr_tuple (List.map expr_of_vdecl locals) }
     let unfold_offsets e offsets =
       let add_offset e d =
     (*Format.eprintf "add_offset %a %a@." Dimension.pp_dimension (Types.array_type_dimension e.expr_type) Dimension.pp_dimension d;*)
     (*Format.eprintf "add_offset %a(%a) %a @." Printers.pp_expr e Types.print_ty e.expr_type Dimension.pp_dimension d;
         let res = *)
         { e with
           expr_tag = Utils.new_tag ();
           expr_loc = d.Dimension.dim_loc;
           expr_type = Types.array_element_type e.expr_type;
           expr_desc = Expr_access (e, d) } in
           expr_desc = Expr_access (e, d) }
     (*in (Format.eprintf "= %a @." Printers.pp_expr res; res) *)
       in
      List.fold_left add_offset e offsets
     (* Create an alias for [expr], if none exists yet *)
-...
         let new_def =
           mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
         in
         (* Format.eprintf "Checkign def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *)
         (* Format.eprintf "Checking def of alias: %a -> %a@." (fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) new_aliases Printers.pp_expr expr; *)
         (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
     (* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
-...
        taking propagated [offsets] into account
        in order to change expression type *)
     let mk_norm_expr offsets ref_e norm_d =
     (*Format.eprintf "mk_norm_expr %a %a @." Printers.pp_expr ref_e Printers.pp_expr { ref_e with expr_desc = norm_d};*)
       let drop_array_type ty =
         Types.map_tuple_type Types.array_element_type ty in
       { ref_e with
-...
     			    if List.exists (fun o -> o.var_id = v) node.node_outputs
     			    then
     			      let newvar = mk_fresh_var node eq.eq_loc t c in
     			      let neweq  = mkeq eq.eq_loc ([v], mk_ident_expr newvar) in
     			      let neweq  = mkeq eq.eq_loc ([v], expr_of_vdecl newvar) in
     			      (neweq :: defs_q, newvar :: vars_q), newvar.var_id :: lhs_q
     			    else
     			      (defs_q, vars_q), v::lhs_q

       | Tstatic (d, _) -> Some d
       | _              -> None
     let rec rename_static rename ty =
      match (repr ty).tdesc with
      | Tstatic (d, ty') -> { ty with tdesc = Tstatic (Dimension.expr_replace_expr rename d, rename_static rename ty') }
      | Tarray  (d, ty') -> { ty with tdesc = Tarray  (Dimension.expr_replace_expr rename d, rename_static rename ty') }
      | _                -> ty
     (*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
     let get_field_type ty label =
       match (repr ty).tdesc with
       | Tstruct fl -> (try Some (List.assoc label fl) with Not_found -> None)
-...
     let array_type_dimension ty =
       match (dynamic_type ty).tdesc with
       | Tarray (d, _) -> d
       | _             -> assert false
       | _             -> (Format.eprintf "internal error: Types.array_type_dimension %a@." print_ty ty; assert false)
     let rec array_type_multi_dimension ty =
       match (dynamic_type ty).tdesc with
-...
     let array_element_type ty =
       match (dynamic_type ty).tdesc with
       | Tarray (_, ty') -> ty'
       | _               -> assert false
       | _               -> (Format.eprintf "internal error: Types.array_element_type %a@." print_ty ty; assert false)
     let rec array_base_type ty =
       let ty = repr ty in

      | _                   -> ()
     let type_var_decl vd_env env vdecl =
     (*Format.eprintf "Typing.type_var_decl START %a@." Printers.pp_var vdecl;*)
       check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
       let eval_const id = Types.get_static_value (Env.lookup_value env id) in
       let type_dim d =
-...
       let new_env = Env.add_value env vdecl.var_id ty_status in
       type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
       vdecl.var_type <- ty_status;
     (*Format.eprintf "END@.";*)
       new_env
     let type_var_decl_list vd_env env l =

     mkdir -p build
     build=`pwd`"/build"
     gcc_compile() {
         gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null;
         if [ $? -ne 0 ]; then
     	rgcc="INVALID";
         else
     	rgcc="VALID"
         fi
+    }
     lustrec_compile() {
         $LUSTREC "$@";
         if [ $? -ne 0 ]; then
             rlustrec="INVALID";
         else
             rlustrec="VALID"
         fi
+    }
     base_compile() {
         while IFS=, read -r file main opts
-...
     	fi
             dir=${SRC_PREFIX}/`dirname "$file"`
     	pushd $dir > /dev/null
         if [ "$main" != "" ]; then
     	$LUSTREC -d $build -verbose 0 $opts -node $main "$name""$ext";
             if [ $? -ne 0 ]; then
                 rlustrec1="INVALID";
             else
                 rlustrec1="VALID"
     	fi
     	pushd $build > /dev/null
     	if [ $ext = ".lus" ]; then
                 gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
                 if [ $? -ne 0 ]; then
     		rgcc1="INVALID";
                 else
     		rgcc1="VALID"
     	    fi
     	if [ "$main" != "" ]; then
     	    lustrec_compile -d $build -verbose 0 $opts -node $main $name$ext;
     	else
     	    rgcc1="NONE"
     	    lustrec_compile -d $build -verbose 0 $opts $name$ext
     	fi
     	popd > /dev/null
         else
     	$LUSTREC -d $build -verbose 0 $opts "$name""$ext";
             if [ $? -ne 0 ]; then
                 rlustrec1="INVALID";
             else
                 rlustrec1="VALID"
             fi
     	pushd $build > /dev/null
     	if [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
                 gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
                 if [ $? -ne 0 ]; then
     		rgcc1="INVALID";
                 else
     		rgcc1="VALID"
                 fi
                 gcc_compile "$name";
     	else
     	    rgcc1="NONE"
     	    rgcc="NONE"
     	fi
     	popd > /dev/null
         fi
         popd > /dev/null
         if [ $verbose -gt 0 ]; then
     	echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
         else
     	echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
         fi;
     	popd > /dev/null
     	if [ $verbose -gt 0 ]; then
     	    echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
     	else
     	    echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
     	fi;
         done < $file_list
+    }
-...
         while IFS=, read -r file main opts
         do
     	name=`basename "$file" .lus`
     	ext=".lus"
     	if [ `dirname "$file"`/"$name" = "$file" ]; then
     	    return 0
     	    name=`basename "$file" .lusi`
     	    ext=".lusi"
     	fi
     	dir=${SRC_PREFIX}/`dirname "$file"`
     	pushd $dir > /dev/null
     # Checking inlining
         $LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus;
         if [ $? -ne 0 ]; then
             rlustrec2="INVALID";
         else
             rlustrec2="VALID"
         fi
         pushd $build > /dev/null
         gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
         if [ $? -ne 0 ]; then
             rgcc2="INVALID";
         else
             rgcc2="VALID"
         fi
         popd > /dev/null
         if [ $verbose -gt 0 ]; then
     	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
         else
     	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
         fi;
         popd > /dev/null
     done < $file_list
     	if [ "$main" != "" ]; then
     	    lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext;
     	else
     	    if [ "$ext" = ".lusi" ]; then
     		lustrec_compile -d $build -verbose 0 $opts $name$ext;
     	    else
     		rlustrec="NONE"
     		rgcc="NONE"
     	    fi
     	fi
     	pushd $build > /dev/null
     	if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
     	    gcc_compile "$name";
     	else
     	    rgcc="NONE"
     	fi
     	popd > /dev/null
     	popd > /dev/null
     	if [ $verbose -gt 0 ]; then
     	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
     	else
     	    echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
     	fi;
         done < $file_list
+    }
     inline_compile_with_check () {
-...
     	fi
     	dir=${SRC_PREFIX}/`dirname "$file"`
     	pushd $dir > /dev/null
         $LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus;
         if [ $? -ne 0 ]; then
             rlustrec2="INVALID";
         else
             rlustrec2="VALID"
         fi
         lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name".lus"
         pushd $build > /dev/null
         gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
         if [ $? -ne 0 ]; then
             rgcc2="INVALID";
         else
             rgcc2="VALID"
         fi
         gcc_compile "$name"
         popd > /dev/null
     	# Cheching witness
         pushd $build > /dev/null
         $LUSTREC -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus
         lustrec_compile -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus
         popd > /dev/null
         z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
         if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
-...
     	rinlining="INVALID/TIMEOUT"
         fi
         if [ $verbose -gt 0 ]; then
     	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
     	echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
         else
     	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
     	echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
         fi
         popd > /dev/null
     done < $file_list
-...
         # Checking horn backend
         if [ "$main" != "" ]; then
     	$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main "$name".lus;
     	lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main $name".lus";
         else
     	$LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts "$name".lus
         fi
         if [ $? -ne 0 ]; then
             rlustrec="INVALID";
         else
             rlustrec="VALID"
     	lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts $name".lus"
         fi
         # echo "z3 $build/$name".smt2
         # TODO: This part of the script has to be optimized
         z3 -T:10 "$build/$name".smt2 | grep unsat > /dev/null
-...
         exit 1
     fi
     # cleaning directory $build
     rm -f "$build"/* 2> /dev/null
     # executing tests
     [ ! -z "$c" ] && base_compile
     [ ! -z "$i" ] && inline_compile
     [ ! -z "$w" ] && inline_compile_with_check

test/tests_ok.list
904	904	./tests/arrays_arnaud/generic1.lusi
905	905	./tests/arrays_arnaud/generic1.lus
906	906	./tests/arrays_arnaud/generic2.lus
907		./tests/arrays_arnaud/generic3.lus,top,-dynamic -check-access
908	907	./tests/clocks/clocks1.lus,,-lusi
909	908	./tests/clocks/clocks1.lusi
910	909	./tests/clocks/clocks1.lus

Project

General

Profile

CristalCaveGem » LustreC

Revision b3f91fdb

Added by Xavier Thirioux almost 8 years ago