Merge branch 'nik_include_pulse' of https://github.com/FStarLang/c2pulse into nik_include_pulse

Author: angelica-moreira

test/issue15_test.c

@@ -0,0 +1,6 @@
+#include "../include/PulseMacros.h"
+
+REQUIRES(emp)
+ENSURES(emp)
+void test_empty(void)
+{ return;  }

test/issue16_test.c

@@ -0,0 +1,19 @@
+#include "../include/PulseMacros.h"
+ERASED_ARG(#vr:erased _)
+REQUIRES(r |-> vr)
+REQUIRES(pure Pulse.Lib.C.Int32.(fits (+) (as_int vr) 1))
+ENSURES(exists* w. (r |-> w) ** pure Pulse.Lib.C.Int32.(as_int w == as_int vr + 1))
+int incr (int *r)
+{
+    *r = *r + 1;
+}
+
+REQUIRES(emp)
+RETURNS(i:Pulse.Lib.C.Int32.int32)
+ENSURES(pure Pulse.Lib.C.Int32.(as_int i == 1))
+int one()
+{
+    int i = 0;
+    incr(&i);
+    return i;
+}

test/issue18_test.c

@@ -0,0 +1,49 @@
+#include <stdint.h>
+#include <stdlib.h>
+#include "../include/PulseMacros.h"
+
+REQUIRES(emp)
+RETURNS(i:int32)
+ENSURES(emp)
+int test(void)
+{
+  return 0;
+}
+
+typedef struct _point {
+  int px;
+  int py;
+} point;
+
+
+INCLUDE (
+  let is_diag_point (p:ref point) (v:int32)
+  : slprop
+  = point_pred p {px=v; py=v}
+
+  let is_point (p:ref point) (xy : (int & int))
+  : slprop
+  = exists* v. point_pred p v ** pure (as_int v.px == fst xy) ** pure (as_int v.py == snd xy)
+
+  ghost
+  fn fold_is_point (p:ref point) (#s:point_spec)
+  requires point_pred p s
+  ensures exists* v. is_point p v ** pure (v == (as_int s.px, as_int s.py))
+  {
+    fold (is_point p (as_int s.px, as_int s.py));
+  }
+
+)
+
+ERASED_ARG(#v:erased _)
+REQUIRES(is_point p v)
+REQUIRES(pure <| fits (+) (fst v) (as_int dx))
+REQUIRES(pure <| fits (+) (snd v) (as_int dy))
+ENSURES(is_point p (fst v + as_int dx, snd v + as_int dy))
+void move(point *p, int dx, int dy)
+{
+  LEMMA(unfold(is_point); point_explode p);
+  p->px = p->px + dx;
+  p->py = p->py + dy;
+  LEMMA(point_recover p; fold_is_point p);
+}

test/issue1_test.c

@@ -0,0 +1,30 @@
+// RUN: %c2pulse %s
+// RUN: cat %p/Issue1_test.fst
+// RUN: diff %p/Issue1_test.fst %p/snapshots/Issue1_test.fst
+// RUN: %run_fstar.sh %p/Issue1_test.fst 2>&1 | %{FILECHECK} %s --check-prefix=PULSE
+
+#include <stdint.h>
+#include <stdlib.h>
+#include "../include/PulseMacros.h"
+
+REQUIRES("x |-> 'i")
+REQUIRES("pure FStar.Int32.(fits (v 'i + 1))")
+ENSURES("exists* j. (x |-> j) ** pure FStar.Int32.((v j <: int) == v 'i + 1)")
+void incr (int *x)
+{
+    *x = *x + 1;
+}
+
+ERASED_ARG(#i:_)
+ERASED_ARG(#j:_)
+REQUIRES(x |-> i)
+REQUIRES(y |-> j)
+REQUIRES(pure FStar.Int32.(fits (v i + 1)))
+ENSURES(exists* k. (x |-> k) ** pure FStar.Int32.(v i + 1 == v k))
+ENSURES(y |-> j)
+void incr_frame(int *x, int *y)
+{
+    incr(x);
+}
+
+// PULSE: All verification conditions discharged successfully

test/issue2_test.c

@@ -0,0 +1,11 @@
+#include "../include/PulseMacros.h"
+	
+ERASED_ARG(#w:_)
+REQUIRES(r |-> w)
+RETURNS(v:Int32.t)
+ENSURES(r |-> w)
+ENSURES(pure (v == w))
+int value_of_explicit(int *r)
+{
+    return *r;
+}

test/issue9_test.c

@@ -0,0 +1,9 @@
+// EXPECT_FAILURE(19)
+#include "../include/PulseMacros.h"
+RETURNS(s:_)
+ENSURES(s |-> 0)
+int* refs_are_scoped()
+{
+    int s = 0;
+    return &s;
+}