diff --git a/Makefile.dev b/Makefile.dev
index 2e2e72588effbf2bb59ef87719c1b115543a9707..bc9881e732bb913bcab6feec587bd2f2fd143302 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -40,6 +40,8 @@ update_version:
cp _oasis _oasis.save
cat _oasis.save | sed "s/^Version:.*/Version: $(VERSION)/" > _oasis
rm committed
+ git add _oasis
+ git add src/lv6version.ml
make clean && make
cia:
diff --git a/_oasis b/_oasis
index 418233bbc800f9c447719a8e8933787bf6668326..ba14a2ddd663b18e65d46ea48883c80e229c80a0 100644
--- a/_oasis
+++ b/_oasis
@@ -1,6 +1,6 @@
OASISFormat: 0.4
Name: lustre-v6
-Version: 1.681
+Version: 1.684
Synopsis: The Lustre V6 Verimag compiler
Description: This package contains:
(1) lus2lic: the (current) name of the compiler (and interpreter via -exec).
diff --git a/src/l2lExpandMetaOp.ml b/src/l2lExpandMetaOp.ml
index a43692b740a8d2b4406605d8360a2981f3bcedbd..270b5d61b133410ab6d80909a10c7d6f50db1329 100644
--- a/src/l2lExpandMetaOp.ml
+++ b/src/l2lExpandMetaOp.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 24/11/2016 (at 16:30) by Erwan Jahier> *)
+(** Time-stamp: <modified the 20/02/2017 (at 11:30) by Erwan Jahier> *)
open Lxm
open Lic
@@ -210,7 +210,9 @@ let (create_fillred_body: local_ctx -> Lic.static_arg list ->
Hence:
node(acc_in:tau; X1:tau_1^c ; ... ; Xn:tau_n^c)
returns (acc_out:tau; Y1:teta_1^c; ... ; Yl:teta_l^c) = fillred<<n,c>>;
- *)
+ *)
+ assert (lctx.node.Lic.inlist_eff <> []);
+ assert (lctx.node.Lic.outlist_eff <> []);
let (acc_in : var_info) = List.hd lctx.node.Lic.inlist_eff in
let (y1_yl : var_info list) = List.tl lctx.node.Lic.inlist_eff in
let (acc_out: var_info) = List.hd lctx.node.Lic.outlist_eff in
@@ -386,8 +388,10 @@ let (create_boolred_body: local_ctx -> int -> int -> int -> Lic.node_body * var_
)
index_list
in
- let cpt_rigth = List.fold_left (binop_to_val_exp lxm "plus")
- (List.hd ite_list) (List.tl ite_list) in
+ let cpt_rigth =
+ assert(ite_list<>[]);
+ List.fold_left (binop_to_val_exp lxm "plus")
+ (List.hd ite_list) (List.tl ite_list) in
let res_left = LeftVarLic (res_vi,lxm) in
let res_rigth = (* i <= cpt && cpt <= j; *)
let i_eff = val_exp_of_int lxm (string_of_int i) BaseLic in
diff --git a/src/licMetaOp.ml b/src/licMetaOp.ml
index e0ee06f5d7e3bab1fde0d89f0b7f63c6a545a66a..1af5930a7f98bf40e4fcea610d51090bac8a931a 100644
--- a/src/licMetaOp.ml
+++ b/src/licMetaOp.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 30/11/2016 (at 17:06) by Erwan Jahier> *)
+(* Time-stamp: <modified the 20/02/2017 (at 11:26) by Erwan Jahier> *)
(* *)
@@ -174,6 +174,7 @@ fun nk2nd nk lxm ->
(* ok pour les args statiques, le profil dynamique est : *)
let clk = Lic.create_var AstCore.VarInput Bool_type_eff "activate" in
+ assert(in_types<>[]);
let ins = clk::
Lic.create_var_list AstCore.VarInput (List.tl in_types) in
let outs = Lic.create_var_list AstCore.VarOutput out_types in
diff --git a/src/lv6MainArgs.ml b/src/lv6MainArgs.ml
index 50209c6e12c7222b5699f19454a28f1728f84aa4..0716c2d897c416bb8bb2f3d3cdd787ad4ab58aa3 100644
--- a/src/lv6MainArgs.ml
+++ b/src/lv6MainArgs.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 22/12/2016 (at 16:20) by jahier> *)
+(* Time-stamp: <modified the 13/01/2017 (at 15:41) by Erwan Jahier> *)
(*
Le manager d'argument adapté de celui de lutin, plus joli
N.B. solution un peu batarde : les options sont stockées, comme avant, dans Global,
@@ -475,6 +475,7 @@ let mkoptab (opt:t) : unit = (
(Arg.Unit (fun i ->
set_c_options opt;
global_opt.gen_wcet <- true;
+ global_opt.soc2c_no_switch <-true;
global_opt.soc2c_global_ctx <- true))
["generates a main file for computing the wcet (force -2c -2cgc)"]
;
diff --git a/src/lv6version.ml b/src/lv6version.ml
index ef36a5a17aeeeb0cbae4ba4049fe1c2a4d20f99e..91d620e3bd0e5357c15aa3a6421bda53c6234346 100644
--- a/src/lv6version.ml
+++ b/src/lv6version.ml
@@ -1,7 +1,7 @@
(** Automatically generated from Makefile *)
let tool = "lus2lic"
let branch = "master"
-let commit = "683"
-let sha_1 = "c6fc6f718951de807ba2f8d855b9473952d8331c"
+let commit = "684"
+let sha_1 = "91428de2baac6fdec5f01f358e5182817893b725"
let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")")
let maintainer = "jahier@imag.fr"
diff --git a/src/soc2c.ml b/src/soc2c.ml
index 5b235a5e96d5eeed0546aa4357d44070351dd7e9..41c1b72385193d4534ade8749316490a6dc86303 100644
--- a/src/soc2c.ml
+++ b/src/soc2c.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 11/01/2017 (at 18:26) by Erwan Jahier> *)
+(* Time-stamp: <modified the 31/01/2017 (at 16:05) by Erwan Jahier> *)
(* let put (os: out_channel) (fmt:('a, unit, string, unit) format4) : 'a = *)
@@ -966,7 +966,7 @@ typedef float _float;
let ocsh = open_out (node ^".sh") in
let main_file, ogensim_main_file, gcc =
if Lv6MainArgs.global_opt.Lv6MainArgs.gen_wcet then
- base^"_main.c",base^"_loop.c","arm-elf-gcc --specs=linux.specs -g"
+ base^"_main.c",base^"_loop.c","$gcc --specs=linux.specs -g"
else
loopfile, "I am a dead string...", "gcc"
in
@@ -987,18 +987,18 @@ set -x
otawa=\"true\"
ogensim=\"true\"
xpdf=\"true\"
-#ifndef OGENSIM
- OGENSIM=osim.arm
-#endif
-#ifndef OTAWA
- OTAWA=owcet.arm
-#endif
-#ifndef ORANGE
- ORANGE=orange
-#endif
-#ifndef LUSTREV6
- LUSTREV6=lus2lic
-#endif
+
+OGENSIM=${OGENSIM:-\"osim.arm\"}
+OTAWA=${OTAWA:-\"owcet.arm\"}
+ORANGE=${ORANGE:-\"orange\"}
+LUSTREV6=${LUSTREV6:-\"lus2lic\"}
+fixffx=${fixffx:-\"fixffx\"}
+mkff=${mkff:-\"mkff\"}
+lutin=${lutin:-\"lutin\"}
+rdbg=${rdbg:-\"rdbg-batch\"}
+getstat=${getstat:-\"getstat.r\"}
+gcc=${gcc:-\"arm-elf-gcc\"}
+
if [ $# -gt 0 ]
then
@@ -1038,8 +1038,8 @@ IDIR=`readlink -f fixffx`
IDIR=`dirname \"$IDIR\"`
ARM_LOOPLOC=\"$IDIR/arm.looploc\"
-mkff -x $execfile > $n_n.ff
-fixffx $ARM_LOOPLOC -i $n_n.ff > $n_n.fixed.ffx
+$mkff -x $execfile > $n_n.ff
+$fixffx $ARM_LOOPLOC -i $n_n.ff > $n_n.fixed.ffx
# Let's run otawa (owcet.arm)\n" ^
"$OTAWA $execfile $main_step -f $n_n.fixed.ffx -f $n_n.ffx --add-prop otawa::ilp::OUTPUT_PATH=$main_step.lp \\\n\t>"^
"$n_n.owcet.arm.log 2>&1 && \n"^
@@ -1060,10 +1060,10 @@ then
"($OGENSIM "^ogensim_exe^" -ul 1 \\\n\t-e $main_step"^
" -cl $n.cycles -lp $freeport \\\n\t-iol $n.io > $n_n"^
".ogensim.log 2>&1&) && \n\nsleep 1 &&\n"^
- "(rdbg-batch -lurette -l 1000 -o ogensim.rif \\\n\t \
+ "($rdbg -lurette -l 1000 -o "^node^".rif \\\n\t \
--sut-socket \"127.0.0.1:$freeport\" \\\n\t \
- --env-stdio \"lutin -boot -rif _${n}_env.lut -n ${n}_env\" || true)) &&\n\n"^
- "getstat.r $n.cycles $WCET > $n.stat
+ --env-stdio \"$lutin -boot -rif _${n}_env.lut -n ${n}_env\" || true)) &&\n\n"^
+ "$getstat $n.cycles $WCET > $n.stat
fi
if [ \"$xpdf\" = \"true\" ]
then
diff --git a/src/socExec.ml b/src/socExec.ml
index d3a35026f698cc5b29d8461ef9c91a9982052b9f..cc37337e98dd3cbae94409ef661d9bf33dbf6b2c 100644
--- a/src/socExec.ml
+++ b/src/socExec.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 02/01/2017 (at 18:11) by Erwan Jahier> *)
+(* Time-stamp: <modified the 20/02/2017 (at 11:27) by Erwan Jahier> *)
open Soc
open Data
@@ -69,6 +69,7 @@ let rec (soc_step : Soc.step_method -> Soc.tbl -> Soc.t -> SocExecValue.ctx
| Condact(node_sk, dft_cst) -> (
let clk = SocExecValue.get_value ctx (Var ("activate",Bool)) in
let vel_in, vel_out = soc.profile in
+ assert(vel_in <> []);
let vel_in = List.map (fun x -> Var x) (List.tl vel_in) in
let vel_out = List.map (fun x -> Var x) vel_out in
let node_soc = SocUtils.find step.lxm node_sk soc_tbl in
@@ -124,7 +125,10 @@ let rec (soc_step : Soc.step_method -> Soc.tbl -> Soc.t -> SocExecValue.ctx
List.map (array_index i) iter_outputs)
| "fold" | "red" | "fill" | "fillred" ->
let a_in = Var (List.hd iter_inputs) in
- ( a_in::(List.map (array_index i) (List.tl iter_inputs)),
+ (
+ assert(iter_inputs <> []);
+ assert(iter_outputs <> []);
+ a_in::(List.map (array_index i) (List.tl iter_inputs)),
a_in::(List.map (array_index i) (List.tl iter_outputs)))
| _ -> assert false (* should not occur *)
in
diff --git a/src/socPredef.ml b/src/socPredef.ml
index a1fee695a3a16b718d7e20d349b1ff41bf9d8452..4d180b318b03c9066bac81c0eaad0b76ed5a44fa 100644
--- a/src/socPredef.ml
+++ b/src/socPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 25/11/2016 (at 17:56) by Erwan Jahier> *)
+(* Time-stamp: <modified the 20/02/2017 (at 11:28) by Erwan Jahier> *)
(** Synchronous Object Code for Predefined operators. *)
@@ -175,6 +175,7 @@ let of_soc_key : Soc.key -> Soc.t =
| _,tl, Curr(cc) -> tl,cc
| _,_,_ -> assert false
in
+ assert(tl<>[]);
let t = List.hd (List.tl tl) in
let mem:var = (get_mem_name sk t, t) in
let prof:var list * var list = sp tl in
@@ -493,7 +494,7 @@ let output_type_of_op op tl =
-> Bool
| "Lustre::real2int" -> Int
| "Lustre::int2real" -> Real
- | "Lustre::if" -> List.hd (List.tl tl)
+ | "Lustre::if" -> assert(tl<>[]);List.hd (List.tl tl)
| _ -> List.hd tl
let (soc_interface_of_pos_op: