Added some tests.
This commit is contained in:
parent
93f2c8bceb
commit
207de4d6e7
10 changed files with 407 additions and 1 deletions
12
test/bad/bad_flatten.ept
Normal file
12
test/bad/bad_flatten.ept
Normal file
|
@ -0,0 +1,12 @@
|
|||
|
||||
node f(x,y : int; b : bool) returns (z : int)
|
||||
var t : int;
|
||||
let
|
||||
do
|
||||
var t2 : int; in
|
||||
t = x + t2;
|
||||
t2 = if b then 0 else 1;
|
||||
done;
|
||||
z = t2
|
||||
tel
|
||||
|
6
test/bad/bad_merge1.ept
Normal file
6
test/bad/bad_merge1.ept
Normal file
|
@ -0,0 +1,6 @@
|
|||
type t = A | B
|
||||
type tt = C
|
||||
node t2bool(x: t) returns (b: bool)
|
||||
let
|
||||
b = merge x (A-> true) (B-> true) (C-> false)
|
||||
tel
|
6
test/bad/bad_merge2.ept
Normal file
6
test/bad/bad_merge2.ept
Normal file
|
@ -0,0 +1,6 @@
|
|||
type t = A | B
|
||||
|
||||
node t2bool(x: t) returns (b: bool)
|
||||
let
|
||||
b = merge x (A-> true) (B-> true) (A-> false)
|
||||
tel
|
6
test/bad/bad_merge3.ept
Normal file
6
test/bad/bad_merge3.ept
Normal file
|
@ -0,0 +1,6 @@
|
|||
type t = A | B | C | D
|
||||
|
||||
node t2bool(x: t) returns (b: bool)
|
||||
let
|
||||
b = merge x (B-> true) (C-> true)
|
||||
tel
|
12
test/good/bad_updown.ept
Normal file
12
test/good/bad_updown.ept
Normal file
|
@ -0,0 +1,12 @@
|
|||
node updown(b : bool) returns (o : bool)
|
||||
var o',on_off:bool;
|
||||
let
|
||||
on_off = true;
|
||||
automaton
|
||||
state Down
|
||||
do o' = false until on_off then Up
|
||||
state Up
|
||||
do o' = true until on_off then Down
|
||||
end;
|
||||
o = merge b (true-> o') (false -> false)
|
||||
tel
|
17
test/good/flatten.ept
Normal file
17
test/good/flatten.ept
Normal file
|
@ -0,0 +1,17 @@
|
|||
|
||||
node f(x,y : int; b : bool) returns (z : int)
|
||||
var t : int;
|
||||
let
|
||||
do
|
||||
var t2,t2' : int; in
|
||||
t2 = if b then 0 else t2';
|
||||
do
|
||||
var t3 : int; in
|
||||
t3 = y + t;
|
||||
t2' = t3;
|
||||
done;
|
||||
t = x + t2;
|
||||
done;
|
||||
z = t;
|
||||
tel
|
||||
|
32
test/good/statics2.ept
Normal file
32
test/good/statics2.ept
Normal file
|
@ -0,0 +1,32 @@
|
|||
(* Check manually *)
|
||||
(* This test should only create two instances of f. *)
|
||||
const c2:int = 3
|
||||
const k2:int = 1
|
||||
|
||||
fun f<<n:int>>() returns (y:int)
|
||||
let
|
||||
y = n + 3 + c2;
|
||||
tel
|
||||
|
||||
fun g<<m:int>>() returns (y:int)
|
||||
var x:int;
|
||||
let
|
||||
x = m + f<<2>>();
|
||||
y = f<<m>>();
|
||||
tel
|
||||
|
||||
fun i<<m:int>>() returns (o : int)
|
||||
var x, y, z: int;
|
||||
let
|
||||
x = f<<2>>();
|
||||
y = f<<1 + m>>();
|
||||
z = f<<k2 + 1>>();
|
||||
o = f<<m + k2>>();
|
||||
tel
|
||||
|
||||
fun h() returns (y,y':int)
|
||||
let
|
||||
y = c2 + g<<c2>>() + i<<k2>>();
|
||||
y' = c2 + Statics.g<<k2>>() + Statics.i<<k2>>();
|
||||
tel
|
||||
|
|
@ -2,8 +2,9 @@
|
|||
set arguments -v test/good/t3.ept *)
|
||||
|
||||
node f(x,z:int) returns (o:int)
|
||||
var o1:int;
|
||||
var o1:int;r:bool;
|
||||
let
|
||||
r = false;
|
||||
automaton
|
||||
state Init
|
||||
do o = 1 + 2
|
||||
|
|
184
test/good/when_merge1.ept
Normal file
184
test/good/when_merge1.ept
Normal file
|
@ -0,0 +1,184 @@
|
|||
(* pour debugger ../../compiler/hec.byte -i -v -I ../../lib t1.ept *)
|
||||
(* pour debugger
|
||||
directory parsing global analysis dataflow sequential sigali simulation translation main
|
||||
set arguments -v ../test/good/t1.ept *)
|
||||
|
||||
type t = A | B
|
||||
|
||||
node bool2int(b: bool) returns (o: int)
|
||||
let
|
||||
o = merge b (true -> 1) (false -> 0)
|
||||
tel
|
||||
|
||||
node t2bool(x: t) returns (b: bool)
|
||||
let
|
||||
b = merge x (A-> true) (B-> false)
|
||||
tel
|
||||
|
||||
(*
|
||||
node mm(x: int) returns (o: int)
|
||||
var last m: int = 0;
|
||||
let
|
||||
switch (x = 0)
|
||||
| true do m = last m + 1; o = m
|
||||
| false do m = 2; o = m
|
||||
end
|
||||
tel
|
||||
|
||||
node mmm(x: int) returns (o': int)
|
||||
var last m: int = 1; o: int;
|
||||
let
|
||||
automaton
|
||||
state I
|
||||
do m = 0; o = last m + 1 until (o = 1) then J
|
||||
state J
|
||||
do m = last m + 1; o = 0
|
||||
end;
|
||||
o' = 1 -> pre o
|
||||
tel
|
||||
|
||||
node m(x: int) returns (o: int)
|
||||
var last o' : int = 1;
|
||||
let
|
||||
automaton
|
||||
state I
|
||||
do o' = 1
|
||||
unless (last o' = 2) then J
|
||||
state J
|
||||
do o' = 3
|
||||
unless (last o' = 1) then I
|
||||
end;
|
||||
o = o';
|
||||
tel
|
||||
|
||||
node h(z: int; x, y: int) returns (o2: int)
|
||||
var o1, o: int;
|
||||
let
|
||||
(o1, o2) = if z<0 then (1, 2) else (3, 4);
|
||||
o = 0 -> pre o + 2
|
||||
tel
|
||||
|
||||
node i(x, y: int) returns (o: int)
|
||||
var z, k: int;
|
||||
let
|
||||
reset
|
||||
o = 0 + x + y;
|
||||
reset
|
||||
z = 1 + o + 3;
|
||||
k = z + o + 2
|
||||
every (x = x)
|
||||
every (x = y)
|
||||
tel
|
||||
|
||||
node j(x, y: int) returns (o: int)
|
||||
let
|
||||
automaton
|
||||
state I
|
||||
var z: int;
|
||||
do o = 1; z = 2
|
||||
until (o = 2) then J
|
||||
state J
|
||||
do o = 2
|
||||
until (o = 1) then I
|
||||
end
|
||||
tel
|
||||
|
||||
node (++)(up, down: int) returns (o: int)
|
||||
var last cpt: int = 42;
|
||||
let
|
||||
o = last cpt;
|
||||
automaton
|
||||
state Init
|
||||
var k : int;
|
||||
do k = 0 -> pre k + 2;
|
||||
cpt = 0
|
||||
until
|
||||
(up = 1) then Up
|
||||
state Up
|
||||
do cpt = last cpt + 1
|
||||
until (down = 1) then Down
|
||||
| (down = 0) then Up
|
||||
state Down
|
||||
do cpt = (last cpt) + 1
|
||||
until (up = 1) then Up
|
||||
end;
|
||||
tel
|
||||
|
||||
node f(x: bool) returns (y: bool)
|
||||
var z: bool;
|
||||
let
|
||||
y = x or x & x;
|
||||
z = true -> if y then not (pre z) else pre z;
|
||||
tel
|
||||
|
||||
(*
|
||||
let increasing(x) returns (o)
|
||||
do true -> x >= pre(x) + 1 done
|
||||
|
||||
modes(v0) =
|
||||
last o = v0
|
||||
when up(x) returns (w)
|
||||
assume (x >= 0) ensure (w >= 0)
|
||||
do w = x + last o + 2; o = w + 4 done
|
||||
when down(x) returns (w)
|
||||
do w = x - last o + 2; o = w + 2 done
|
||||
end
|
||||
|
||||
val gain : int >
|
||||
modes last o : int when up: int -> int when down: int -> int
|
||||
end with { up # down }
|
||||
|
||||
let node gain(v0)(up, down) returns (o)
|
||||
assume (v0 >= 0) & (increasing up)
|
||||
guaranty (deacreasing o)
|
||||
last o = 0 in
|
||||
automaton
|
||||
state Await
|
||||
do
|
||||
unless down then Down(1) | up then Up(1)
|
||||
state Down(d)
|
||||
let rec cpt = 1 -> pre cpt + 1 in
|
||||
do o = last o - d
|
||||
until (cpt >= 5) then Down(d-5)
|
||||
until up then Up(1)
|
||||
state Up(d)
|
||||
let rec cpt = 1 -> pre cpt + 1 in
|
||||
do o = last o + d
|
||||
until (cpt >= 5) then Up(d+5)
|
||||
until down then Down(1)
|
||||
state Unreachable
|
||||
let rec c = 0 + 2 in
|
||||
var m in
|
||||
do o = m + 2; m = 3 + c done
|
||||
end
|
||||
|
||||
node g(x, y: int) returns (o: int)
|
||||
let
|
||||
o = x ++ y;
|
||||
tel
|
||||
|
||||
node dfby(x)(y) returns (o)
|
||||
let
|
||||
o = x fby (x fby y)
|
||||
tel
|
||||
|
||||
node f(x)(y) returns (o)
|
||||
var last o = x;
|
||||
let
|
||||
o = last o + y
|
||||
tel
|
||||
|
||||
val f : int > (int => int)
|
||||
|
||||
static x = e in ...
|
||||
|
||||
(if c then (fun x -> x + 2) else (fun k -> k + 3))(x+2)
|
||||
|
||||
let M(x1,..., xn) =
|
||||
let y1 = ... in ... let yk = ... in
|
||||
modes
|
||||
mem m1 = ...; mem ml = ...;
|
||||
step (...) returns (...) ...
|
||||
reset = ...
|
||||
end
|
||||
*) *)
|
130
tools/old_debugger_script
Normal file
130
tools/old_debugger_script
Normal file
|
@ -0,0 +1,130 @@
|
|||
load_printer "/sw/lib/ocaml/menhirLib/menhirLib.cmo"
|
||||
load_printer "/sw/lib/ocaml/str.cma"
|
||||
load_printer "_build/global/names.d.cmo"
|
||||
load_printer "_build/global/location.d.cmo"
|
||||
load_printer "_build/utilities/misc.d.cmo"
|
||||
load_printer "_build/global/types.d.cmo"
|
||||
load_printer "_build/global/signature.d.cmo"
|
||||
load_printer "_build/utilities/global/compiler_options.d.cmo"
|
||||
load_printer "_build/utilities/global/errors.d.cmo"
|
||||
load_printer "_build/utilities/global/compiler_utils.d.cmo"
|
||||
load_printer "_build/global/modules.d.cmo"
|
||||
load_printer "_build/global/initial.d.cmo"
|
||||
load_printer "_build/global/idents.d.cmo"
|
||||
load_printer "_build/global/clocks.d.cmo"
|
||||
load_printer "_build/utilities/pp_tools.d.cmo"
|
||||
load_printer "_build/global/global_printer.d.cmo"
|
||||
load_printer "_build/global/static.d.cmo"
|
||||
load_printer "_build/heptagon/heptagon.d.cmo"
|
||||
load_printer "_build/heptagon/analysis/initialization.d.cmo"
|
||||
load_printer "_build/global/global_mapfold.d.cmo"
|
||||
load_printer "_build/heptagon/hept_mapfold.d.cmo"
|
||||
load_printer "_build/heptagon/analysis/statefull.d.cmo"
|
||||
load_printer "_build/heptagon/analysis/typing.d.cmo"
|
||||
load_printer "_build/heptagon/hept_printer.d.cmo"
|
||||
load_printer "_build/heptagon/parsing/hept_parsetree.d.cmo"
|
||||
load_printer "_build/heptagon/parsing/hept_parser.d.cmo"
|
||||
load_printer "_build/heptagon/parsing/hept_lexer.d.cmo"
|
||||
load_printer "_build/heptagon/parsing/hept_scoping.d.cmo"
|
||||
load_printer "_build/heptagon/transformations/automata.d.cmo"
|
||||
load_printer "_build/heptagon/transformations/block.d.cmo"
|
||||
load_printer "_build/heptagon/transformations/completion.d.cmo"
|
||||
load_printer "_build/heptagon/transformations/reset.d.cmo"
|
||||
load_printer "_build/heptagon/transformations/every.d.cmo"
|
||||
load_printer "_build/heptagon/transformations/last.d.cmo"
|
||||
load_printer "_build/heptagon/transformations/present.d.cmo"
|
||||
load_printer "_build/heptagon/main/hept_compiler.d.cmo"
|
||||
load_printer "_build/heptagon/parsing/hept_parsetree_mapfold.d.cmo"
|
||||
load_printer "_build/heptagon/parsing/hept_static_scoping.d.cmo"
|
||||
load_printer "_build/minils/minils.d.cmo"
|
||||
load_printer "_build/minils/mls_mapfold.d.cmo"
|
||||
load_printer "_build/minils/mls_printer.d.cmo"
|
||||
load_printer "_build/utilities/graph.d.cmo"
|
||||
load_printer "_build/utilities/global/dep.d.cmo"
|
||||
load_printer "_build/minils/mls_utils.d.cmo"
|
||||
load_printer "_build/main/hept2mls.d.cmo"
|
||||
load_printer "_build/minils/transformations/itfusion.d.cmo"
|
||||
load_printer "_build/obc/obc.d.cmo"
|
||||
load_printer "_build/obc/control.d.cmo"
|
||||
load_printer "_build/obc/obc_mapfold.d.cmo"
|
||||
load_printer "_build/main/mls2obc.d.cmo"
|
||||
load_printer "_build/minils/transformations/callgraph.d.cmo"
|
||||
load_printer "_build/obc/c/c.d.cmo"
|
||||
load_printer "_build/obc/c/csubst.d.cmo"
|
||||
load_printer "_build/obc/obc_utils.d.cmo"
|
||||
load_printer "_build/obc/c/cgen.d.cmo"
|
||||
load_printer "_build/obc/c/cmain.d.cmo"
|
||||
load_printer "_build/obc/obc_printer.d.cmo"
|
||||
load_printer "_build/minils/main/mls2seq.d.cmo"
|
||||
load_printer "_build/minils/analysis/clocking.d.cmo"
|
||||
load_printer "_build/minils/transformations/normalize.d.cmo"
|
||||
load_printer "_build/minils/transformations/schedule.d.cmo"
|
||||
load_printer "_build/global/global_compare.d.cmo"
|
||||
load_printer "_build/minils/mls_compare.d.cmo"
|
||||
load_printer "_build/minils/transformations/checkpass.d.cmo"
|
||||
load_printer "_build/minils/transformations/introvars.d.cmo"
|
||||
load_printer "_build/minils/transformations/singletonvars.d.cmo"
|
||||
load_printer "_build/minils/transformations/tomato.d.cmo"
|
||||
load_printer "_build/minils/main/mls_compiler.d.cmo"
|
||||
load_printer "_build/main/heptc.d.cmo"
|
||||
|
||||
|
||||
install_printer Idents.IdentSet.fprint_t
|
||||
|
||||
install_printer Global_printer.print_ck
|
||||
install_printer Global_printer.print_clock
|
||||
install_printer Global_printer.print_field
|
||||
install_printer Global_printer.print_ident
|
||||
install_printer Global_printer.print_interface
|
||||
install_printer Global_printer.print_param
|
||||
install_printer Global_printer.print_qualname
|
||||
install_printer Global_printer.print_size_constraint
|
||||
install_printer Global_printer.print_static_exp
|
||||
install_printer Global_printer.print_static_exp_tuple
|
||||
install_printer Global_printer.print_struct
|
||||
install_printer Global_printer.print_type
|
||||
|
||||
|
||||
|
||||
install_printer Names.print_name
|
||||
|
||||
install_printer Hept_printer.print_iterator
|
||||
install_printer Hept_printer.print_pat
|
||||
install_printer Hept_printer.print_vd
|
||||
install_printer Hept_printer.print_exps
|
||||
install_printer Hept_printer.print_exp
|
||||
install_printer Hept_printer.print_app
|
||||
install_printer Hept_printer.print_eq
|
||||
install_printer Hept_printer.print_eq_list
|
||||
install_printer Hept_printer.print_state_handler_list
|
||||
install_printer Hept_printer.print_switch_handler_list
|
||||
install_printer Hept_printer.print_present_handler_list
|
||||
install_printer Hept_printer.print_inblock
|
||||
install_printer Hept_printer.print_type_def
|
||||
install_printer Hept_printer.print_const_dec
|
||||
install_printer Hept_printer.print_contract
|
||||
install_printer Hept_printer.print_node_params
|
||||
install_printer Hept_printer.print_node
|
||||
install_printer Hept_printer.print_open_module
|
||||
|
||||
|
||||
install_printer Mls_printer.print_pat
|
||||
install_printer Mls_printer.print_ck
|
||||
install_printer Mls_printer.print_vd
|
||||
install_printer Mls_printer.print_vd_tuple
|
||||
install_printer Mls_printer.print_local_vars
|
||||
install_printer Mls_printer.print_const_dec
|
||||
install_printer Mls_printer.print_params
|
||||
install_printer Mls_printer.print_node_params
|
||||
install_printer Mls_printer.print_exp_tuple
|
||||
install_printer Mls_printer.print_vd_tuple
|
||||
install_printer Mls_printer.print_index
|
||||
install_printer Mls_printer.print_dyn_index
|
||||
install_printer Mls_printer.print_every
|
||||
install_printer Mls_printer.print_exp_desc
|
||||
install_printer Mls_printer.print_eq
|
||||
install_printer Mls_printer.print_eqs
|
||||
install_printer Mls_printer.print_open_module
|
||||
install_printer Mls_printer.print_type_dec
|
||||
install_printer Mls_printer.print_contract
|
||||
install_printer Mls_printer.print_node
|
Loading…
Reference in a new issue