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

Add a few test files.

parent 6c638318
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
# 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
# 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
......@@ -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
......
==> 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
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
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
node double_delay(x: bool) returns (r,pr: bool);
let
r = x fby x fby x;
pr = r fby r;
tel
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
(* 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
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
node plus(a: int ; b: int) returns (d: int);
let
d = a + b;
tel
node test_boolred(t:bool^5) returns (res:bool);
let
res = boolred<<1,2,5>>(t);
tel
\ No newline at end of file
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
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