Code for #623

FStarLang · Aug 16, 2016 · 9b69565 · 9b69565
1 parent a8db6c4
commit 9b69565
Showing 1 changed file with 43 additions and 0 deletions.
diff --git a/examples/bug-reports/bug623.fst b/examples/bug-reports/bug623.fst
@@ -0,0 +1,43 @@
+module Test
+
+val null: unit -> All unit
+  (requires (fun h -> True))
+  (ensures  (fun h r h' -> True))
+let null () = ()
+
+(* Fails *)
+(* let test0 = assert(false); null () *)
+
+(* Succeeds *)
+let test1 () = assert(false); null ()
+
+(* Succeeds *)
+let test2 (u:unit) = assert(false); null ()
+
+(* Fails *)
+(* let test3 (u:unit) : All unit (requires (fun h -> True)) (ensures (fun h r h' -> True)) = assert(false); null() *)
+
+(* Succeeds *)
+let test3' () : All unit (requires (fun h -> True)) (ensures (fun h r h' -> True)) = assert(false); null()
+
+(* Succeeds *)
+let test4 (u:unit) : ML unit = assert(false); null()
+
+(* Fails *)
+(* let test5 (u:unit) : ML unit = assert(false) *)
+
+val null2: unit -> Div unit
+  (requires (True))
+  (ensures  (fun r -> True))
+let null2 () = ()
+
+(* Succeeds *)
+let test6 (u:unit) : ML unit = assert(false); null2()
+
+val null3: unit -> Pure unit
+  (requires (True))
+  (ensures  (fun r -> True))
+let null3 () = ()
+
+(* Fails *)
+(* let test7 (u:unit) : ML unit = assert(false); null3() *)