testcases for #1055 and #1818

examples/bug-reports/Bug1055.fst

@@ -0,0 +1,86 @@
+(*
+   Copyright 2008-2018 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+module Bug1055
+
+open FStar.ST
+open FStar.All
+
+(*
+ * F* now checks that top-level unannotated effectful functions have a trivial precondition
+ *)
+
+let test1_f (_:unit{false}) : ML unit = ()
+(*
+ * Fails since it has a non-trivial precondition (false)
+ *)
+[@expect_failure]
+let test1_g () = test1_f (); assert false
+
+(*
+ * But will succeed with an explicit annotation
+ *)
+let test1_g_with_spec ()
+  : All unit (fun _ -> False) (fun _ _ _ -> True)
+  = test1_f (); assert false
+
+
+type test2_filename = string
+let test2_canWrite (f:test2_filename) = false
+let test2_write (f:test2_filename{test2_canWrite f}) (s: string) : ML unit =
+  FStar.IO.print_string "A"
+
+[@expect_failure]
+let test2_dynamicChecking () =
+  test2_write "demo/password" "junk"
+
+[@expect_failure]
+let test2_dynamicChecking2 () =
+  assert False;
+  test2_write "demo/password" "junk"
+
+[@expect_failure]
+let test3_write (#a:Type) (r:ref a) = r := 42
+
+[@expect_failure]
+let test4_append_to2 (#a:Type) (xs:list a) = ignore(alloc 5); 2 :: xs
+
+
+(*
+ * This works because it has a trivial precondition,
+ *   In addition, its postcondition is available to the callers, see test5_client below
+ *)
+let test5_write (r:ref int) = r := 42
+
+let test5_client (r:ref int) =
+  test5_write r;
+  let h = ST.get () in
+  assert (Heap.sel h r == 42)
+
+(*
+ * Partial applications or just renaming works as expected
+ *)
+let test6_f (x:ref int) (y:int)
+  : ST unit
+    (requires fun h -> Heap.sel h x == y)
+    (ensures fun _ _ _ -> True)
+  = ()
+
+let test6_g = test6_f  //the inferred type of test6_g is same as test6_f
+
+let test6_h (x:ref int) = test6_f x  //the inferred type of test6_h is also as expected (application of x to test6_f)
+
+[@expect_failure]
+let test6_i (x:ref int) (y:int) = test6_f x y  //this fails since non-trivial precondition

examples/bug-reports/Bug1818.fst

@@ -0,0 +1,8 @@
+module Bug1818
+
+let test_t () = x:int -> Pure unit (requires x > 0) (ensures fun _ -> True)
+
+assume val bar (x:int) : Pure unit (requires x > 0) (ensures fun _ -> True)
+
+let foo () : (test_t ()) =
+  fun x -> bar x

examples/bug-reports/Makefile

@@ -35,7 +35,7 @@ SHOULD_VERIFY_CLOSED=bug022.fst bug024.fst bug025.fst bug026.fst bug026b.fst bug
   bug1561a.fst bug1561b.fst bug1065a.fst bug1065b.fst bug1065c.fst bug1568.fst Bug1571.fst Bug1572.fst Bug1592.fst \
   Bug1595.fst Bug1601.fst Bug1602.fst Bug1604.fst Bug1605.fst Bug1621.fst Bug1680.fst Bug1682.fst Bug1694.fst \
   Bug1730b.fst Bug1612.fst Bug1614a.fst Bug1614b.fst Bug1614c.fst Bug1614d.fst Bug1614e.fst Bug1750.fst Bug1750.Aux.fst \
-  Bug1622.fst bug1540.fst Bug1784.fst Bug1802.fst
+  Bug1622.fst bug1540.fst Bug1784.fst Bug1802.fst Bug1055.fst Bug1818.fst
 
 SHOULD_VERIFY_INTERFACE_CLOSED=bug771.fsti bug771b.fsti
 SHOULD_VERIFY_AND_WARN_CLOSED=bug016.fst
@@ -48,7 +48,7 @@ SHOULD_VERIFY_OPEN=bug045.fst bug057.fst bug064.fst bug065.fst bug071.fst bug121
   bug171b.fst bug171c.fst bug258.fst bug259.fst bug282.fst bug291.fst bug419.fst bug442.fst\
   bug442b.fst bug484.fst bug542.fst bug543.fst bug554.fst bug604.fst bug606.fst\
   bug626.fst bug682.fst bug715.fst bug739.fst bug815.fst bug815b.fst bug851.fst bug933.fst bug933b.fst\
-  bug1038.fst bug1055b.fst bug1091.fst bug1390.fst bug807d.fst bug1486.fst bug1392.fst
+  bug1038.fst bug1091.fst bug1390.fst bug807d.fst bug1486.fst bug1392.fst
 
 # These examples go through but their corresponding GitHub issue is still open. Consider closing and adding them
 # to SHOULD_VERIFY_CLOSED.