Merge pull request #574 from FStarLang/nik_testcase_for_extraction_with_interfaces

Test: Regression test for Pulse fn extraction with .fsti interface

Author: gebner

test/bug-reports/ExtractPulseFnIface.c.expected

@@ -0,0 +1,17 @@
+/* krml header omitted for test repeatability */
+
+
+#include "ExtractPulseFnIface.h"
+
+extern krml_checked_int_t Prims_op_Addition(krml_checked_int_t x, krml_checked_int_t y);
+
+krml_checked_int_t ExtractPulseFnIface_pure_add(krml_checked_int_t x, krml_checked_int_t y)
+{
+  return Prims_op_Addition(x, y);
+}
+
+krml_checked_int_t ExtractPulseFnIface_pulse_read_ref(krml_checked_int_t *r)
+{
+  return *r;
+}
+

test/bug-reports/ExtractPulseFnIface.fst

@@ -0,0 +1,19 @@
+module ExtractPulseFnIface
+#lang-pulse
+
+open Pulse.Lib.Pervasives
+open Pulse.Lib.Reference
+module R = Pulse.Lib.Reference
+
+let pure_add (x y : int) : int = x + y
+
+fn pulse_read_ref
+  (r: ref int)
+  (#v: Ghost.erased int)
+  requires R.pts_to r v
+  returns x: int
+  ensures R.pts_to r v ** pure (x == Ghost.reveal v)
+{
+  let x = !r;
+  x
+}

test/bug-reports/ExtractPulseFnIface.fsti

@@ -0,0 +1,21 @@
+module ExtractPulseFnIface
+#lang-pulse
+
+(** Interface for ExtractPulseFnIface.
+    Tests that a Pulse fn declared in .fsti extracts to C correctly.
+    Regression test: previously, fn declarations in .fsti were not
+    recognized by the interleaver, causing the implementation to be
+    tagged KrmlPrivate and silently dropped by KaRaMeL. *)
+
+open Pulse.Lib.Pervasives
+open Pulse.Lib.Reference
+module R = Pulse.Lib.Reference
+
+val pure_add (x y : int) : int
+
+fn pulse_read_ref
+  (r: ref int)
+  (#v: Ghost.erased int)
+  requires R.pts_to r v
+  returns x: int
+  ensures R.pts_to r v ** pure (x == Ghost.reveal v)