Skip to content
Snippets Groups Projects
Commit 75178f1d authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Fix a bug when expanding boolred.

Some generated intermediary variables where declared as int instead
of bool.  Funnily, ecexe was ok with that...
parent 360a5c23
No related branches found
No related tags found
No related merge requests found
(** Time-stamp: <modified the 04/06/2013 (at 14:43) by Erwan Jahier> *)
(** Time-stamp: <modified the 22/01/2014 (at 16:39) by Erwan Jahier> *)
open Lxm
open Lic
......@@ -104,6 +104,14 @@ let (binop_to_val_exp : Ident.t -> val_exp -> val_exp -> val_exp) =
ve_typ = ve1.ve_typ;
ve_core = CallByPosLic(op, [ve1; ve2])
}
let (binop_to_val_exp_bool : Ident.t -> val_exp -> val_exp -> val_exp) =
fun op ve1 ve2 ->
let op = { it = PREDEF_CALL({src=lxm;it=("Lustre",op),[]}) ; src = lxm } in
{
ve_clk = ve1.ve_clk;
ve_typ = [Bool_type_eff];
ve_core = CallByPosLic(op, [ve1; ve2])
}
let (fby_to_val_exp : val_exp -> val_exp -> val_exp) =
fun ve1 ve2 ->
let op = { it = FBY ; src = lxm } in
......@@ -302,11 +310,11 @@ let (create_boolred_body: local_ctx -> int -> int -> int -> Lic.node_body * var_
<=>
node toto(tab:bool^n) returns (res:bool);
var
cpt:int;
let
cpt = (if tab[0] then 1 else 0) + ... + (if tab[k-1] then 1 else 0);
res = i <= cpt && cpt <= j;
tel
cpt:int;
let
cpt = (if tab[0] then 1 else 0) + ... + (if tab[k-1] then 1 else 0);
res = i <= cpt && cpt <= j;
tel
*)
assert(0 <= i && i <= j && j <= k && k>0);
let (tab_vi : var_info) = match lctx.node.Lic.inlist_eff with
......@@ -336,8 +344,8 @@ let (create_boolred_body: local_ctx -> int -> int -> int -> Lic.node_body * var_
let i_eff = val_exp_of_int (string_of_int i) in
let j_eff = val_exp_of_int (string_of_int j) in
let cpt_eff = val_exp_of_var_info cpt_vi in
let i_inf_cpt = binop_to_val_exp "lte" i_eff cpt_eff in
let cpt_inf_j = binop_to_val_exp "lte" cpt_eff j_eff in
let i_inf_cpt = binop_to_val_exp_bool "lte" i_eff cpt_eff in
let cpt_inf_j = binop_to_val_exp_bool "lte" cpt_eff j_eff in
binop_to_val_exp "and" i_inf_cpt cpt_inf_j
in
let cpt_eq = { src = lxm ; it = ([cpt_left], cpt_rigth) } in
......
......@@ -2,6 +2,6 @@
let tool = "lus2lic"
let branch = "(no"
let commit = "433"
let sha_1 = "0b46db200d272357a11ce46ca7311d8a34f26a9f"
let sha_1 = "360a5c237ffd24aaae3d180f62ecf25cb539fb4d"
let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")")
let maintainer = "jahier@imag.fr"
Test Run By jahier on Wed Jan 22 14:16:58 2014
Test Run By jahier on Wed Jan 22 17:58:47 2014
Native configuration is i686-pc-linux-gnu
=== lus2lic tests ===
......@@ -1028,7 +1028,5 @@ XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/seman
# of unexpected failures 76
# of unexpected successes 21
# of expected failures 37
testcase ./lus2lic.tests/non-reg.exp completed in 101 seconds
testcase ./lus2lic.tests/progression.exp completed in 1 seconds
testcase ./lus2lic.tests/non-reg.exp completed in 101 seconds
testcase ./lus2lic.tests/non-reg.exp completed in 110 seconds
testcase ./lus2lic.tests/progression.exp completed in 1 seconds
testcase ./lus2lic.tests/non-reg.exp completed in 101 seconds
testcase ./lus2lic.tests/non-reg.exp completed in 110 seconds
testcase ./lus2lic.tests/progression.exp completed in 1 seconds
......@@ -74,7 +74,7 @@ if
$RDBG_PATH/rdbgbatch.native -lurette --seed 42 -p 6 -l 10 --stop-on-oracle-error \
--sut-stdio "./patch_ecexe $ec $lv4_node" \
--env-stdio "./lutin -boot -rif $env" \
--oracle-stdio "./lus2lic -exec -rif $_oracle -n $oracle" --debug-me ;
--oracle-stdio "./lus2lic -exec -rif $_oracle -n $oracle" ;
then
echo "rdbg -lurette: ok"
else
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment