From 1697a133cababe66fef1fbf7a1ed9036255d8e68 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Tue, 30 Jun 2015 23:42:57 -0700
Subject: Fixed bugs in encoding of preconditions of function values, Issue
 #84.

---
 Test/hofs/Naked.dfy           | 10 +++---
 Test/hofs/Naked.dfy.expect    |  8 ++---
 Test/hofs/Requires.dfy        | 82 +++++++++++++++++++++++++++++++++++++++++++
 Test/hofs/Requires.dfy.expect |  5 +++
 Test/hofs/Simple.dfy.expect   |  5 +--
 5 files changed, 95 insertions(+), 15 deletions(-)
 create mode 100644 Test/hofs/Requires.dfy
 create mode 100644 Test/hofs/Requires.dfy.expect

(limited to 'Test/hofs')

diff --git a/Test/hofs/Naked.dfy b/Test/hofs/Naked.dfy
index fa99377f..d23eb507 100644
--- a/Test/hofs/Naked.dfy
+++ b/Test/hofs/Naked.dfy
@@ -19,17 +19,17 @@ module Functions {
 
 module Requires {
   function t(x: nat): nat
-  requires !t.requires(x);
+  requires !t.requires(x);  // error: use of naked function in its own SCC
   { x }
 
   function g(x: nat): nat
-  requires !(g).requires(x);
+  requires !(g).requires(x);  // error: use of naked function in its own SCC
   { x }
 
-  function g2(x: int): int { h(x) }
-
+  function D(x: int): int  // used so termination errors don't mask other errors
+  function g2(x: int): int decreases D(x) { h(x) }  // error: precondition violation
   function h(x: int): int
-    requires !g2.requires(x);
+    requires !g2.requires(x);  // error: use of naked function in its own SCC
   { x }
 }
 
diff --git a/Test/hofs/Naked.dfy.expect b/Test/hofs/Naked.dfy.expect
index b4dfc561..514952a1 100644
--- a/Test/hofs/Naked.dfy.expect
+++ b/Test/hofs/Naked.dfy.expect
@@ -21,11 +21,7 @@ Execution trace:
 Naked.dfy(26,14): Error: cannot use naked function in recursive setting. Possible solution: eta expansion.
 Execution trace:
     (0,0): anon0
-Naked.dfy(29,30): Error: cannot prove termination; try supplying a decreases clause
-Execution trace:
-    (0,0): anon0
-    (0,0): anon4_Else
-Naked.dfy(29,30): Error: possible violation of function precondition
+Naked.dfy(30,45): Error: possible violation of function precondition
 Naked.dfy(32,14): Related location
 Execution trace:
     (0,0): anon0
@@ -47,4 +43,4 @@ Naked.dfy(48,11): Error: cannot use naked function in recursive setting. Possibl
 Execution trace:
     (0,0): anon0
 
-Dafny program verifier finished with 1 verified, 12 errors
+Dafny program verifier finished with 2 verified, 11 errors
diff --git a/Test/hofs/Requires.dfy b/Test/hofs/Requires.dfy
new file mode 100644
index 00000000..68677b3e
--- /dev/null
+++ b/Test/hofs/Requires.dfy
@@ -0,0 +1,82 @@
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main()
+{
+  test0(10);
+	test5(11);
+	test6(12);
+	test1();
+	test2();
+}
+
+predicate valid(x:int) 
+{
+  x > 0
+}
+
+function ref1(y:int) : int
+  requires valid(y);
+{
+  y - 1
+}
+
+lemma assumption1()
+  ensures forall a, b :: valid(a) && valid(b) && ref1(a) == ref1(b) ==> a == b;
+{
+} 
+
+method test0(a: int)
+{
+  if ref1.requires(a) {
+    // the precondition should suffice to let us call the method
+    ghost var b := ref1(a);
+  }
+}
+method test5(a: int)
+{
+  if valid(a) {
+    // valid(a) is the precondition of ref1
+    assert ref1.requires(a);
+  }  
+} 
+method test6(a: int)
+{
+  if ref1.requires(a) {
+    // the precondition of ref1 is valid(a)
+    assert valid(a);
+  }  
+}
+
+method test1()
+{
+  if * {
+    assert forall a, b :: valid(a) && valid(b) && ref1(a) == ref1(b) ==> a == b;
+  } else {
+    assert forall a, b :: ref1.requires(a) && ref1.requires(b) && ref1(a) == ref1(b) 
+                          ==> a == b;
+  }
+}
+
+function {:opaque} ref2(y:int) : int        // Now with an opaque attribute
+  requires valid(y);
+{
+  y - 1
+}
+
+lemma assumption2()
+  ensures forall a, b :: valid(a) && valid(b) && ref2(a) == ref2(b) ==> a == b;
+{
+  reveal_ref2();
+}
+
+method test2()
+{
+  assumption2();
+  if * {
+    assert forall a, b :: valid(a) && valid(b) && ref2(a) == ref2(b) ==> a == b;
+  } else {
+    assert forall a, b :: ref2.requires(a) && ref2.requires(b) && ref2(a) == ref2(b) 
+                          ==> a == b;
+  }
+}
diff --git a/Test/hofs/Requires.dfy.expect b/Test/hofs/Requires.dfy.expect
new file mode 100644
index 00000000..b9a40d66
--- /dev/null
+++ b/Test/hofs/Requires.dfy.expect
@@ -0,0 +1,5 @@
+
+Dafny program verifier finished with 20 verified, 0 errors
+Program compiled successfully
+Running...
+
diff --git a/Test/hofs/Simple.dfy.expect b/Test/hofs/Simple.dfy.expect
index 1a1027ae..e2f16ef3 100644
--- a/Test/hofs/Simple.dfy.expect
+++ b/Test/hofs/Simple.dfy.expect
@@ -18,9 +18,6 @@ Execution trace:
     (0,0): anon3_Then
     (0,0): anon2
 Simple.dfy(61,10): Error: possible violation of function precondition
-Execution trace:
-    (0,0): anon0
-Simple.dfy(61,18): Error: assertion violation
 Execution trace:
     (0,0): anon0
 Simple.dfy(73,10): Error: assertion violation
@@ -29,4 +26,4 @@ Execution trace:
     Simple.dfy(72,38): anon5_Else
     Simple.dfy(73,38): anon6_Else
 
-Dafny program verifier finished with 14 verified, 7 errors
+Dafny program verifier finished with 14 verified, 6 errors
-- 
cgit v1.2.3