diff --git a/include/mpfr_lustre.c b/include/mpfr_lustre.c
new file mode 100644
index 0000000000000000000000000000000000000000..d58ca6a435310dd3d240caec77f168b87da4dbea
--- /dev/null
+++ b/include/mpfr_lustre.c
@@ -0,0 +1,96 @@
+#include <mpfr.h>
+#include "mpfr_lustre.h"
+
+void MPFR_LUSTRE_INIT () {
+ return;
+}
+
+void MPFR_LUSTRE_CLEAR () {
+ return;
+}
+
+void MPFRNeq_step (mpfr_t i1, mpfr_t i2,
+ _Bool (*out)
+ )
+{
+ *out = mpfr_lessgreater_p(i1, i2);
+}
+
+void MPFREq_step (mpfr_t i1, mpfr_t i2,
+ _Bool (*out)
+ )
+{
+ *out = mpfr_equal_p(i1, i2);
+}
+
+void MPFRGt_step (mpfr_t i1, mpfr_t i2,
+ _Bool (*out)
+ )
+{
+ *out = mpfr_greater_p(i1, i2);
+}
+
+void MPFRGe_step (mpfr_t i1, mpfr_t i2,
+ _Bool (*out)
+ )
+{
+ *out = mpfr_greaterequal_p(i1, i2);
+}
+
+extern void MPFRLt_step (mpfr_t i1, mpfr_t i2,
+ _Bool (*out)
+ )
+{
+ *out = mpfr_less_p(i1, i2);
+}
+void MPFRLe_step (mpfr_t i1, mpfr_t i2,
+ _Bool (*out)
+ )
+{
+ *out = mpfr_lessequal_p(i1, i2);
+}
+
+void MPFRDiv_step (mpfr_t i1, mpfr_t i2,
+ mpfr_t out
+ )
+{
+ mpfr_div(out, i1, i2, MPFR_RNDN);
+}
+
+void MPFRTimes_step (mpfr_t i1, mpfr_t i2,
+ mpfr_t out
+ )
+{
+ mpfr_mul(out, i1, i2, MPFR_RNDN);
+}
+
+void MPFRMinus_step (mpfr_t i1, mpfr_t i2,
+ mpfr_t out
+ )
+{
+ mpfr_sub(out, i1, i2, MPFR_RNDN);
+}
+
+void MPFRPlus_step (mpfr_t i1, mpfr_t i2,
+ mpfr_t out
+ )
+{
+ mpfr_add(out, i1, i2, MPFR_RNDN);
+}
+
+void MPFRUminus_step (mpfr_t i,
+ mpfr_t out
+ )
+{
+ mpfr_neg(out, i, MPFR_RNDN);
+}
+
+void MPFRInit(mpfr_t i, mpfr_prec_t prec)
+{
+ mpfr_init2(i, prec);
+}
+
+void MPFRClear(mpfr_t i)
+{
+ mpfr_clear(i);
+}
diff --git a/include/mpfr_lustre.lusi b/include/mpfr_lustre.lusi
new file mode 100644
index 0000000000000000000000000000000000000000..e23ae1364c2e52bf3afddeedcaf3d42eb4079fb3
--- /dev/null
+++ b/include/mpfr_lustre.lusi
@@ -0,0 +1,23 @@
+
+
+function MPFRUminus(i: real) returns (out: real) lib gmp lib mpfr;
+
+function MPFRPlus(i1, i2: real) returns (out: real);
+
+function MPFRMinus(i1, i2: real) returns (out: real);
+
+function MPFRTimes(i1, i2: real) returns (out: real);
+
+function MPFRDiv(i1, i2: real) returns (out: real);
+
+function MPFRLe(i1, i2: real) returns (out: bool);
+
+function MPFRLt(i1, i2: real) returns (out: bool);
+
+function MPFRGe(i1, i2: real) returns (out: bool);
+
+function MPFRGt(i1, i2: real) returns (out: bool);
+
+function MPFREq(i1, i2: real) returns (out: bool);
+
+function MPFRNeq(i1, i2: real) returns (out: bool);
diff --git a/src/global.ml b/src/global.ml
new file mode 100644
index 0000000000000000000000000000000000000000..892f630c4c1a2c7aca7fb19381d3f0adb1474799
--- /dev/null
+++ b/src/global.ml
@@ -0,0 +1,21 @@
+let type_env : (Types.type_expr Env.t) ref = ref Env.initial
+let clock_env : (Clocks.clock_expr Env.t) ref = ref Env.initial
+let basename = ref ""
+let main_node = ref ""
+
+module TypeEnv =
+struct
+let lookup_value ident = Env.lookup_value !type_env ident
+let exists_value ident = Env.exists_value !type_env ident
+let iter f = Env.iter !type_env f
+let pp pp_fun fmt () = Env.pp_env pp_fun fmt !type_env
+end
+
+let initialize () =
+ begin
+ main_node := !Options.main_node;
+ end
+
+(* Local Variables: *)
+(* compile-command:"make -C .." *)
+(* End: *)
diff --git a/src/mpfr.ml b/src/mpfr.ml
new file mode 100755
index 0000000000000000000000000000000000000000..d310936c25775eaa00abdf4f36a304c1aac9b84d
--- /dev/null
+++ b/src/mpfr.ml
@@ -0,0 +1,265 @@
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(********************************************************************)
+
+open Utils
+open LustreSpec
+open Corelang
+open Normalization
+open Machine_code
+
+let mpfr_module = mktop (Open(false, "mpfr_lustre"))
+
+let mpfr_rnd () = "MPFR_RNDN"
+
+let mpfr_prec () = !Options.mpfr_prec
+
+let inject_id = "MPFRId"
+
+let inject_copy_id = "mpfr_set"
+
+let inject_real_id = "mpfr_set_flt"
+
+let inject_init_id = "mpfr_init2"
+
+let inject_clear_id = "mpfr_clear"
+
+let mpfr_t = "mpfr_t"
+
+let unfoldable_value value =
+ not (Types.is_real_type value.value_type && is_const_value value)
+
+let inject_id_id expr =
+ let e = mkpredef_call expr.expr_loc inject_id [expr] in
+ { e with
+ expr_type = Type_predef.type_real;
+ expr_clock = expr.expr_clock;
+ }
+
+let pp_inject_real pp_var pp_val fmt var value =
+ Format.fprintf fmt "%s(%a, %a, %s);"
+ inject_real_id
+ pp_var var
+ pp_val value
+ (mpfr_rnd ())
+
+let inject_assign expr =
+ let e = mkpredef_call expr.expr_loc inject_copy_id [expr] in
+ { e with
+ expr_type = Type_predef.type_real;
+ expr_clock = expr.expr_clock;
+ }
+
+let pp_inject_copy pp_var fmt var value =
+ Format.fprintf fmt "%s(%a, %a, %s);"
+ inject_copy_id
+ pp_var var
+ pp_var value
+ (mpfr_rnd ())
+
+let rec pp_inject_assign pp_var fmt var value =
+ if is_const_value value
+ then
+ pp_inject_real pp_var pp_var fmt var value
+ else
+ pp_inject_copy pp_var fmt var value
+
+let pp_inject_init pp_var fmt var =
+ Format.fprintf fmt "%s(%a, %i);"
+ inject_init_id
+ pp_var var
+ (mpfr_prec ())
+
+let pp_inject_clear pp_var fmt var =
+ Format.fprintf fmt "%s(%a);"
+ inject_clear_id
+ pp_var var
+
+let base_inject_op id =
+ match id with
+ | "+" -> "MPFRPlus"
+ | "-" -> "MPFRMinus"
+ | "*" -> "MPFRTimes"
+ | "/" -> "MPFRDiv"
+ | "uminus" -> "MPFRUminus"
+ | "<=" -> "MPFRLe"
+ | "<" -> "MPFRLt"
+ | ">=" -> "MPFRGe"
+ | ">" -> "MPFRGt"
+ | "=" -> "MPFREq"
+ | "!=" -> "MPFRNeq"
+ | _ -> raise Not_found
+
+let inject_op id =
+ try
+ base_inject_op id
+ with Not_found -> id
+
+let homomorphic_funs =
+ List.fold_right (fun id res -> try base_inject_op id :: res with Not_found -> res) Basic_library.internal_funs []
+
+let is_homomorphic_fun id =
+ List.mem id homomorphic_funs
+
+let inject_call expr =
+ match expr.expr_desc with
+ | Expr_appl (id, args, None) when not (Basic_library.is_expr_internal_fun expr) ->
+ { expr with expr_desc = Expr_appl (inject_op id, args, None) }
+ | _ -> expr
+
+let expr_of_const_array expr =
+ match expr.expr_desc with
+ | Expr_const (Const_array cl) ->
+ let typ = Types.array_element_type expr.expr_type in
+ let expr_of_const c =
+ { expr_desc = Expr_const c;
+ expr_type = typ;
+ expr_clock = expr.expr_clock;
+ expr_loc = expr.expr_loc;
+ expr_delay = Delay.new_var ();
+ expr_annot = None;
+ expr_tag = new_tag ();
+ }
+ in { expr with expr_desc = Expr_array (List.map expr_of_const cl) }
+ | _ -> assert false
+
+(* inject_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
+let rec inject_list alias node inject_element defvars elist =
+ List.fold_right
+ (fun t (defvars, qlist) ->
+ let defvars, norm_t = inject_element alias node defvars t in
+ (defvars, norm_t :: qlist)
+ ) elist (defvars, [])
+
+let rec inject_expr ?(alias=true) node defvars expr =
+let res=
+ match expr.expr_desc with
+ | Expr_const (Const_real _) -> mk_expr_alias_opt alias node defvars expr
+ | Expr_const (Const_array _) -> inject_expr ~alias:alias node defvars (expr_of_const_array expr)
+ | Expr_const (Const_struct _) -> assert false
+ | Expr_ident _
+ | Expr_const _ -> defvars, expr
+ | Expr_array elist ->
+ let defvars, norm_elist = inject_list alias node (fun _ -> inject_expr ~alias:true) defvars elist in
+ let norm_expr = { expr with expr_desc = Expr_array norm_elist } in
+ defvars, norm_expr
+ | Expr_power (e1, d) ->
+ let defvars, norm_e1 = inject_expr node defvars e1 in
+ let norm_expr = { expr with expr_desc = Expr_power (norm_e1, d) } in
+ defvars, norm_expr
+ | Expr_access (e1, d) ->
+ let defvars, norm_e1 = inject_expr node defvars e1 in
+ let norm_expr = { expr with expr_desc = Expr_access (norm_e1, d) } in
+ defvars, norm_expr
+ | Expr_tuple elist ->
+ let defvars, norm_elist =
+ inject_list alias node (fun alias -> inject_expr ~alias:alias) defvars elist in
+ let norm_expr = { expr with expr_desc = Expr_tuple norm_elist } in
+ defvars, norm_expr
+ | Expr_appl (id, args, r) ->
+ let defvars, norm_args = inject_expr node defvars args in
+ let norm_expr = { expr with expr_desc = Expr_appl (id, norm_args, r) } in
+ mk_expr_alias_opt alias node defvars (inject_call norm_expr)
+ | Expr_arrow _ -> defvars, expr
+ | Expr_pre e ->
+ let defvars, norm_e = inject_expr node defvars e in
+ let norm_expr = { expr with expr_desc = Expr_pre norm_e } in
+ defvars, norm_expr
+ | Expr_fby (e1, e2) ->
+ let defvars, norm_e1 = inject_expr node defvars e1 in
+ let defvars, norm_e2 = inject_expr node defvars e2 in
+ let norm_expr = { expr with expr_desc = Expr_fby (norm_e1, norm_e2) } in
+ defvars, norm_expr
+ | Expr_when (e, c, l) ->
+ let defvars, norm_e = inject_expr node defvars e in
+ let norm_expr = { expr with expr_desc = Expr_when (norm_e, c, l) } in
+ defvars, norm_expr
+ | Expr_ite (c, t, e) ->
+ let defvars, norm_c = inject_expr node defvars c in
+ let defvars, norm_t = inject_expr node defvars t in
+ let defvars, norm_e = inject_expr node defvars e in
+ let norm_expr = { expr with expr_desc = Expr_ite (norm_c, norm_t, norm_e) } in
+ defvars, norm_expr
+ | Expr_merge (c, hl) ->
+ let defvars, norm_hl = inject_branches node defvars hl in
+ let norm_expr = { expr with expr_desc = Expr_merge (c, norm_hl) } in
+ defvars, norm_expr
+in
+(*Format.eprintf "inject_expr %B %a = %a@." alias Printers.pp_expr expr Printers.pp_expr (snd res);*)
+res
+
+and inject_branches node defvars hl =
+ List.fold_right
+ (fun (t, h) (defvars, norm_q) ->
+ let (defvars, norm_h) = inject_expr node defvars h in
+ defvars, (t, norm_h) :: norm_q
+ )
+ hl (defvars, [])
+
+
+let rec inject_eq node defvars eq =
+ let (defs', vars'), norm_rhs = inject_expr ~alias:false node defvars eq.eq_rhs in
+ let norm_eq = { eq with eq_rhs = norm_rhs } in
+ norm_eq::defs', vars'
+
+(** normalize_node node returns a normalized node,
+ ie.
+ - updated locals
+ - new equations
+ -
+*)
+let inject_node node =
+ cpt_fresh := 0;
+ let inputs_outputs = node.node_inputs@node.node_outputs in
+ let is_local v =
+ List.for_all ((!=) v) inputs_outputs in
+ let orig_vars = inputs_outputs@node.node_locals in
+ let defs, vars =
+ List.fold_left (inject_eq node) ([], orig_vars) (get_node_eqs node) in
+ (* Normalize the asserts *)
+ let vars, assert_defs, asserts =
+ List.fold_left (
+ fun (vars, def_accu, assert_accu) assert_ ->
+ let assert_expr = assert_.assert_expr in
+ let (defs, vars'), expr =
+ inject_expr
+ ~alias:false
+ node
+ ([], vars) (* defvar only contains vars *)
+ assert_expr
+ in
+ vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
+ ) (vars, [], []) node.node_asserts in
+ let new_locals = List.filter is_local vars in
+ (* Compute traceability info:
+ - gather newly bound variables
+ - compute the associated expression without aliases
+ *)
+ (* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals)) new_locals in *)
+ let node =
+ { node with
+ node_locals = new_locals;
+ node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
+ }
+ in ((*Printers.pp_node Format.err_formatter node;*) node)
+
+let inject_decl decl =
+ match decl.top_decl_desc with
+ | Node nd ->
+ {decl with top_decl_desc = Node (inject_node nd)}
+ | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
+
+let inject_prog decls =
+ List.map inject_decl decls
+
+
+(* Local Variables: *)
+(* compile-command:"make -C .." *)
+(* End: *)
diff --git a/src/plugins.ml b/src/plugins.ml
new file mode 100644
index 0000000000000000000000000000000000000000..44fccd4b2805de3c30131d4f32dfd0a41dc8a3fd
--- /dev/null
+++ b/src/plugins.ml
@@ -0,0 +1,35 @@
+open LustreSpec
+
+module type PluginType =
+sig
+
+end
+
+
+
+let inline_annots rename_var_fun annot_list =
+ List.map (
+ fun ann ->
+ { ann with
+ annots = List.fold_left (
+ fun accu (sl, eexpr) ->
+ let items =
+ match sl with
+ | plugin_name::args ->
+ if plugin_name = "salsa" then
+ match args with
+ | ["ranges";varname] ->
+ [["salsa";"ranges";(rename_var_fun varname)], eexpr]
+ | _ -> [(sl, eexpr)]
+ else
+ [(sl, eexpr)]
+ | _ -> assert false
+ in
+ items@accu
+ ) [] ann.annots
+ }
+ ) annot_list
+
+(* Local Variables: *)
+(* compile-command:"make -C .." *)
+(* End: *)
diff --git a/test/test-compile.sh.in b/test/test-compile.sh.in
new file mode 100755
index 0000000000000000000000000000000000000000..6ff6838d211a9b4975315cf7a59de1486afac664
--- /dev/null
+++ b/test/test-compile.sh.in
@@ -0,0 +1,271 @@
+#!/bin/bash
+
+eval set -- $(getopt -n $0 -o "-aciwvh:" -- "$@")
+
+declare c i w h a v
+declare -a files
+
+SRC_PREFIX=@SRC_PATH@-tests/
+#SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler
+NOW=`date "+%y%m%d%H%M"`
+report=`pwd`/report-@PACKAGE_VERSION@-$NOW
+LUSTREC=lustrec
+mkdir -p build
+build=`pwd`"/build"
+
+gcc_compile() {
+ if [ $verbose -gt 1 ]; then
+ echo "gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ $1.c > /dev/null"
+ fi
+ 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() {
+ if [ $verbose -gt 1 ]; then
+ echo "$LUSTREC $@"
+ fi
+ $LUSTREC "$@";
+ if [ $? -ne 0 ]; then
+ rlustrec="INVALID";
+ else
+ rlustrec="VALID"
+ fi
+}
+
+base_compile() {
+ while IFS=, read -r file main opts
+ do
+ name=`basename "$file" .lus`
+ ext=".lus"
+ if [ `dirname "$file"`/"$name" = "$file" ]; then
+ name=`basename "$file" .lusi`
+ ext=".lusi"
+ fi
+ dir=${SRC_PREFIX}/`dirname "$file"`
+ pushd $dir > /dev/null
+
+ if [ "$main" != "" ]; then
+ lustrec_compile -d $build -verbose 0 $opts -node $main $name$ext;
+ else
+ lustrec_compile -d $build -verbose 0 $opts $name$ext
+ fi
+ pushd $build > /dev/null
+
+ if [ $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 ($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
+}
+
+inline_compile () {
+ while IFS=, read -r file main opts
+ do
+ name=`basename "$file" .lus`
+ ext=".lus"
+ if [ `dirname "$file"`/"$name" = "$file" ]; then
+ name=`basename "$file" .lusi`
+ ext=".lusi"
+ fi
+ dir=${SRC_PREFIX}/`dirname "$file"`
+ pushd $dir > /dev/null
+
+ 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 () {
+# Checking inlining
+ while IFS=, read -r file main opts
+ do
+ name=`basename "$file" .lus`
+ ext=".lus"
+ if [ `dirname "$file"`/"$name" = "$file" ]; then
+ name=`basename "$file" .lusi`
+ ext=".lusi"
+ fi
+ dir=${SRC_PREFIX}/`dirname "$file"`
+ pushd $dir > /dev/null
+
+ 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
+ popd > /dev/null
+ pushd $build > /dev/null
+
+ if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
+ gcc_compile "$name";
+ else
+ rgcc="NONE"
+ fi
+ # Cheching witness
+
+ if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
+ mv ${name}_witnesses/inliner_witness.lus ${name}_inliner_witness.lus
+ lustrec_compile -verbose 0 -horn-traces -node check ${name}_inliner_witness.lus
+ z3="`z3 -T:10 ${name}_inliner_witness.smt2 | xargs`"
+ if [ "x`echo $z3 | grep -o unsat`" == "xunsat" ]; then
+ rinlining="VALID";
+ elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
+ rinlining="ERROR";
+ elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
+ rinlining="UNKNOWN";
+ elif [ "x`echo $z3 | xargs | grep -o timeout`" == "xtimeout" ]; then
+ rinlining="TIMEOUT"
+ else
+ rinlining="INVALID"
+ fi
+ else
+ rinlining="NONE"
+ fi
+ popd > /dev/null
+
+ if [ $verbose -gt 0 ]; then
+ echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining check ($rinlining), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
+ else
+ echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining check ($rinlining), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "TIMEOUT\|INVALID\|ERROR\|UNKNOWN"
+ fi
+done < $file_list
+
+}
+
+check_prop () {
+ while IFS=, read -r file main opts
+ do
+ name=`basename "$file" .lus`
+ if [ "$name" = "$file" ]; then
+ return 0
+ fi
+ dir=${SRC_PREFIX}/`dirname "$file"`
+ pushd $dir > /dev/null
+
+ # Checking horn backend
+ if [ "$main" != "" ]; then
+ lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts -node $main $name".lus";
+ else
+ lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts $name".lus"
+ fi
+
+ # echo "z3 $build/$name".smt2
+ # TODO: This part of the script has to be optimized
+ z3="`z3 -T:10 ${build}/${name}.smt2 | xargs`"
+ if [ "x`echo $z3 | grep -o unsat`" == "xunsat" ]; then
+ rhorn="VALID";
+ elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
+ rhorn="ERROR";
+ elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
+ rhorn="UNKNOWN";
+ elif [ "x`echo $z3 | xargs | grep -o timeout`" == "xtimeout" ]; then
+ rhorn="TIMEOUT"
+ else
+ rhorn="INVALID"
+ fi
+ if [ $verbose -gt 0 ]; then
+ echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
+ else
+ echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
+ fi
+ popd > /dev/null
+done < $file_list
+}
+
+usage () {
+echo "usage: $0 [-aciwh] file_list"
+echo "-a: perform all steps"
+echo "-c: basic compilation"
+echo "-i: compile with inline mode"
+echo "-w: compile with inline mode. Check the inlining with z3"
+echo "-h: check files with the horn-pdf backend (requires z3)"
+echo "-v <int>: verbose level"
+}
+
+verbose=0
+nobehavior=1
+
+while [ $# -gt 0 ] ; do
+ case "$1" in
+ -v) shift ; verbose="$1"; shift ;;
+ -a) nobehavior=0; c=1 ; w=1; h=1; shift ;;
+ -c) nobehavior=0; c=1 ; shift ;;
+ -i) nobehavior=0; i=1 ; shift ;;
+ -w) nobehavior=0; w=1 ; shift ;;
+ -h) nobehavior=0; h=1 ; shift ;;
+ --) shift ;;
+ -*) echo "bad option '$1'" ; exit 1 ;;
+ *) files=("${files[@]}" "$1") ; shift ;;
+ esac
+done
+
+file_list=${files[0]}
+
+
+if [ ${#files} -eq 0 ] ; then
+ echo input list required
+ usage
+ 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
+[ ! -z "$h" ] && check_prop
+[ "$nobehavior" -eq 1 ] && echo "Must provide an argument in [aciwh]" && usage
+
+
+ # Removing Generated lusi file
+ #grep generated ../${file}i > /dev/null
+ #if [ $? -ne 1 ];then
+ # rm ../${file}i
+ #fi
+