diff --git a/src/l2lCheckKcgKeyWord.ml b/src/l2lCheckKcgKeyWord.ml
index 7a0980007552135c4ba870d042d82e9aae8f2cf6..388eda8c66eb74b17222ccd3e08d800bfa3ed5a4 100644
--- a/src/l2lCheckKcgKeyWord.ml
+++ b/src/l2lCheckKcgKeyWord.ml
@@ -18,15 +18,17 @@ module StringSet =
let kcg_kw_list = ["state";"clock";"initial"]
let kcg_kw = StringSet.of_list kcg_kw_list
-let (check_var_info : Lic.var_info-> unit) =
+let (check_var_info : Lic.var_info -> unit) =
fun v ->
(match v with
|var_name_eff->
- if StringSet.mem v.var_name_eff kcg_kw then
- assert false;
+ if StringSet.mem v.var_name_eff kcg_kw then
+ (let msg = "kcg name clash" in
+ raise (Lv6errors.Global_error msg)
+ );
|_ -> ()
- )
+ )
let (check_type :Lic.type_ -> unit) =
diff --git a/src/licDump.ml b/src/licDump.ml
index ec0e7473ed382dd547ae709feeef32752aaddbc9..9b818942ffc46b6a5cd81bc62267479cc43966e2 100644
--- a/src/licDump.ml
+++ b/src/licDump.ml
@@ -465,9 +465,9 @@ and (string_of_by_pos_op_eff: Lic.by_pos_op srcflagged -> Lic.val_exp list -> st
| WHEN clk, vel -> (tuple vel) ^ (string_of_clock clk)
- | CURRENT Some _,_ -> (*if global_opt.kcg then "merge " ^ tuple_par vel ^ " (true -> " ^
- (tuple_par vel) ^ ") (false -> pre " ^ (tuple_par vel) ^")"
- else *)"current " ^ tuple_par (if global_opt.ec then List.tl vel else vel)
+ | CURRENT Some _,_ -> if global_opt.kcg then
+ "merge " ^ tuple_par (List.tl vel) ^ " (true -> " ^(tuple_par (List.tl vel)) ^ ") (false -> pre " ^ (tuple_par (List.tl vel)) ^ ")"
+ else "current " ^ tuple_par (if global_opt.ec then List.tl vel else vel)
| CURRENT None,_ -> (*if global_opt.kcg then else *) "current " ^ tuple_par vel
| TUPLE,_ -> (tuple vel)
| CONCAT, [ve1; ve2] ->
@@ -596,7 +596,7 @@ and string_of_eq_info_eff (leff_list, vee) =
and (string_of_assert : Lic.val_exp srcflagged -> string ) =
fun eq_eff ->
wrap_long_line (
- if global_opt.kcg then "assume ID : " ^ string_of_val_exp_eff eq_eff.it ^ ";"
+ if global_opt.kcg then "assume " ^ FreshName.local_var "A" ^ ": " ^ string_of_val_exp_eff eq_eff.it ^ ";"
else
"assert(" ^ string_of_val_exp_eff eq_eff.it ^ ");")
diff --git a/test/lus2lic-kcg.sum b/test/lus2lic-kcg.sum
index e17d88f76fa0e3215ddf229dc13ec28531a46b88..b18f2fb05d44abbae49ab8f9ca8f1b50f7564845 100644
--- a/test/lus2lic-kcg.sum
+++ b/test/lus2lic-kcg.sum
@@ -1,4 +1,4 @@
-Test Run By ndiaye on Thu Jun 25 09:41:30 2015
+Test Run By ndiaye on Fri Jul 3 11:13:08 2015
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic-kcg tests ===
@@ -35,15 +35,12 @@ PASS: /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c SOURIS_scade.lus -n
PASS: ./lus2lic {-kcg -o STABLE_scade.lus STABLE.lus -n STABLE}
FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c STABLE_scade.lus -node STABLE
PASS: ./lus2lic {-kcg -o SWITCH_scade.lus SWITCH.lus -n SWITCH}
-FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c SWITCH_scade.lus -node SWITCH
PASS: ./lus2lic {-kcg -o SWITCH1_scade.lus SWITCH1.lus -n SWITCH1}
-FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c SWITCH1_scade.lus -node SWITCH1
PASS: ./lus2lic {-kcg -o TIME_STABLE_scade.lus TIME_STABLE.lus -n TIME_STABLE}
FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c TIME_STABLE_scade.lus -node TIME_STABLE
PASS: ./lus2lic {-kcg -o TIME_STABLE1_scade.lus TIME_STABLE1.lus -n TIME_STABLE1}
FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c TIME_STABLE1_scade.lus -node TIME_STABLE1
PASS: ./lus2lic {-kcg -o Watch_scade.lus Watch.lus -n Watch}
-FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c Watch_scade.lus -node Watch
PASS: ./lus2lic {-kcg -o X_scade.lus X.lus -n X}
FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c X_scade.lus -node X
PASS: ./lus2lic {-kcg -o X2_scade.lus X2.lus -n X2}
@@ -65,7 +62,6 @@ PASS: /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c after_scade.lus -no
PASS: ./lus2lic {-kcg -o alias_scade.lus alias.lus -n alias}
FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c alias_scade.lus -node alias
PASS: ./lus2lic {-kcg -o arbitre_scade.lus arbitre.lus -n arbitre}
-FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c arbitre_scade.lus -node arbitre
PASS: ./lus2lic {-kcg -o argos_scade.lus argos.lus -n argos}
PASS: /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c argos_scade.lus -node argos
PASS: ./lus2lic {-kcg -o array_concat_scade.lus array_concat.lus -n array_concat}
@@ -129,7 +125,6 @@ FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/mi
PASS: ./lus2lic {-kcg -o clock_ite_scade.lus clock_ite.lus -n clock_ite}
FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c clock_ite_scade.lus -node clock_ite
PASS: ./lus2lic {-kcg -o cminus_scade.lus cminus.lus -n cminus}
-FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c cminus_scade.lus -node cminus
PASS: ./lus2lic {-kcg -o complex_scade.lus complex.lus -n complex}
PASS: /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c complex_scade.lus -node complex
PASS: ./lus2lic {-kcg -o compteur_scade.lus compteur.lus -n compteur}
@@ -177,7 +172,6 @@ FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/mi
PASS: ./lus2lic {-kcg -o filter_scade.lus filter.lus -n filter}
PASS: /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c filter_scade.lus -node filter
PASS: ./lus2lic {-kcg -o flo_scade.lus flo.lus -n flo}
-FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c flo_scade.lus -node flo
PASS: ./lus2lic {-kcg -o followed_by_scade.lus followed_by.lus -n followed_by}
PASS: /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c followed_by_scade.lus -node followed_by
PASS: ./lus2lic {-kcg -o fresh_name_scade.lus fresh_name.lus -n fresh_name}
@@ -275,13 +269,9 @@ PASS: /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c morel4_scade.lus -n
PASS: ./lus2lic {-kcg -o morel5_scade.lus morel5.lus -n morel5}
PASS: /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c morel5_scade.lus -node morel5
PASS: ./lus2lic {-kcg -o mouse_scade.lus mouse.lus -n mouse}
-FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c mouse_scade.lus -node mouse
PASS: ./lus2lic {-kcg -o mouse1_scade.lus mouse1.lus -n mouse1}
-FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c mouse1_scade.lus -node mouse1
PASS: ./lus2lic {-kcg -o mouse2_scade.lus mouse2.lus -n mouse2}
-FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c mouse2_scade.lus -node mouse2
PASS: ./lus2lic {-kcg -o mouse3_scade.lus mouse3.lus -n mouse3}
-FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c mouse3_scade.lus -node mouse3
PASS: ./lus2lic {-kcg -o moyenne_scade.lus moyenne.lus -n moyenne}
FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c moyenne_scade.lus -node moyenne
PASS: ./lus2lic {-kcg -o multiclock_scade.lus multiclock.lus -n multiclock}
@@ -324,13 +314,11 @@ FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/mi
PASS: ./lus2lic {-kcg -o notTwo_scade.lus notTwo.lus -n notTwo}
PASS: /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c notTwo_scade.lus -node notTwo
PASS: ./lus2lic {-kcg -o o2l_feux_compl_scade.lus o2l_feux_compl.lus -n o2l_feux_compl}
-FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c o2l_feux_compl_scade.lus -node o2l_feux_compl
+PASS: /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c o2l_feux_compl_scade.lus -node o2l_feux_compl
PASS: ./lus2lic {-kcg -o oneq_scade.lus oneq.lus -n oneq}
PASS: /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c oneq_scade.lus -node oneq
PASS: ./lus2lic {-kcg -o onlyroll_scade.lus onlyroll.lus -n onlyroll}
-FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c onlyroll_scade.lus -node onlyroll
PASS: ./lus2lic {-kcg -o onlyroll2_scade.lus onlyroll2.lus -n onlyroll2}
-FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c onlyroll2_scade.lus -node onlyroll2
PASS: ./lus2lic {-kcg -o over2_scade.lus over2.lus -n over2}
FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c over2_scade.lus -node over2
PASS: ./lus2lic {-kcg -o over3_scade.lus over3.lus -n over3}
@@ -366,8 +354,8 @@ PASS: ./lus2lic {-kcg -o ply03_scade.lus ply03.lus -n ply03}
FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c ply03_scade.lus -node ply03
PASS: ./lus2lic {-kcg -o polymorphic_pack_scade.lus polymorphic_pack.lus -n polymorphic_pack}
PASS: ./lus2lic {-kcg -o poussoir_scade.lus poussoir.lus -n poussoir}
-FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c poussoir_scade.lus -node poussoir
-FAIL: Test -kcg : ./lus2lic {-kcg -o pplus_scade.lus pplus.lus -n pplus}
+PASS: ./lus2lic {-kcg -o pplus_scade.lus pplus.lus -n pplus}
+PASS: /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c pplus_scade.lus -node pplus
PASS: ./lus2lic {-kcg -o pre_x_scade.lus pre_x.lus -n pre_x}
PASS: /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c pre_x_scade.lus -node pre_x
PASS: ./lus2lic {-kcg -o predef01_scade.lus predef01.lus -n predef01}
@@ -448,7 +436,7 @@ FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/mi
PASS: ./lus2lic {-kcg -o test_node_expand_scade.lus test_node_expand.lus -n test_node_expand}
PASS: /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c test_node_expand_scade.lus -node test_node_expand
PASS: ./lus2lic {-kcg -o test_node_expand2_scade.lus test_node_expand2.lus -n test_node_expand2}
-FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c test_node_expand2_scade.lus -node test_node_expand2
+PASS: /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c test_node_expand2_scade.lus -node test_node_expand2
PASS: ./lus2lic {-kcg -o test_poly_scade.lus test_poly.lus -n test_poly}
FAIL: Check that the generated scade code compiles : /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c test_poly_scade.lus -node test_poly
PASS: ./lus2lic {-kcg -o test_struct_scade.lus test_struct.lus -n test_struct}
@@ -498,5 +486,5 @@ PASS: /usr/local/tools/lustre/misc/scade-win32/621/bin/s2c zzz2_scade.lus -nod
=== lus2lic-kcg Summary ===
-# of expected passes 368
-# of unexpected failures 119
+# of expected passes 372
+# of unexpected failures 103