diff options
Diffstat (limited to 'Test')
-rw-r--r-- | Test/dafny0/Extern.dfy | 27 | ||||
-rw-r--r-- | Test/dafny0/Extern.dfy.expect | 4 | ||||
-rw-r--r-- | Test/dafny0/Extern2.cs | 14 | ||||
-rw-r--r-- | Test/dafny0/ExternHelloLibrary.cs | 15 | ||||
-rw-r--r-- | Test/dafny0/ExternHelloLibrary.dll | bin | 0 -> 3072 bytes | |||
-rw-r--r-- | Test/dafny0/ExternNegative.dfy | 26 | ||||
-rw-r--r-- | Test/dafny0/ExternNegative.dfy.expect | 3 | ||||
-rw-r--r-- | Test/dafny0/ExternNegative2.dfy | 26 |
8 files changed, 115 insertions, 0 deletions
diff --git a/Test/dafny0/Extern.dfy b/Test/dafny0/Extern.dfy new file mode 100644 index 00000000..cbdffe34 --- /dev/null +++ b/Test/dafny0/Extern.dfy @@ -0,0 +1,27 @@ +// RUN: %dafny /compile:1 /print:"%t.print" /dprint:"%t.dprint" "%s" "%S\Extern2.cs" "%S\ExternHelloLibrary.dll" > "%t"
+// RUN: %diff "%s.expect" "%t"
+extern "Modx" module Mod1
+{
+ extern "classx" class Class1
+ {
+ extern "Fun1x" static function method Fun1() : int
+ ensures Fun1() > 0
+ extern "Method1x" static method Method1() returns (x: int)
+ ensures x > 0
+ static function method Fun2() : int
+ ensures Fun2() > 0
+ {
+ Fun1()
+ }
+ static method Method2() returns (x: int)
+ ensures x > 0
+ {
+ x := Method1();
+ }
+ }
+ method Main()
+ {
+ var m2 := Class1.Method2();
+ print ("Fun2() = ", Class1.Fun2(), "Method2() = ", m2, "\n");
+ }
+}
diff --git a/Test/dafny0/Extern.dfy.expect b/Test/dafny0/Extern.dfy.expect new file mode 100644 index 00000000..fec087d9 --- /dev/null +++ b/Test/dafny0/Extern.dfy.expect @@ -0,0 +1,4 @@ + +Dafny program verifier finished with 7 verified, 0 errors +Compiled program written to D:\de\dafny\Test\dafny0\Extern.cs +Compiled assembly into Extern.exe diff --git a/Test/dafny0/Extern2.cs b/Test/dafny0/Extern2.cs new file mode 100644 index 00000000..2fcaf18b --- /dev/null +++ b/Test/dafny0/Extern2.cs @@ -0,0 +1,14 @@ +using System.Numerics; +namespace @Modx { + + public partial class @classx { + public static BigInteger @Fun1x() { + return BigInteger.One; + } + public static void @Method1x(out BigInteger @x) + { + ExternHelloLibrary.ExternHelloLibrary.SayHello(); + @x = BigInteger.One; + } + } +} diff --git a/Test/dafny0/ExternHelloLibrary.cs b/Test/dafny0/ExternHelloLibrary.cs new file mode 100644 index 00000000..81163997 --- /dev/null +++ b/Test/dafny0/ExternHelloLibrary.cs @@ -0,0 +1,15 @@ +// Note that ExternHelloLibrary.dll was produced from this file using +// csc /t:library ExternHelloLibrary.cs + +using System; + +namespace ExternHelloLibrary +{ + public static class ExternHelloLibrary + { + public static void SayHello() + { + Console.WriteLine("Hello from ExternHelloLibrary."); + } + } +} diff --git a/Test/dafny0/ExternHelloLibrary.dll b/Test/dafny0/ExternHelloLibrary.dll Binary files differnew file mode 100644 index 00000000..914e4248 --- /dev/null +++ b/Test/dafny0/ExternHelloLibrary.dll diff --git a/Test/dafny0/ExternNegative.dfy b/Test/dafny0/ExternNegative.dfy new file mode 100644 index 00000000..4ae73232 --- /dev/null +++ b/Test/dafny0/ExternNegative.dfy @@ -0,0 +1,26 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+extern "Modx" module Mod1
+{
+ extern "classx" class Class1
+ {
+ extern "Fun1x" static function method Fun1() : int
+ ensures Fun1() > 0
+ extern "Method1x" static method Method1() returns (x: int)
+ ensures x > 0
+ static abstract function method Fun2() : int
+ ensures Fun2() > 0
+ {
+ Fun1()
+ }
+ static static method Method2() returns (x: int)
+ ensures x > 0
+ {
+ x := Method1();
+ }
+ }
+}
+// Will give error about duplicate CompileName for module.
+extern "Modx" module Mod2
+{
+}
diff --git a/Test/dafny0/ExternNegative.dfy.expect b/Test/dafny0/ExternNegative.dfy.expect new file mode 100644 index 00000000..5d95ced7 --- /dev/null +++ b/Test/dafny0/ExternNegative.dfy.expect @@ -0,0 +1,3 @@ +ExternNegative.dfy(11,11): Error: Function methods cannot be declared 'abstract'. +ExternNegative.dfy(16,11): Error: Duplicate declaration modifier: static +2 parse errors detected in ExternNegative.dfy diff --git a/Test/dafny0/ExternNegative2.dfy b/Test/dafny0/ExternNegative2.dfy new file mode 100644 index 00000000..3d09913b --- /dev/null +++ b/Test/dafny0/ExternNegative2.dfy @@ -0,0 +1,26 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+extern "Modx" module Mod1
+{
+ extern "classx" class Class1
+ {
+ extern "Fun1x" static function method Fun1() : int
+ ensures Fun1() > 0
+ extern "Method1x" static method Method1() returns (x: int)
+ ensures x > 0
+ static function method Fun2() : int
+ ensures Fun2() > 0
+ {
+ Fun1()
+ }
+ static method Method2() returns (x: int)
+ ensures x > 0
+ {
+ x := Method1();
+ }
+ }
+}
+// Will give error about duplicate CompileName for module.
+extern "Modx" module Mod2
+{
+}
|