From fbc1f4e21de5654fe455a39d49da96668a1b2555 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Thu, 18 Jun 2015 15:02:00 +0200
Subject: [PATCH] Add a few test files.
---
.gitignore | 9 ++++-
src/lustre-v6.mldylib | 63 +++++++++++++++++++++++++++++
src/lustre-v6.mllib | 63 +++++++++++++++++++++++++++++
test/Makefile | 5 ++-
test/lus2lic.sum | 60 +++++++++++++++++----------
test/lus2lic.time | 18 ++++-----
test/should_work/carligths.lus | 20 +++++++++
test/should_work/double_delay.lus | 6 +++
test/should_work/map.lus | 18 +++++++++
test/should_work/modes3x2_v4.lus | 67 +++++++++++++++++++++++++++++++
test/should_work/oneq.lus | 14 +++++++
test/should_work/pplus.lus | 4 ++
test/should_work/test_boolred.lus | 5 +++
test/should_work/test_poly.lus | 10 +++++
14 files changed, 329 insertions(+), 33 deletions(-)
create mode 100644 src/lustre-v6.mldylib
create mode 100644 src/lustre-v6.mllib
create mode 100644 test/should_work/carligths.lus
create mode 100644 test/should_work/double_delay.lus
create mode 100644 test/should_work/map.lus
create mode 100644 test/should_work/modes3x2_v4.lus
create mode 100644 test/should_work/oneq.lus
create mode 100644 test/should_work/pplus.lus
create mode 100644 test/should_work/test_boolred.lus
create mode 100644 test/should_work/test_poly.lus
diff --git a/.gitignore b/.gitignore
index dc7e4db4..43ca35bc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -29,6 +29,14 @@ release*
*.lus.tex
*.res
*.ps
+*.exec
+*.save
+*.dro
+*.rif
+*.cov
+*.gp
+*.lesar
+*.sum
*.annot
*gz
src/version.ml
@@ -55,7 +63,6 @@ lus2lic-types.pdf
lus2lic.pdf
*.tex
ocamldoc
-test/*
_build/
main.native
myocamlbuild.ml
diff --git a/src/lustre-v6.mldylib b/src/lustre-v6.mldylib
new file mode 100644
index 00000000..70b1ee4b
--- /dev/null
+++ b/src/lustre-v6.mldylib
@@ -0,0 +1,63 @@
+# OASIS_START
+# DO NOT EDIT (digest: 702371850d29477bd775b51a95b16417)
+Lus2licRun
+SocExecValue
+SocUtils
+Lv6util
+Lv6version
+Lv6errors
+Lxm
+Lv6MainArgs
+Verbose
+Soc
+SocPredef
+Lv6Id
+SocExec
+SocExecEvalPredef
+Compile
+AstTab
+AstTabSymbol
+AstInstanciateModel
+Lv6parserUtils
+AstV6
+FilenameExtras
+LicTab
+LicDump
+AstPredef
+Lic
+AstCore
+FreshName
+IdSolver
+EvalConst
+LicEvalConst
+LicEvalType
+UnifyType
+Ast2lic
+AstV6Dump
+EvalClock
+UnifyClock
+LicEvalClock
+EvalType
+LicPrg
+LicMetaOp
+L2lCheckOutputs
+Misc
+L2lRmPoly
+L2lExpandMetaOp
+L2lSplit
+L2lExpandNodes
+L2lExpandArrays
+L2lCheckLoops
+L2lCheckMemSafe
+L2lOptimIte
+Lv6lexer
+Lv6parser
+AstRecognizePredef
+Lic2soc
+Action
+ActionsDeps
+SocVar
+Lus2licRun
+SortActions
+SortActionsExpe
+# OASIS_STOP
diff --git a/src/lustre-v6.mllib b/src/lustre-v6.mllib
new file mode 100644
index 00000000..70b1ee4b
--- /dev/null
+++ b/src/lustre-v6.mllib
@@ -0,0 +1,63 @@
+# OASIS_START
+# DO NOT EDIT (digest: 702371850d29477bd775b51a95b16417)
+Lus2licRun
+SocExecValue
+SocUtils
+Lv6util
+Lv6version
+Lv6errors
+Lxm
+Lv6MainArgs
+Verbose
+Soc
+SocPredef
+Lv6Id
+SocExec
+SocExecEvalPredef
+Compile
+AstTab
+AstTabSymbol
+AstInstanciateModel
+Lv6parserUtils
+AstV6
+FilenameExtras
+LicTab
+LicDump
+AstPredef
+Lic
+AstCore
+FreshName
+IdSolver
+EvalConst
+LicEvalConst
+LicEvalType
+UnifyType
+Ast2lic
+AstV6Dump
+EvalClock
+UnifyClock
+LicEvalClock
+EvalType
+LicPrg
+LicMetaOp
+L2lCheckOutputs
+Misc
+L2lRmPoly
+L2lExpandMetaOp
+L2lSplit
+L2lExpandNodes
+L2lExpandArrays
+L2lCheckLoops
+L2lCheckMemSafe
+L2lOptimIte
+Lv6lexer
+Lv6parser
+AstRecognizePredef
+Lic2soc
+Action
+ActionsDeps
+SocVar
+Lus2licRun
+SortActions
+SortActionsExpe
+# OASIS_STOP
diff --git a/test/Makefile b/test/Makefile
index 7ce7db11..663873f6 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -130,8 +130,11 @@ lus2lic4.log:
$(TEST_MACHINE) "cd $(testdir); runtest --tool lus2lic4 lus2lic.tests/test4.exp" || true
+kcg.log:
+ $(TEST_MACHINE) "cd $(testdir); runtest --tool lus2lic-kcg lus2lic.tests/kcg.exp" || true
+
progression:
- $(TEST_MACHINE) "cd $(testdir); runtest --tool lus2lic progression.exp" || true
+ $(TEST_MACHINE) "cd $(testdir); runtest --tool lus2lic lus2lic.tests/progression.exp" || true
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index 457c45a2..f8dee0b4 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,5 +1,5 @@
==> lus2lic0.sum <==
-Test Run By jahier on Fri May 22 15:45:45
+Test Run By jahier on Thu Jun 18 11:40:19
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic0 tests ===
@@ -63,7 +63,7 @@ XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/lecte
XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/s.lus
==> lus2lic1.sum <==
-Test Run By jahier on Fri May 22 15:45:50
+Test Run By jahier on Thu Jun 18 11:40:19
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic1 tests ===
@@ -175,6 +175,7 @@ PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c call07.lus {}
PASS: ./lus2lic {-2c carV2.lus -n carV2}
PASS: gcc -o carV2.exec carV2_carV2.c carV2_carV2_loop.c
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c carV2.lus {}
+FAIL: Generate c code : ./lus2lic {-2c carligths.lus -n carligths}
PASS: ./lus2lic {-2c ck2.lus -n ck2}
PASS: gcc -o ck2.exec ck2_ck2.c ck2_ck2_loop.c
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c ck2.lus {}
@@ -397,7 +398,7 @@ PASS: gcc -o multipar.exec multipar_multipar.c multipar_multipar_loop.c
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus {}
==> lus2lic2.sum <==
-Test Run By jahier on Fri May 22 15:46:27
+Test Run By jahier on Thu Jun 18 11:40:34
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic2 tests ===
@@ -496,6 +497,9 @@ PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c notTwo.lus {}
PASS: ./lus2lic {-2c o2l_feux_compl.lus -n o2l_feux_compl}
PASS: gcc -o o2l_feux_compl.exec o2l_feux_compl_o2l_feux_compl.c o2l_feux_compl_o2l_feux_compl_loop.c
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c o2l_feux_compl.lus {}
+PASS: ./lus2lic {-2c oneq.lus -n oneq}
+PASS: gcc -o oneq.exec oneq_oneq.c oneq_oneq_loop.c
+PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c oneq.lus {}
PASS: ./lus2lic {-2c onlyroll.lus -n onlyroll}
PASS: gcc -o onlyroll.exec onlyroll_onlyroll.c onlyroll_onlyroll_loop.c
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c onlyroll.lus {}
@@ -551,6 +555,7 @@ PASS: ./lus2lic {-2c polymorphic_pack.lus -n polymorphic_pack}
PASS: ./lus2lic {-2c poussoir.lus -n poussoir}
PASS: gcc -o poussoir.exec poussoir_poussoir.c poussoir_poussoir_loop.c
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c poussoir.lus {}
+FAIL: Generate c code : ./lus2lic {-2c pplus.lus -n pplus}
PASS: ./lus2lic {-2c pre_x.lus -n pre_x}
PASS: gcc -o pre_x.exec pre_x_pre_x.c pre_x_pre_x_loop.c
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c pre_x.lus {}
@@ -727,7 +732,7 @@ PASS: gcc -o zzz2.exec zzz2_zzz2.c zzz2_zzz2_loop.c
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c zzz2.lus {}
==> lus2lic3.sum <==
-Test Run By jahier on Fri May 22 15:47:35
+Test Run By jahier on Thu Jun 18 11:41:18
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic3 tests ===
@@ -887,6 +892,10 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node call07.lus {}
PASS: ./lus2lic {-o carV2.lic carV2.lus}
PASS: ./lus2lic {-ec -o carV2.ec carV2.lus}
PASS: ./myec2c {-o carV2.c carV2.ec}
+PASS: ./lus2lic {-o carligths.lic carligths.lus}
+PASS: ./lus2lic {-ec -o carligths.ec carligths.lus}
+PASS: ./myec2c {-o carligths.c carligths.ec}
+FAIL: Try to compare lus2lic -exec and ecexe: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node carligths.lus {}
PASS: ./lus2lic {-o ck2.lic ck2.lus}
PASS: ./lus2lic {-ec -o ck2.ec ck2.lus}
PASS: ./myec2c {-o ck2.c ck2.ec}
@@ -1230,7 +1239,7 @@ PASS: ./myec2c {-o multipar.c multipar.ec}
PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node multipar.lus {}
==> lus2lic4.sum <==
-Test Run By jahier on Fri May 22 15:48:35
+Test Run By jahier on Thu Jun 18 11:41:31
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic4 tests ===
@@ -1361,6 +1370,9 @@ PASS: ./lus2lic {-o o2l_feux_compl.lic o2l_feux_compl.lus}
PASS: ./lus2lic {-ec -o o2l_feux_compl.ec o2l_feux_compl.lus}
PASS: ./myec2c {-o o2l_feux_compl.c o2l_feux_compl.ec}
PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node o2l_feux_compl.lus {}
+PASS: ./lus2lic {-o oneq.lic oneq.lus}
+PASS: ./lus2lic {-ec -o oneq.ec oneq.lus}
+PASS: ./myec2c {-o oneq.c oneq.ec}
PASS: ./lus2lic {-o onlyroll.lic onlyroll.lus}
PASS: ./lus2lic {-ec -o onlyroll.ec onlyroll.lus}
PASS: ./myec2c {-o onlyroll.c onlyroll.ec}
@@ -1446,6 +1458,10 @@ PASS: ./lus2lic {-o poussoir.lic poussoir.lus}
PASS: ./lus2lic {-ec -o poussoir.ec poussoir.lus}
PASS: ./myec2c {-o poussoir.c poussoir.ec}
PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node poussoir.lus {}
+PASS: ./lus2lic {-o pplus.lic pplus.lus}
+PASS: ./lus2lic {-ec -o pplus.ec pplus.lus}
+PASS: ./myec2c {-o pplus.c pplus.ec}
+FAIL: Try to compare lus2lic -exec and ecexe: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node pplus.lus {}
PASS: ./lus2lic {-o pre_x.lic pre_x.lus}
PASS: ./lus2lic {-ec -o pre_x.ec pre_x.lus}
PASS: ./myec2c {-o pre_x.c pre_x.ec}
@@ -1702,38 +1718,38 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {}
=== lus2lic1 Summary ===
# of expected passes 319
-# of unexpected failures 3
+# of unexpected failures 4
==> lus2lic2.sum <==
=== lus2lic2 Summary ===
-# of expected passes 316
-# of unexpected failures 2
+# of expected passes 319
+# of unexpected failures 3
==> lus2lic3.sum <==
=== lus2lic3 Summary ===
-# of expected passes 485
-# of unexpected failures 6
+# of expected passes 488
+# of unexpected failures 7
==> lus2lic4.sum <==
=== lus2lic4 Summary ===
-# of expected passes 447
-# of unexpected failures 3
+# of expected passes 453
+# of unexpected failures 4
===============================
-# Total number of failures: 14
-lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 4 seconds
-lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 36 seconds
-lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 68 seconds
-lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 59 seconds
-lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 78 seconds
+# Total number of failures: 18
+lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 0 seconds
+lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 15 seconds
+lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 44 seconds
+lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 13 seconds
+lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 47 seconds
* Ref time:
-0.05user 0.04system 4:07.91elapsed 0%CPU (0avgtext+0avgdata 5092maxresident)k
-160inputs+0outputs (0major+5512minor)pagefaults 0swaps
+0.02user 0.04system 1:59.42elapsed 0%CPU (0avgtext+0avgdata 5076maxresident)k
+0inputs+0outputs (0major+5538minor)pagefaults 0swaps
* Quick time (-j 4):
-0.05user 0.02system 1:29.15elapsed 0%CPU (0avgtext+0avgdata 5056maxresident)k
-160inputs+0outputs (0major+5562minor)pagefaults 0swaps
+0.04user 0.01system 0:57.45elapsed 0%CPU (0avgtext+0avgdata 5116maxresident)k
+96inputs+0outputs (0major+5557minor)pagefaults 0swaps
diff --git a/test/lus2lic.time b/test/lus2lic.time
index 15aa7c1f..055ec557 100644
--- a/test/lus2lic.time
+++ b/test/lus2lic.time
@@ -1,11 +1,11 @@
-lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 4 seconds
-lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 36 seconds
-lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 68 seconds
-lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 59 seconds
-lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 78 seconds
+lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 0 seconds
+lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 15 seconds
+lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 44 seconds
+lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 13 seconds
+lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 47 seconds
* Ref time:
-0.05user 0.04system 4:07.91elapsed 0%CPU (0avgtext+0avgdata 5092maxresident)k
-160inputs+0outputs (0major+5512minor)pagefaults 0swaps
+0.02user 0.04system 1:59.42elapsed 0%CPU (0avgtext+0avgdata 5076maxresident)k
+0inputs+0outputs (0major+5538minor)pagefaults 0swaps
* Quick time (-j 4):
-0.05user 0.02system 1:29.15elapsed 0%CPU (0avgtext+0avgdata 5056maxresident)k
-160inputs+0outputs (0major+5562minor)pagefaults 0swaps
+0.04user 0.01system 0:57.45elapsed 0%CPU (0avgtext+0avgdata 5116maxresident)k
+96inputs+0outputs (0major+5557minor)pagefaults 0swaps
diff --git a/test/should_work/carligths.lus b/test/should_work/carligths.lus
new file mode 100644
index 00000000..1a51ea45
--- /dev/null
+++ b/test/should_work/carligths.lus
@@ -0,0 +1,20 @@
+node carlights(TL, TR, LH, FL, LRL:bool) returns (side, low, high, fog, long:bool);
+var fog_select, long_select :bool;
+let
+ assert(not ((LH and TL) or (LH and TR)));
+ fog_select = FL;
+ long_select = LRL;
+ side = false -> (not(pre(side) or pre(low) or pre(high)) and TL) or
+ ( (pre(high) or pre(low) ) and (TL or TR)) or
+ (if not(TL or TR or LH) then pre(side) else false);
+ low = false -> (pre(side) and TL) or
+ (pre(high) and LH) or
+ (if not(TL or TR or LH) then pre(low) else false);
+ high = false -> (pre(low) and LH ) or
+ (if not(TL or TR or LH) then pre(high) else false);
+ fog = pre(low) and fog_select;
+ long = pre(high) and long_select;
+
+
+
+tel
diff --git a/test/should_work/double_delay.lus b/test/should_work/double_delay.lus
new file mode 100644
index 00000000..7174f550
--- /dev/null
+++ b/test/should_work/double_delay.lus
@@ -0,0 +1,6 @@
+
+node double_delay(x: bool) returns (r,pr: bool);
+let
+ r = x fby x fby x;
+ pr = r fby r;
+tel
diff --git a/test/should_work/map.lus b/test/should_work/map.lus
new file mode 100644
index 00000000..ce0c8f8a
--- /dev/null
+++ b/test/should_work/map.lus
@@ -0,0 +1,18 @@
+
+function myplus<<type t>>(x, y : t) returns (o : t);
+let
+ o = x + y;
+tel
+
+const n=4;
+node titi<<type t>> = map<<myplus<<t>>,n>>;
+function toto(x,y: int^n) returns (o: int^n);
+let
+ o = map<<+, n>>(x,y);
+ (* o = titi<<int>>(x,y); *)
+tel
+
+function map(x,y: real^n) returns (o: real^n);
+let
+ o = titi<<real>>(x,y);
+tel
diff --git a/test/should_work/modes3x2_v4.lus b/test/should_work/modes3x2_v4.lus
new file mode 100644
index 00000000..196b1815
--- /dev/null
+++ b/test/should_work/modes3x2_v4.lus
@@ -0,0 +1,67 @@
+(* version utilisant les horloges enumérées à la V6 *)
+
+type data = int;
+
+-- version pour otawa
+extern function A0(x:data) returns (y:data);
+extern function A1(x:data) returns (y:data);
+extern function A2(x:data) returns (y:data);
+extern function B0(x:data) returns (y:data);
+extern function B1(x:data) returns (y:data);
+
+
+
+type state = enum { idle, low, high };
+
+node A(x:data; ca1, ca2: bool) returns (y:data);
+var
+ s, ps: state;
+let
+ s = if ps = idle then (if ca1 then low else idle)
+ else if ps = low then (if ca1 then idle else if ca2 then high else low)
+ else (* ps = high *) (if ca1 then idle else if ca2 then low else high);
+ ps = idle -> pre s;
+ y = merge s
+ ( idle -> A0(x when idle(s)))
+ ( low -> A1(x when low(s)) )
+ ( high -> A2(x when high(s)));
+tel
+
+node B(x:data; nom, sby: bool) returns (z:data);
+var
+ sby_when_not_nom : bool when not nom;
+let
+ sby_when_not_nom = sby when not nom;
+ z = merge nom
+ (true -> B0(x when nom))
+ (false -> (merge sby_when_not_nom
+ (true -> B1(x when sby_when_not_nom))
+ (false -> (0 -> pre z) when not sby_when_not_nom)));
+tel
+node B_old(x:data; nom, sby: bool) returns (z:data);
+let
+ z = if nom then current (B0(x when nom))
+ else if sby then current (B1(x when sby))
+ else (0 -> pre z);
+tel
+
+node modes3x2_v4(x:data; on_off, toggle: bool) returns (res: data;
+--);
+--var
+ y, z : data;
+ sby : bool;
+ nom : bool;
+);
+let
+-- assert #(on_off, toggle);
+
+ y = A(x, on_off, toggle);
+ z = B(y, nom, sby);
+
+ (* coordination commandes *)
+ --pcritic, critic = switch(false, on_off, on_off);
+ --sleep = pcritic and (on_off or toggle);
+ sby = (on_off = (true -> pre nom));
+ nom = (on_off = (false -> pre sby));
+ res = y + z;
+tel
diff --git a/test/should_work/oneq.lus b/test/should_work/oneq.lus
new file mode 100644
index 00000000..d9a68b21
--- /dev/null
+++ b/test/should_work/oneq.lus
@@ -0,0 +1,14 @@
+node oneq(x:bool) returns (y:bool);
+let
+ y = x;
+tel
+
+type alias = int;
+type pair = struct { a:int; b:int };
+type color = enum { blue, white, black };
+
+function type_decl(i1, i2: int) returns (x: pair);
+let
+ x= pair {a=i1; b=i2};
+tel
+
diff --git a/test/should_work/pplus.lus b/test/should_work/pplus.lus
new file mode 100644
index 00000000..bcc89f9b
--- /dev/null
+++ b/test/should_work/pplus.lus
@@ -0,0 +1,4 @@
+node plus(a: int ; b: int) returns (d: int);
+let
+ d = a + b;
+tel
diff --git a/test/should_work/test_boolred.lus b/test/should_work/test_boolred.lus
new file mode 100644
index 00000000..9c13db39
--- /dev/null
+++ b/test/should_work/test_boolred.lus
@@ -0,0 +1,5 @@
+
+node test_boolred(t:bool^5) returns (res:bool);
+let
+ res = boolred<<1,2,5>>(t);
+tel
\ No newline at end of file
diff --git a/test/should_work/test_poly.lus b/test/should_work/test_poly.lus
new file mode 100644
index 00000000..340f348b
--- /dev/null
+++ b/test/should_work/test_poly.lus
@@ -0,0 +1,10 @@
+
+
+node truc = map<<+,42>>;
+
+(* PASSE DoNotPoly en spécialisant truc ! ... *)
+node test_poly(x,y: int) returns (o: int^42; o2:real^42);
+let
+ o = if (x < y) then 0^42 else truc(x^42, y^42);
+ o2=truc(3.0^42, 2.0^42);
+tel
--
GitLab