Minor and various enhancements.

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:

_oasis

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

src/l2lExpandMetaOp.ml

-(** 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

src/licMetaOp.ml

-(* 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

src/lv6MainArgs.ml

-(* 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 stockes, 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)"]
     ;

src/lv6version.ml

 (** 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"

src/soc2c.ml

-(* 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

src/socExec.ml

-(* 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

src/socPredef.ml

-(* 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: