CristalCaveGem » LustreC

PostInstallCommand: mkdir -p $(prefix)/include; cp -rf include $(prefix)/include/lustrec

(* DO NOT EDIT (digest: 6666f62d55895fd4c2e5dbbf8e9d4998) *)

                              "$(prefix)/include;";

                              "-rf";

                              "include";

                              "$(prefix)/include/lustrec"

  | Types.Tbool           -> fprintf fmt "_Bool %s%a" var pp_suffix ()

  | Types.Treal           -> fprintf fmt "double %s%a" var pp_suffix ()

  | Types.Tint            -> fprintf fmt "int %s%a" var pp_suffix ()

    let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in

  | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix

  | Types.Tconst ty       -> fprintf fmt "%s %s" ty var

  | Types.Tarrow (_, _)   -> fprintf fmt "void (*%s)()" var

  | _                     -> eprintf "internal error: pp_c_type %a@." Types.print_ty t; assert false

    fprintf fmt "{%a}"

  fprintf fmt "%a = (%a) (%s->_reg.%s)"

    fprintf fmt "%s" id.var_id

    then fprintf fmt "*%s" id.var_id

    else fprintf fmt "%s" id.var_id

    fprintf fmt "%s" id.var_id

      fprintf fmt "%s" id.var_id

      fprintf fmt "&%s" id.var_id

  fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name

    | Const_array ca -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:"," pp_c_const) ca

    | Array vl      -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl

    | Access (t, i) -> fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i

      then fprintf fmt "*%a" pp_var v

      else fprintf fmt "%s->_reg.%a" self pp_var v

  Utils.fprintf_list ~sep:"" (fun fmt (loc, check) -> fprintf fmt "@[<v>%a@,assert (%a);@]@," Location.pp_c_loc loc (pp_c_val self (pp_c_var_read m)) check) fmt m.mstep.step_checks

 | LVar v -> fprintf fmt "[%s]" v

 | LInt r -> fprintf fmt "[%d]" !r

   let pp_var_suffix fmt v = fprintf fmt "%a%a" pp_value v pp_suffix loop_vars in

(*eprintf "pp_assign %a %a %d@." Types.print_ty var_type pp_val value depth;*)

(*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)

      fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"

(*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)

      fprintf fmt "@[<v 2>{@,%a@]@,}"

   fprintf fmt "%s_step (%a%t%a%t%s->%s);"

   fprintf fmt "%s (%a%t%a);"

  fprintf fmt "@[<v 2>case %a:@,%a@,break;@]" pp_c_tag t (Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) h

(**************************************************************************)

(*     Printing spec for c *)

(**************************************************************************)

let pp_econst fmt c = 

  match c with

    | EConst_int i -> pp_print_int fmt i

    | EConst_real r -> pp_print_string fmt r

    | EConst_float r -> pp_print_float fmt r

    | EConst_bool b -> pp_print_bool fmt b

    | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")

let rec pp_eexpr is_output fmt eexpr = 

  let pp_eexpr = pp_eexpr is_output in

  match eexpr.eexpr_desc with

    | EExpr_const c -> pp_econst fmt c

    | EExpr_ident id -> 

      if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id

    | EExpr_tuple el -> Utils.fprintf_list ~sep:"," pp_eexpr fmt el

    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2

    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2

    (* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)

    (* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)

    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e

    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id

    | EExpr_merge (id, e1, e2) -> 

      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2

    | EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r

    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" Printers.pp_node_args vars pp_eexpr e 

    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" Printers.pp_node_args vars pp_eexpr e 

    (* | EExpr_whennot _ *)

    (* | EExpr_uclock _ *)

    (* | EExpr_dclock _ *)

    (* | EExpr_phclock _ -> assert false *)

and pp_eapp is_output fmt id e r =

  let pp_eexpr = pp_eexpr is_output in

  match r with

  | None ->

    (match id, e.eexpr_desc with

    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2

    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e

    | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2

    | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2

    | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2

    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2

    | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2

    | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2

    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2

    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2

    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2

    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2

    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2

    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2

    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2

    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2

    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e

    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3

    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)

  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 

let pp_ensures is_output fmt e =

  match e with

    | EnsuresExpr e -> fprintf fmt "ensures %a;@ " (pp_eexpr is_output) e

    | SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (Utils.fprintf_list ~sep:", " (pp_eexpr is_output)) args

let pp_acsl_spec outputs fmt spec =

  let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in

  let pp_eexpr = pp_eexpr is_output in

  fprintf fmt "@[<v 2>/*@@ ";

  Utils.fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires;

  Utils.fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures;

  fprintf fmt "@ ";

  (* fprintf fmt "assigns *self%t%a;@ "  *)

  (*   (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *)

  (*   (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *)

  Utils.fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> 

    fprintf fmt "behavior %s:@[@ %a@ %a@]" 

      name

      (Utils.fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes

      (Utils.fprintf_list ~sep:"@ " (pp_ensures is_output)) requires

  ) fmt spec.behaviors;

  fprintf fmt "@]@ */@.";

  ()

	pp_acsl_spec m.mstep.step_outputs fmt spec

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

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

  fprintf fmt "INC=${LUSTREC_BASE}/include/lustrec@.";

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

 fprintf fmt "@.";

 fprintf fmt "clean:@.";

 fprintf fmt "\t\\rm -f *.o %s_%s@." basename nodename

  | Expr_appl of call_t

 and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *)

(************************************************************************)

(*        Renaming                                                      *)

 let rec rename_expr  f_node f_var f_const expr =

   { expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc }

 and rename_expr_desc f_node f_var f_const expr_desc =

   let re = rename_expr  f_node f_var f_const in

   match expr_desc with

   | Expr_const _ -> expr_desc

   | Expr_ident i -> Expr_ident (f_var i)

   | Expr_array el -> Expr_array (List.map re el)

   | Expr_access (e1, d) -> Expr_access (re e1, d)

   | Expr_power (e1, d) -> Expr_power (re e1, d)

   | Expr_tuple el -> Expr_tuple (List.map re el)

   | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)

   | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) 

   | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)

   | Expr_pre e' -> Expr_pre (re e')

   | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)

   | Expr_merge (i, hl) -> 

     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)

   | Expr_appl (i, e', i') -> 

     Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) -> f_var x, l) i')

   | _ -> assert false

 let rename_node_annot f_node f_var f_const expr  =

   assert false

 let rename_expr_annot f_node f_var f_const annot =

   assert false

let rename_node f_node f_var f_const nd =

  let rename_var v = { v with var_id = f_var v.var_id } in

  let inputs = List.map rename_var nd.node_inputs in

  let outputs = List.map rename_var nd.node_outputs in

  let locals = List.map rename_var nd.node_locals in

  let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in

  let node_checks = List.map (Dimension.expr_replace_var f_var)  nd.node_checks in

  let node_asserts = List.map 

    (fun a -> 

      { a with assert_expr = rename_expr f_node f_var f_const a.assert_expr } 

    ) nd.node_asserts

  in

  let eqs = List.map 

    (fun eq -> { eq with

      eq_lhs = List.map f_var eq.eq_lhs; 

      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs

    } ) nd.node_eqs

  in

  let spec = 

    Utils.option_map 

      (fun s -> rename_node_annot f_node f_var f_const s) 

      nd.node_spec 

  in

  let annot =

    Utils.option_map

      (fun s -> rename_expr_annot f_node f_var f_const s) 

      nd.node_annot

  in

  {

    node_id = f_node nd.node_id;

    node_type = nd.node_type;

    node_clock = nd.node_clock;

    node_inputs = inputs;

    node_outputs = outputs;

    node_locals = locals;

    node_gencalls = gen_calls;

    node_checks = node_checks;

    node_asserts = node_asserts;

    node_eqs = eqs;

    node_spec = spec;

    node_annot = annot;

  }

let rename_const f_const c =

  { c with const_id = f_const c.const_id }

let rename_prog f_node f_var f_const prog =

  List.rev (

    List.fold_left (fun accu top ->

      (match top.top_decl_desc with

      | Node nd -> 

	{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }

      | Consts c -> 

	{ top with top_decl_desc = Consts (List.map (rename_const f_const) c) }

      | ImportedNode _

      | ImportedFun _

      | Open _ -> top)

      ::accu

) [] prog

  )

(**********************************************************************)

  {expr_tag: tag; (* Unique identifier *)

   expr_desc: expr_desc;

   mutable expr_type: Types.type_expr;

   mutable expr_clock: Clocks.clock_expr;

   mutable expr_delay: Delay.delay_expr; (* Used for the initialisation check *)

   mutable expr_annot: LustreSpec.expr_annot option; (* Spec *)

   expr_loc: Location.t}

| Expr_const of constant

| Expr_ident of ident

| Expr_tuple of expr list

| Expr_ite   of expr * expr * expr

| Expr_arrow of expr * expr

| Expr_fby of expr * expr

| Expr_array of expr list

| Expr_access of expr * Dimension.dim_expr (* acces(e,i) is the i-th element 

					      of array epxression e *)

| Expr_power of expr * Dimension.dim_expr (* power(e,n) is the array of 

					     size n filled with expression e *)

| Expr_pre of expr

| Expr_when of expr * ident * label

| Expr_merge of ident * (label * expr) list

| Expr_appl of call_t

| Expr_uclock of expr * int

| Expr_dclock of expr * int

| Expr_phclock of expr * rat

and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *)

(** rename_prog f_node f_var f_const prog *)

val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program -> program

let rec expr_replace_var fvar e = 

 { e with dim_desc = expr_replace_desc fvar e.dim_desc }

and expr_replace_desc fvar e =

  let re = expr_replace_var fvar in

  match e with

  | Dvar

  | Dunivar

  | Dbool _

  | Dint _ -> e

  | Dident v -> Dident (fvar v)

  | 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)

  (* | EExpr_concat of eexpr * eexpr *)

  (* | EExpr_tail of eexpr *)

  (* | EExpr_whennot of eexpr * ident *)

  (* | EExpr_uclock of eexpr * int *)

  (* | EExpr_dclock of eexpr * int *)

  (* | EExpr_phclock of eexpr * rat *)

  (* Perform global inlining *)

  let prog =

    if !Options.global_inline && 

      (match !Options.main_node with | "" -> false | _ -> true) then

      Inliner.global_inline prog type_env clock_env

    else

      prog

  in

let global_inline = ref false

let witnesses = ref false

    "-inline", Arg.Set global_inline, "inline all node calls (require a main node)";

    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";

    | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2

    | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e

    | _ -> fprintf fmt "%s (%a)" id pp_expr e

)

let pp_econst fmt c = 

  match c with

    | EConst_int i -> pp_print_int fmt i

    | EConst_real r -> pp_print_string fmt r

    | EConst_float r -> pp_print_float fmt r

    | EConst_bool b -> pp_print_bool fmt b

    | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")

let rec pp_eexpr fmt eexpr = 

  match eexpr.eexpr_desc with

    | EExpr_const c -> pp_econst fmt c

    | EExpr_ident id -> pp_print_string fmt id

    | EExpr_tuple el -> fprintf_list ~sep:"," pp_eexpr fmt el

    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2

    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2

    (* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)

    (* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)

    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e

    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id

    | EExpr_merge (id, e1, e2) -> 

      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2

    | EExpr_appl (id, e, r) -> pp_eapp fmt id e r

    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" pp_node_args vars pp_eexpr e 

    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" pp_node_args vars pp_eexpr e 

    (* | EExpr_whennot _ *)

    (* | EExpr_uclock _ *)

    (* | EExpr_dclock _ *)

    (* | EExpr_phclock _ -> assert false *)

and pp_eapp fmt id e r =

  match r with

  | None ->

    (match id, e.eexpr_desc with

    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2

    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e

    | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2

    | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2

    | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2

    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2

    | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2

    | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2

    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2

    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2

    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2

    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2

    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2

    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2

    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2

    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2

    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e

    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3

    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)

  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 

let pp_ensures fmt e =

  match e with

    | EnsuresExpr e -> fprintf fmt "ensures %a;@ " pp_eexpr e

    | SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (fprintf_list ~sep:", " pp_eexpr) args

let pp_spec fmt spec =

  fprintf fmt "@[<hov 2>(*@@ ";

  fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires;

  fprintf_list ~sep:"" pp_ensures fmt spec.ensures;

  fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> 

    fprintf fmt "behavior %s:@[@ %a@ %a@]" 

      name

      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes

      (fprintf_list ~sep:"@ " pp_ensures) requires

  ) fmt spec.behaviors;

  fprintf fmt "@]*)";

  ()

fprintf fmt "@[<v 0>%a%tnode %s (%a) returns (%a)@.%a%alet@.@[<h 2>   @ @[%a@]@ @]@.tel@]@."

  (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec

  (fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@.") 

   used during node applications and assignments *)

  let tins = type_list_of_type ty_lhs in

  let args = expr_list_of_expr eq.eq_rhs in

  List.iter2 (type_subtyping_arg env in_main false) args tins;

  | Node nd -> (

      try

	type_node env nd decl.top_decl_loc

      with Error (loc, err) as exc -> (

	if !Options.global_inline then

	  Format.eprintf "Type error: failing node@.%a@.@?"

	    Printers.pp_node nd

	;

	raise exc)

  )

let desome x = match x with Some x -> x | None -> failwith "desome"

	@for i in `find . -iname *.lusi`; do grep generated $$i > /dev/null; if [ $$? -eq 0 ]; then rm $$i; fi; done

#LUSTREC="../../_build/src/lustrec"

LUSTREC=lustrec

  echo fichier:$file

 #  echo opts:$opts

   rm -f witness*

	$LUSTREC -d build -verbose 0 $opts -inline -witnesses -node $main ../$file;

  #  echo "horn encoding: lustreh -horn -node check witness.lus 2>/dev/nul"

    lustreh -horn -node check witness.lus 2>/dev/null

    #    gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ `basename $file .lus`.c > /dev/null

   # echo "Calling z3: "

    z3="`z3 -t:10 witness.smt2 | xargs`"

    #echo "Test: $z3"

    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then

      rz3="VALID";

    elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then

      rz3="ERROR";

    elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then

      rz3="UNKNOWN";

      rz3="INVALID"

      exit 1

    echo "lustrec ($rlustrec),inlining valid ($rz3),`dirname $file`,`basename $file`,node $main" | column -t -s',' | tee -a ../report-$NOW | grep "INVALID\|ERROR\|UNKNOWN"

done < ../tests_ok.nolarge.list