From 3e3d1d1234b6f29a33e7ca480b4b90fe4116f139 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 15 Dec 2009 12:26:00 -0500 Subject: Initial generalization of Especialize, with security bug known --- tests/espec.ur | 56 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ tests/espec.urp | 3 +++ tests/espec.urs | 1 + 3 files changed, 60 insertions(+) create mode 100644 tests/espec.ur create mode 100644 tests/espec.urp create mode 100644 tests/espec.urs (limited to 'tests') diff --git a/tests/espec.ur b/tests/espec.ur new file mode 100644 index 00000000..37b22a36 --- /dev/null +++ b/tests/espec.ur @@ -0,0 +1,56 @@ +fun foo (wrap : xbody -> transaction page) = wrap + Foo + + +fun bar (wrap : xbody -> transaction page) (n : int) = wrap + Bar; {[n]} + + +fun baz (n : int) (wrap : xbody -> transaction page) = wrap + Baz; {[n]} + + +fun middle (n : int) (wrap : xbody -> transaction page) (m : int) = wrap + Middle; {[n]}; {[m]} + + +fun crazy (f : int -> int) (b : bool) (wrap : xbody -> transaction page) (m : int) = wrap + Crazy; {[b]}; {[f m]} + + +fun wild (q : bool) (f : int -> int) (n : float) (wrap : xbody -> transaction page) (m : int) = wrap + Wild; {[n]}; {[f m]}; {[q]} + + +fun wrap x = return {x} + +fun wrapN n x = return {[n]}; {x} + +fun foo2 (wrap : xbody -> transaction page) = wrap + Foo + + +fun foo3 (n : int) = wrap + Foo + + +fun bar2 (n : int) (wrap : xbody -> transaction page) = wrap + Bar; n={[n]} + + +fun bar3 (n : int) = wrap + Bar + + + +fun main () = return + Foo + Bar + Baz + Middle + 2 * n) False wrap 2}>Crazy + 2 * n) 1.23 wrap 2}>Wild +

+ Foo3 + Bar3 + diff --git a/tests/espec.urp b/tests/espec.urp new file mode 100644 index 00000000..045fb1e0 --- /dev/null +++ b/tests/espec.urp @@ -0,0 +1,3 @@ +debug + +espec diff --git a/tests/espec.urs b/tests/espec.urs new file mode 100644 index 00000000..6ac44e0b --- /dev/null +++ b/tests/espec.urs @@ -0,0 +1 @@ +val main : unit -> transaction page -- cgit v1.2.3