Add VeriFast kernel queue proofs (#117)

FreeRTOS/Test/VeriFast/include/proof/common.gh

@@ -0,0 +1,539 @@
+/*
+ * FreeRTOS VeriFast Proofs
+ * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+#ifndef COMMON_H
+#define COMMON_H
+
+#include <listex.gh>
+
+fixpoint list<t> rotate_left<t>(int n, list<t> xs) {
+  return append(drop(n, xs), take(n, xs));
+}
+
+fixpoint list<t> singleton<t>(t x) {
+  return cons(x, nil);
+}
+
+lemma void note(bool b)
+  requires b;
+  ensures b;
+{}
+
+lemma_auto void rotate_length<t>(int n, list<t> xs)
+  requires 0 <= n && n <= length(xs);
+  ensures length(rotate_left(n, xs)) == length(xs);
+{}
+
+lemma void take_length_eq<t>(int k, list<t> xs, list<t> ys)
+  requires 0 <= k && k <= length(xs) && take(k, xs) == ys;
+  ensures length(ys) == k;
+{}
+
+lemma void leq_bound(int x, int b)
+  requires b <= x && x <= b;
+  ensures x == b;
+{}
+
+lemma void mul_mono_l_strict(int x, int y, int n)
+    requires 0 < n &*& x < y;
+    ensures x * n < y * n;
+{
+    for (int i = 1; i < n; i++)
+        invariant i <= n &*& x * i < y * i;
+        decreases n - i;
+    {}
+}
+
+lemma void div_leq(int x, int y, int n)
+  requires 0 < n && x * n <= y * n;
+  ensures x <= y;
+{
+  assert x * n <= y * n;
+  if (x <= y) {
+    mul_mono_l(x,y,n);
+  } else {
+    mul_mono_l_strict(y,x,n); //< contradiction
+  }
+}
+
+lemma void div_lt(int x, int y, int n)
+  requires 0 < n && x * n < y * n;
+  ensures x < y;
+{
+  assert x * n <= y * n;
+  if (x == y) {
+  } else if (x <= y) {
+    mul_mono_l(x,y,n);
+  } else {
+    assert y < x;
+    mul_mono_l(y,x,n); //< contradiction
+  }
+}
+
+lemma_auto void mod_same(int n)
+  requires 0 < n;
+  ensures n % n == 0;
+{
+  div_rem_nonneg(n, n);
+  if (n / n < 1) {} else if (n / n > 1) {
+    mul_mono_l(2, n/n, n);
+  } else {}
+}
+
+lemma void mod_lt(int x, int n)
+  requires 0 <= x && x < n;
+  ensures x % n == x;
+{
+  div_rem_nonneg(x, n);
+  if (x / n > 0) {
+    mul_mono_l(1, x / n, n);
+  } else {
+  }
+}
+
+lemma void mod_plus_one(int x, int y, int n)
+  requires 0 <= y && 0 < n && x == (y % n);
+  ensures ((x+1) % n) == ((y+1) % n);
+{
+  div_rem_nonneg(y, n);
+  div_rem_nonneg(y+1, n);
+  div_rem_nonneg(y%n+1, n);
+  if (y%n+1 < n) {
+    mod_lt(y%n+1, n);
+    assert y%n == y - y/n*n;
+    assert (y+1)%n == y + 1 - (y + 1)/n*n;
+    if ((y+1)/n > y/n) {
+      mul_mono_l(y/n + 1, (y+1)/n, n);
+    } else if ((y+1)/n < y/n) {
+      mul_mono_l((y+1)/n + 1, y/n, n);
+    }
+    assert y - (y+1)/n*n == y - y/n*n;
+    assert y+1 - (y+1)/n*n == y - y/n*n + 1;
+    assert (y+1)%n == y%n + 1;
+  } else {
+    assert y%n+1 == n;
+    assert (y%n+1)%n == 0;
+    if (y/n + 1 < (y+1)/n) {
+      mul_mono_l(y/n + 2, (y+1)/n, n);
+    } else if (y/n + 1 > (y+1)/n) {
+      mul_mono_l((y+1)/n, y/n, n);
+    }
+    assert (y+1)/n == y/n + 1;
+    note((y+1)/n*n == (y/n + 1)*n);
+    assert (y+1)%n == 0;
+  }
+  assert (y%n+1)%n == (y+1)%n;
+}
+
+lemma void mod_mul(int x, int n, int y)
+  requires 0 < n && 0 <= x && 0 <= y;
+  ensures (x*n + y)%n == y%n;
+{
+  mul_mono_l(0, x, n);
+  div_rem_nonneg(x*n+y, n);
+  div_rem_nonneg(y, n);
+
+  if ((x*n+y)/n > x + y/n) {
+    mul_mono_l(x + y/n + 1, (x*n+y)/n, n);
+  } else if ((x*n+y)/n < x + y/n) {
+    mul_mono_l((x*n+y)/n + 1, x + y/n, n);
+  }
+  note((x*n + y)/n == x + y/n);
+  note((x*n + y)/n*n == (x + y/n)*n);
+}
+
+lemma void mod_plus_distr(int x, int y, int n)
+  requires 0 < n && 0 <= x && 0 <= y;
+  ensures ((x % n) + y) % n == (x + y) % n;
+{
+  div_rem_nonneg(x, n);
+  div_rem_nonneg(x%n+y, n);
+  div_rem_nonneg(x+y, n);
+
+  assert x == x/n*n + x%n;
+  mod_mul(x/n, n, x%n + y);
+}
+
+lemma_auto void mod_mod(int x, int n)
+  requires 0 < n && 0 <= x;
+  ensures (x % n) % n == (x % n);
+{
+  mod_plus_distr(x, 0, n);
+}
+
+lemma void mod_plus(int x, int y, int n);
+  requires 0 < n && 0 <= x && 0 <= y;
+  ensures (x + y) % n == ((x % n) + (y % n)) % n;
+
+lemma_auto void mod_range(int x, int n)
+  requires 0 <= x && 0 < n;
+  ensures 0 <= (x % n) && (x % n) < n;
+{
+  div_rem_nonneg(x, n);
+}
+
+lemma void drop_update_le<t>(int i, int j, t x, list<t> xs)
+  requires 0 <= i && i <= j && j < length(xs);
+  ensures drop(i, update(j, x, xs)) == update(j - i, x, drop(i, xs));
+{
+  switch (xs) {
+  case nil:
+  case cons(x0, xs0):
+    if (i == 0) {
+    } else {
+      drop_update_le(i - 1, j - 1, x, xs0);
+    }
+  }
+}
+
+lemma void drop_update_ge<t>(int i, int j, t x, list<t> xs)
+  requires 0 <= j && j < i && i < length(xs);
+  ensures drop(i, update(j, x, xs)) == drop(i, xs);
+{
+  switch (xs) {
+  case nil:
+  case cons(x0, xs0):
+    if (j == 0) {
+    } else {
+      drop_update_ge(i - 1, j - 1, x, xs0);
+    }
+  }
+}
+
+lemma void take_update_le<t>(int i, int j, t x, list<t> xs)
+  requires 0 <= i && i <= j;
+  ensures take(i, update(j, x, xs)) == take(i, xs);
+{
+  switch (xs) {
+  case nil:
+  case cons(x0, xs0):
+    if (i == 0) {
+    } else {
+      take_update_le(i - 1, j - 1, x, xs0);
+    }
+  }
+}
+
+lemma void take_update_ge<t>(int i, int j, t x, list<t> xs)
+  requires 0 <= j && j < i && i <= length(xs);
+  ensures take(i, update(j, x, xs)) == update(j, x, take(i, xs));
+{
+  switch (xs) {
+  case nil:
+  case cons(x0, xs0):
+    if (j == 0) {
+    } else {
+      take_update_ge(i - 1, j - 1, x, xs0);
+    }
+  }
+}
+
+lemma void update_eq_append<t>(int i, t x, list<t> xs)
+  requires 0 <= i && i < length(xs);
+  ensures update(i, x, xs) == append(take(i, xs), cons(x, drop(i + 1, xs)));
+{
+  switch (xs) {
+  case nil:
+  case cons(x0, xs0):
+    if (i == 0) {
+    } else {
+      update_eq_append(i - 1, x, xs0);
+    }
+  }
+}
+
+lemma void take_append_ge<t>(int n, list<t> xs, list<t> ys)
+  requires length(xs) <= n;
+  ensures take(n, append(xs, ys)) == append(xs, take(n - length(xs), ys));
+{
+  switch (xs) {
+  case nil:
+  case cons(x0, xs0):
+    take_append_ge(n - 1, xs0, ys);
+  }
+}
+
+lemma void drop_drop<t>(int m, int n, list<t> xs)
+  requires 0 <= m && 0 <= n;
+  ensures drop(m, drop(n, xs)) == drop(m+n, xs);
+{
+  switch (xs) {
+  case nil:
+  case cons(x0, xs0):
+    if (n == 0) {} else {
+      drop_drop(m, n-1, xs0);
+    }
+  }
+}
+
+lemma void take_take<t>(int m, int n, list<t> xs)
+  requires 0 <= m && m <= n && n <= length(xs);
+  ensures take(m, take(n, xs)) == take(m, xs);
+{
+  switch (xs) {
+  case nil:
+  case cons(x0, xs0):
+    if (m == 0) {} else {
+      take_take(m - 1, n - 1, xs0);
+    }
+  }
+}
+
+lemma void index_of_distinct<t>(list<t> xs, t x1, t x2)
+  requires mem(x1, xs) == true &*& mem(x2, xs) == true &*& x1 != x2;
+  ensures index_of(x1, xs) != index_of(x2, xs);
+{
+  switch (xs) {
+  case nil:
+  case cons(h, tl):
+    if (h == x1 || h == x2) {
+      /* trivial */
+    } else {
+      index_of_distinct(tl, x1, x2);
+    }
+  }
+}
+
+lemma void remove_remove_nth<t>(list<t> xs, t x)
+  requires mem(x, xs) == true;
+  ensures remove(x, xs) == remove_nth(index_of(x, xs), xs);
+{
+  switch (xs) {
+  case nil:
+  case cons(h, tl):
+    if (x == h) {
+      assert index_of(x, xs) == 0;
+    } else {
+      remove_remove_nth(tl, x);
+    }
+  }
+}
+
+lemma void enq_lemma<t>(int k, int i, list<t> xs, list<t> ys, t z)
+  requires 0 <= k && 0 <= i && 0 < length(xs) && k < length(xs) && i < length(xs) && take(k, rotate_left(i, xs)) == ys;
+  ensures take(k+1, rotate_left(i, update((i+k)%length(xs), z, xs))) == append(ys, cons(z, nil));
+{
+  int j = (i+k)%length(xs);
+  assert take(k, append(drop(i, xs), take(i, xs))) == ys;
+  if (i + k < length(xs)) {
+    mod_lt(i + k, length(xs));
+    assert j == i + k;
+    drop_update_le(i, i + k, z, xs);
+    assert drop(i, update(i + k, z, xs)) == update(k, z, drop(i, xs));
+    take_update_le(i, i + k, z, xs);
+    assert take(i, update(i + k, z, xs)) == take(i, xs);
+    take_append(k+1, update(k, z, drop(i, xs)), take(i, xs));
+    assert take(k+1, append(update(k, z, drop(i, xs)), take(i, xs))) == take(k+1, update(k, z, drop(i, xs)));
+    update_eq_append(k, z, drop(i, xs));
+    assert update(k, z, drop(i, xs)) == append(take(k, drop(i, xs)), cons(z, drop(k + 1, drop(i, xs))));
+    take_append_ge(k+1, take(k, drop(i, xs)), cons(z, drop(k + 1, drop(i, xs))));
+    assert take(k+1, append(take(k, drop(i, xs)), cons(z, drop(k + 1, drop(i, xs))))) ==
+           append(take(k, drop(i, xs)), {z});
+    take_append(k, drop(i, xs), take(i, xs));
+    assert take(k+1, append(take(k, drop(i, xs)), cons(z, drop(k + 1, drop(i, xs))))) ==
+           append(take(k, append(drop(i, xs), take(i, xs))), {z});
+    assert take(k+1, update(k, z, drop(i, xs))) ==
+           append(take(k, append(drop(i, xs), take(i, xs))), {z});
+    assert take(k+1, append(update(k, z, drop(i, xs)), take(i, xs))) ==
+           append(take(k, append(drop(i, xs), take(i, xs))), {z});
+    assert take(k+1, append(drop(i, update(i + k, z, xs)), take(i, update(i + k, z, xs)))) ==
+           append(take(k, append(drop(i, xs), take(i, xs))), {z});
+
+  } else {
+    assert i + k < 2 * length(xs);
+    div_rem_nonneg(i + k, length(xs));
+    if ((i + k) / length(xs) > 1) {
+      mul_mono_l(2, (i + k) / length(xs), length(xs));
+    } else if ((i + k) / length(xs) < 1) {
+      mul_mono_l((i + k) / length(xs), 0, length(xs));
+    }
+    assert j == i + k - length(xs);
+    assert j < i;
+    drop_update_ge(i, j, z, xs);
+    assert drop(i, update(j, z, xs)) == drop(i, xs);
+    take_update_ge(i, j, z, xs);
+    assert update(j, z, take(i, xs)) == take(i, update(j, z, xs));
+    take_append_ge(k+1, drop(i, xs), take(i, update(j, z, xs)));
+    assert take(k+1, append(drop(i, update(j, z, xs)), take(i, update(j, z, xs)))) ==
+           append(drop(i, xs), take(j+1, update(j, z, take(i, xs))));
+    update_eq_append(j, z, take(i, xs));
+    assert update(j, z, take(i, xs)) == append(take(j, take(i, xs)), cons(z, drop(j + 1, take(i, xs))));
+    take_take(j, i, xs);
+    assert update(j, z, take(i, xs)) == append(take(j, xs), cons(z, drop(j+1, take(i, xs))));
+    take_append_ge(j+1, take(j, xs), cons(z, drop(j+1, take(i, xs))));
+    assert append(drop(i, xs), take(j+1, update(j, z, take(i, xs)))) ==
+           append(drop(i, xs), append(take(j, xs), {z}));
+    take_append_ge(k, drop(i, xs), take(i, xs));
+    append_assoc(drop(i, xs), take(j, xs), {z});
+    assert append(drop(i, xs), append(take(j, xs), {z})) ==
+           append(take(k, append(drop(i, xs), take(i, xs))), {z});
+    assert append(drop(i, xs), take(j+1, update(j, z, take(i, xs)))) ==
+           append(take(k, append(drop(i, xs), take(i, xs))), {z});
+  }
+  assert take(k+1, append(drop(i, update(j, z, xs)), take(i, update(j, z, xs)))) ==
+         append(take(k, append(drop(i, xs), take(i, xs))), {z});
+  assert take(k+1, append(drop(i, update(j, z, xs)), take(i, update(j, z, xs)))) == append(ys, {z});
+}
+
+lemma void front_enq_lemma<t>(int k, int i, list<t> xs, list<t> ys, t z)
+  requires 0 < length(xs) && 0 <= k && k < length(xs) && 0 <= i && i < length(xs) && take(k, rotate_left((i+1)%length(xs), xs)) == ys;
+  ensures take(k+1, rotate_left(i, update(i, z, xs))) == cons(z, ys);
+{
+  int n = length(xs);
+  if (i+1 < n) {
+    mod_lt(i+1, n);
+    assert i < n;
+    assert take(k+1, rotate_left(i, update(i, z, xs))) ==
+           take(k+1, append(drop(i, update(i, z, xs)), take(i, update(i, z, xs))));
+    drop_update_le(i, i, z, xs);
+    take_update_le(i, i, z, xs);
+    assert take(k+1, append(drop(i, update(i, z, xs)), take(i, update(i, z, xs)))) ==
+           take(k+1, append(update(0, z, drop(i, xs)), take(i, xs)));
+    update_eq_append(0, z, drop(i, xs));
+    assert update(0, z, drop(i, xs)) == cons(z, drop(1, drop(i, xs)));
+    drop_drop(1, i, xs);
+    assert take(k+1, append(update(0, z, drop(i, xs)), take(i, xs))) ==
+           take(k+1, append(cons(z, drop(i+1, xs)), take(i, xs)));
+    assert take(k+1, append(cons(z, drop(i+1, xs)), take(i, xs))) ==
+           cons(z, take(k, append(drop(i+1, xs), take(i, xs))));
+
+    assert ys == take(k, rotate_left(i+1, xs));
+    assert ys == take(k, append(drop(i+1, xs), take(i+1, xs)));
+    if (k <= length(drop(i+1, xs))) {
+      take_append(k, drop(i+1, xs), take(i+1, xs));
+      take_append(k, drop(i+1, xs), take(i, xs));
+    } else {
+      take_append_ge(k, drop(i+1, xs), take(i+1, xs));
+      take_append_ge(k, drop(i+1, xs), take(i, xs));
+
+      assert (i+1) + k < 2 * n;
+      div_rem_nonneg((i+1) + k, n);
+      if (((i+1) + k) / n > 1) {
+        mul_mono_l(2, ((i+1) + k) / n, n);
+      } else if (((i+1) + k) / n < 1) {
+        mul_mono_l(((i+1) + k) / n, 0, n);
+      }
+      int j = ((i+1)+k)%n;
+      assert j <= i;
+      int l = length(drop(i+1, xs));
+      assert l == n - i - 1;
+      take_take(k - l, i + 1, xs);
+      take_take(k - l, i, xs);
+    }
+  } else {
+    assert i == (n-1);
+    assert (i + 1) % n == 0;
+    drop_update_le(i, i, z, xs);
+    update_eq_append(0, z, xs);
+    assert take(k+1, rotate_left(i, update(i, z, xs))) ==
+           take(k+1, append(drop(i, update(i, z, xs)), take(i, update(i, z, xs))));
+    drop_update_le(i, i, z, xs);
+    assert take(k+1, rotate_left(i, update(i, z, xs))) ==
+           take(k+1, append(update(0, z, drop(i, xs)), take(i, update(i, z, xs))));
+    update_eq_append(0, z, drop(i, xs));
+    assert take(k+1, rotate_left(i, update(i, z, xs))) ==
+           take(k+1, append(cons(z, drop(1, drop(i, xs))), take(i, update(i, z, xs))));
+    drop_drop(1, i, xs);
+    assert take(k+1, rotate_left(i, update(i, z, xs))) ==
+           take(k+1, append(cons(z, nil), take(i, update(i, z, xs))));
+    take_update_le(i, i, z, xs);
+    assert take(k+1, rotate_left(i, update(i, z, xs))) ==
+           cons(z, take(k, take(i, xs)));
+    take_take(k, i, xs);
+    assert take(k+1, rotate_left(i, update(i, z, xs))) == cons(z, ys);
+  }
+}
+
+lemma void deq_lemma<t>(int k, int i, list<t> xs, list<t> ys, t z)
+  requires 0 < k && k <= length(xs) && 0 <= i && i < length(xs) && take(k, rotate_left(i, xs)) == ys && z == head(ys);
+  ensures take(k-1, rotate_left((i+1)%length(xs), xs)) == tail(ys);
+{
+  int j = (i+1)%length(xs);
+  drop_n_plus_one(i, xs);
+  assert tail(take(k, append(drop(i, xs), take(i, xs)))) == take(k-1, append(drop(i+1, xs), take(i, xs)));
+  if (i+1 < length(xs)) {
+    mod_lt(i+1, length(xs));
+    assert j == i+1;
+    if (k-1 <= length(xs)-j) {
+      take_append(k-1, drop(j, xs), take(j, xs));
+      take_append(k-1, drop(j, xs), take(i, xs));
+    } else {
+      assert k+i > length(xs);
+      take_append_ge(k-1, drop(j, xs), take(j, xs));
+      take_append_ge(k-1, drop(j, xs), take(i, xs));
+      assert k-1-(length(xs)-j) == k+i-length(xs);
+      assert k+i-length(xs) <= i;
+      take_take(k+i-length(xs), j, xs);
+      take_take(k+i-length(xs), i, xs);
+      assert take(k+i-length(xs), take(j, xs)) == take(k+i-length(xs), take(i, xs));
+    }
+  } else {
+    assert i+1 == length(xs);
+    assert (i+1)%length(xs) == 0;
+    assert j == 0;
+    assert append(drop(j, xs), take(j, xs)) == xs;
+    assert append(drop(i+1, xs), take(i, xs)) == take(i, xs);
+    take_append_ge(k-1, drop(i+1, xs), take(i, xs));
+    take_take(k-1, i, xs);
+  }
+  assert take(k-1, append(drop(j, xs), take(j, xs))) == take(k-1, append(drop(i+1, xs), take(i, xs)));
+  assert take(k-1, append(drop(j, xs), take(j, xs))) == tail(take(k, append(drop(i, xs), take(i, xs))));
+}
+
+lemma void deq_value_lemma<t>(int k, int i, list<t> xs, list<t> ys)
+  requires 0 < k && k <= length(ys) && 0 <= i && i < length(xs) && take(k, rotate_left(i, xs)) == ys;
+  ensures nth(i, xs) == head(ys);
+{
+  drop_n_plus_one(i, xs);
+  assert nth(i, xs) == head(take(k, append(drop(i, xs), take(i, xs))));
+}
+
+lemma void combine_list_no_change<t>(list<t>prefix, t x, list<t>suffix, int i, list<t> xs)
+  requires 0 <= i && i < length(xs) && prefix == take(i, xs) && x == nth(i, xs) && suffix == drop(i+1, xs);
+  ensures xs == append(prefix, cons(x, suffix));
+{
+  drop_n_plus_one(i, xs);
+}
+
+/* Following lemma from `verifast/examples/vstte2010/problem4.java`. */
+lemma void update_rewrite<t>(list<t> vs, t v, int pos)
+  requires 0 <= pos && pos < length(vs);
+  ensures update(pos, v, vs) == append(take(pos, vs), cons(v, (drop(pos+1, vs))));
+{
+  switch(vs) {
+    case nil:
+    case cons(h, t):
+      if(pos == 0) {
+      } else {
+        update_rewrite(t, v, pos - 1);
+      }
+  }
+}
+
+lemma void combine_list_update<t>(list<t>prefix, t x, list<t>suffix, int i, list<t> xs)
+  requires 0 <= i && i < length(xs) && prefix == take(i, xs) && suffix == drop(i+1, xs);
+  ensures update(i, x, xs) == append(prefix, cons(x, suffix));
+{
+  update_rewrite(xs, x, i);
+}
+
+#endif /* COMMON_H */

FreeRTOS/Test/VeriFast/include/proof/queue.h

@@ -0,0 +1,435 @@
+/*
+ * FreeRTOS VeriFast Proofs
+ * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+#ifndef QUEUE_H
+#define QUEUE_H
+
+#define VERIFAST
+#include <stdlib.h>
+#include <stdint.h>
+#include <string.h>
+#include <threading.h>
+/*@#include "common.gh"@*/
+
+typedef size_t TickType_t;
+typedef size_t UBaseType_t;
+typedef ssize_t BaseType_t;
+
+/* Empty/no-op macros */
+/* Tracing */
+#define traceBLOCKING_ON_QUEUE_PEEK(x)
+#define traceBLOCKING_ON_QUEUE_RECEIVE(x)
+#define traceBLOCKING_ON_QUEUE_SEND(x)
+#define traceQUEUE_CREATE(x)
+#define traceQUEUE_CREATE_FAILED(x)
+#define traceQUEUE_DELETE(x)
+#define traceQUEUE_PEEK(x)
+#define traceQUEUE_PEEK_FAILED(x)
+#define traceQUEUE_PEEK_FROM_ISR(x)
+#define traceQUEUE_PEEK_FROM_ISR_FAILED(x)
+#define traceQUEUE_RECEIVE(x)
+#define traceQUEUE_RECEIVE_FAILED(x)
+#define traceQUEUE_RECEIVE_FROM_ISR(x)
+#define traceQUEUE_RECEIVE_FROM_ISR_FAILED(x)
+#define traceQUEUE_SEND(x)
+#define traceQUEUE_SEND_FAILED(x)
+#define traceQUEUE_SEND_FROM_ISR(x)
+#define traceQUEUE_SEND_FROM_ISR_FAILED(x)
+/* Coverage */
+#define mtCOVERAGE_TEST_MARKER()
+/* Asserts */
+#define configASSERT(x)
+#define portASSERT_IF_INTERRUPT_PRIORITY_INVALID()
+
+/* Map portable memory management functions */
+#define pvPortMalloc malloc
+#define vPortFree free
+
+#define queueSEND_TO_BACK	0
+#define queueSEND_TO_FRONT	1
+#define queueOVERWRITE		2
+
+#define pdTRUE	1
+#define pdFALSE	0
+
+#define pdPASS pdTRUE
+#define pdFAIL pdFALSE
+#define errQUEUE_FULL	0
+#define errQUEUE_EMPTY	0
+
+#define queueUNLOCKED					( ( int8_t ) -1 )
+#define queueLOCKED_UNMODIFIED			( ( int8_t ) 0 )
+#define queueINT8_MAX					( ( int8_t ) 127 )
+
+typedef struct QueuePointers
+{
+	int8_t *pcTail;					/*< Points to the byte at the end of the queue storage area.  Once more byte is allocated than necessary to store the queue items, this is used as a marker. */
+	int8_t *pcReadFrom;				/*< Points to the last place that a queued item was read from when the structure is used as a queue. */
+} QueuePointers_t;
+
+typedef struct SemaphoreData
+{
+#ifdef VERIFAST /*< do not model xMutexHolder */
+	void *xMutexHolder;
+#else
+	TaskHandle_t xMutexHolder;		 /*< The handle of the task that holds the mutex. */
+#endif
+	UBaseType_t uxRecursiveCallCount;/*< Maintains a count of the number of times a recursive mutex has been recursively 'taken' when the structure is used as a mutex. */
+} SemaphoreData_t;
+
+/* VeriFast does not support unions so we replace with a struct */
+struct fake_union_t {
+	QueuePointers_t xQueue;
+	SemaphoreData_t xSemaphore;
+};
+
+typedef struct xLIST {
+	UBaseType_t uxNumberOfItems;
+#ifndef VERIFAST /*< do not model pxIndex and xListEnd of xLIST struct */
+	struct xLIST_ITEM *pxIndex;
+	MiniListItem_t xListEnd;
+#endif
+} List_t;
+
+typedef struct QueueDefinition 		/* The old naming convention is used to prevent breaking kernel aware debuggers. */ {
+	int8_t *pcHead;					/*< Points to the beginning of the queue storage area. */
+	int8_t *pcWriteTo;				/*< Points to the free next place in the storage area. */
+
+#ifdef VERIFAST /*< VeriFast does not model unions */
+	struct fake_union_t u;
+#else
+	union
+	{
+		QueuePointers_t xQueue;		/*< Data required exclusively when this structure is used as a queue. */
+		SemaphoreData_t xSemaphore; /*< Data required exclusively when this structure is used as a semaphore. */
+	} u;
+#endif
+
+	List_t xTasksWaitingToSend;		/*< List of tasks that are blocked waiting to post onto this queue.  Stored in priority order. */
+	List_t xTasksWaitingToReceive;	/*< List of tasks that are blocked waiting to read from this queue.  Stored in priority order. */
+
+	volatile UBaseType_t uxMessagesWaiting;/*< The number of items currently in the queue. */
+	UBaseType_t uxLength;			/*< The length of the queue defined as the number of items it will hold, not the number of bytes. */
+	UBaseType_t uxItemSize;			/*< The size of each items that the queue will hold. */
+
+	volatile int8_t cRxLock;		/*< Stores the number of items received from the queue (removed from the queue) while the queue was locked.  Set to queueUNLOCKED when the queue is not locked. */
+	volatile int8_t cTxLock;		/*< Stores the number of items transmitted to the queue (added to the queue) while the queue was locked.  Set to queueUNLOCKED when the queue is not locked. */
+
+	/*@struct mutex *irqMask;@*/		/*< Ghost mutex simulates the effect of irq masking */
+	/*@struct mutex *schedulerSuspend;@*/	/*< Ghost mutex simulates the effect of scheduler suspension */
+	/*@struct mutex *locked;@*/		/*< Ghost mutex simulates the effect of queue locking */
+} xQUEUE;
+
+typedef xQUEUE Queue_t;
+
+typedef struct QueueDefinition * QueueHandle_t;
+
+/*@
+#define QUEUE_SHAPE(q, Storage, N, M, K)					\
+	malloc_block_QueueDefinition(q) &*&						\
+	q->pcHead |-> Storage &*&								\
+	q->pcWriteTo |-> ?WPtr &*&								\
+	q->u.xQueue.pcTail |-> ?End &*&							\
+	q->u.xQueue.pcReadFrom |-> ?RPtr &*&					\
+	q->uxItemSize |-> M &*&									\
+	q->uxLength |-> N &*&									\
+	q->uxMessagesWaiting |-> K &*&							\
+	q->cRxLock |-> ?rxLock &*&								\
+	q->cTxLock |-> ?txLock &*&								\
+	struct_QueuePointers_padding(&q->u.xQueue) &*&			\
+	struct_SemaphoreData_padding(&q->u.xSemaphore) &*&		\
+	struct_fake_union_t_padding(&q->u) &*&					\
+	struct_xLIST_padding(&q->xTasksWaitingToSend) &*&		\
+	struct_xLIST_padding(&q->xTasksWaitingToReceive) &*&	\
+	q->u.xSemaphore.xMutexHolder |-> _ &*&					\
+	q->u.xSemaphore.uxRecursiveCallCount |-> _ &*&			\
+	true
+
+predicate queue(QueueHandle_t q, int8_t *Storage, size_t N, size_t M, size_t W, size_t R, size_t K, bool is_locked; list<list<char> >abs) =
+	QUEUE_SHAPE(q, Storage, N, M, K) &*&
+	0 < N &*&
+	0 < M &*&
+	0 <= W &*& W < N &*&
+	0 <= R &*& R < N &*&
+	0 <= K &*& K <= N &*&
+	W == (R + 1 + K) % N &*&
+	(-1) <= rxLock &*&
+	(-1) <= txLock &*&
+	(is_locked ? 0 <= rxLock : (-1) == rxLock) &*&
+	(is_locked ? 0 <= txLock : (-1) == txLock) &*&
+	WPtr == Storage + (W*M) &*&
+	RPtr == Storage + (R*M) &*&
+	End == Storage + (N*M) &*&
+	buffer(Storage, N, M, ?contents) &*&
+	length(contents) == N &*&
+	abs == take(K, rotate_left((R+1)%N, contents)) &*&
+	malloc_block(Storage, N*M) &*&
+	true
+	;
+
+predicate buffer(char *buffer, size_t N, size_t M; list<list<char> > elements) =
+	N == 0
+		? elements == nil
+		: chars(buffer, M, ?x) &*& buffer(buffer + M, N - 1, M, ?xs) &*& elements == cons(x, xs);
+
+// TODO: buffer_from_chars proof
+lemma void buffer_from_chars(char *buffer, size_t N, size_t M);
+requires chars(buffer, N*M, _);
+ensures exists<list<list<char> > >(?elements) &*& buffer(buffer, N, M, elements) &*& length(elements) == N;
+
+// TODO: split_element proof
+lemma void split_element<t>(char *buffer, size_t N, size_t M, size_t i);
+requires buffer(buffer, N, M, ?elements) &*& i < N;
+ensures
+	buffer(buffer, i, M, take(i, elements)) &*&
+	chars(buffer + i * M, M, nth(i, elements)) &*&
+	buffer(buffer + (i + 1) * M, (N-1-i), M, drop(i+1, elements));
+
+// TODO: join_element proof
+lemma void join_element(char *buffer, size_t N, size_t M, size_t i);
+requires
+	buffer(buffer, i, M, ?prefix) &*&
+	chars(buffer + i * M, M, ?element) &*&
+	buffer(buffer + (i + 1) * M, (N-1-i), M, ?suffix);
+ensures buffer(buffer, N, M, append(prefix, cons(element, suffix)));
+
+predicate list(List_t *l;) =
+	l->uxNumberOfItems |-> _;
+
+predicate queuelists(QueueHandle_t q;) =
+	list(&q->xTasksWaitingToSend) &*&
+	list(&q->xTasksWaitingToReceive);
+@*/
+
+/* Because prvCopyDataFromQueue does *not* decrement uxMessagesWaiting (K) the
+queue predicate above does not hold as a postcondition. If the caller
+subsequently decrements K then the queue predicate can be reinstated. */
+/*@
+predicate queue_after_prvCopyDataFromQueue(QueueHandle_t q, int8_t *Storage, size_t N, size_t M, size_t W, size_t R, size_t K, bool is_locked; list<list<char> >abs) =
+	QUEUE_SHAPE(q, Storage, N, M, K) &*&
+	0 < N &*&
+	0 < M &*&
+	0 <= W &*& W < N &*&
+	0 <= R &*& R < N &*&
+	0 <= K &*& K <= N &*&
+	W == (R + K) % N &*& //< Differs from queue predicate
+	(-1) <= rxLock &*&
+	(-1) <= txLock &*&
+	(is_locked ? 0 <= rxLock : (-1) == rxLock) &*&
+	(is_locked ? 0 <= txLock : (-1) == txLock) &*&
+	WPtr == Storage + (W*M) &*&
+	RPtr == Storage + (R*M) &*&
+	End == Storage + (N*M) &*&
+	buffer(Storage, N, M, ?contents) &*&
+	length(contents) == N &*&
+	abs == take(K, rotate_left(R, contents)) &*& //< Differs from queue predicate
+	malloc_block(Storage, N*M) &*&
+	true
+	;
+@*/
+
+/* Can't be called `mutex` as this clashes with VeriFast's predicate */
+/*@
+predicate freertos_mutex(QueueHandle_t q, int8_t *Storage, size_t N, size_t K;) =
+	QUEUE_SHAPE(q, Storage, N, 0, K) &*&
+	queuelists(q) &*&
+	0 < N &*&
+	0 <= K &*& K <= N &*&
+	(-1) <= rxLock &*&
+	(-1) <= txLock &*&
+	WPtr == Storage &*&
+	RPtr == Storage &*&
+	End == Storage &*&
+	malloc_block(Storage, 0) &*&
+	chars(Storage, 0, _) &*&
+	true
+	;
+@*/
+
+/* A queuehandle can be shared between tasks and ISRs. Acquiring the ghost
+`irqMask` gives access to the core queue resources. The permissions granted
+after masking interrupts depends on the caller:
+- A task has access to the queue and the queuelists
+- An ISR has access to the queue and, if the queue is unlocked, the queuelists */
+/*@
+predicate queuehandle(QueueHandle_t q, size_t N, size_t M, bool is_isr;) =
+	q->irqMask |-> ?m &*& mutex(m, irqs_masked_invariant(q, N, M, is_isr));
+
+predicate_ctor irqs_masked_invariant(QueueHandle_t queue, size_t N, size_t M, bool is_isr)() =
+	queue(queue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
+	(is_isr && is_locked ? true : queuelists(queue));
+@*/
+
+/* A queuesuspend can be shared between tasks. Acquiring the ghost `schedulerSuspend` gives access to the `locked` mutex. */
+/*@
+predicate_ctor scheduler_suspended_invariant(QueueHandle_t queue)() =
+	queue->locked |-> ?m &*&
+	mutex(m, queue_locked_invariant(queue));
+
+predicate queuesuspend(QueueHandle_t q;) =
+	q->schedulerSuspend |-> ?m &*&
+	mutex(m, scheduler_suspended_invariant(q));
+@*/
+
+/* A queuelock is exclusively acquired by a task. Acquiring the ghost `queuelock` gives access to the queue list resources. */
+/*@
+predicate queuelock(QueueHandle_t q;) =
+	q->locked |-> ?m &*&
+	mutex(m, queue_locked_invariant(q));
+
+predicate_ctor queue_locked_invariant(QueueHandle_t queue)() =
+	queuelists(queue);
+@*/
+
+BaseType_t vListInitialise(List_t *list);
+/*@requires list(list);@*/
+/*@ensures list(list);@*/
+
+BaseType_t listLIST_IS_EMPTY(List_t *list);
+/*@requires list->uxNumberOfItems |-> ?len;@*/
+/*@ensures list->uxNumberOfItems |-> len &*& result == (len == 0 ? pdTRUE : pdFALSE);@*/
+
+typedef struct xTIME_OUT
+{
+	BaseType_t xOverflowCount;
+	TickType_t xTimeOnEntering;
+} TimeOut_t;
+
+/*@
+predicate xTIME_OUT(struct xTIME_OUT *to;) =
+	to->xOverflowCount |-> _ &*&
+	to->xTimeOnEntering |-> _ &*&
+	struct_xTIME_OUT_padding(to);
+@*/
+
+void vTaskInternalSetTimeOutState( TimeOut_t * x);
+/*@requires xTIME_OUT(x);@*/
+/*@ensures xTIME_OUT(x);@*/
+
+BaseType_t xTaskCheckForTimeOut( TimeOut_t * const pxTimeOut, TickType_t * const pxTicksToWait );
+/*@requires xTIME_OUT(pxTimeOut) &*& u_integer(pxTicksToWait, _);@*/
+/*@ensures xTIME_OUT(pxTimeOut) &*& u_integer(pxTicksToWait, _);@*/
+
+BaseType_t xTaskRemoveFromEventList(List_t *list);
+/*@requires list(list);@*/
+/*@ensures list(list);@*/
+
+void vTaskPlaceOnEventList( List_t * const pxEventList, const TickType_t xTicksToWait );
+/*@requires list(pxEventList);@*/
+/*@ensures list(pxEventList);@*/
+
+void vTaskMissedYield();
+/*@requires true;@*/
+/*@ensures true;@*/
+
+void vTaskSuspendAll();
+/*@requires exists<QueueHandle_t>(?xQueue) &*&
+	[1/2]xQueue->schedulerSuspend |-> ?m &*&
+	[1/2]mutex(m, scheduler_suspended_invariant(xQueue));@*/
+/*@ensures [1/2]xQueue->schedulerSuspend |-> m &*&
+	mutex_held(m, scheduler_suspended_invariant(xQueue), currentThread, 1/2) &*&
+	xQueue->locked |-> ?m2 &*&
+	mutex(m2, queue_locked_invariant(xQueue));@*/
+
+BaseType_t xTaskResumeAll( void );
+/*@requires exists<QueueHandle_t>(?xQueue) &*&
+	[1/2]xQueue->schedulerSuspend |-> ?m &*&
+	mutex_held(m, scheduler_suspended_invariant(xQueue), currentThread, 1/2) &*&
+	xQueue->locked |-> ?m2 &*&
+	mutex(m2, queue_locked_invariant(xQueue));@*/
+/*@ensures [1/2]xQueue->schedulerSuspend |-> m &*&
+	[1/2]mutex(m, scheduler_suspended_invariant(xQueue));@*/
+
+void prvLockQueue( QueueHandle_t xQueue );
+/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*&
+	[1/2]queuelock(xQueue); @*/
+/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*&
+	[1/2]xQueue->locked |-> ?m &*&
+	mutex_held(m, queue_locked_invariant(xQueue), currentThread, 1/2) &*&
+	queue_locked_invariant(xQueue)();@*/
+
+void prvUnlockQueue( QueueHandle_t xQueue );
+/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false &*&
+	[1/2]xQueue->locked |-> ?m &*&
+	mutex_held(m, queue_locked_invariant(xQueue), currentThread, 1/2) &*&
+	queue_locked_invariant(xQueue)();@*/
+/*@ensures [1/2]queuehandle(xQueue, N, M, is_isr) &*&
+	[1/2]queuelock(xQueue);@*/
+
+void setInterruptMask(QueueHandle_t xQueue)
+/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/
+/*@ensures [1/2]xQueue->irqMask |-> ?m &*&
+	mutex_held(m, irqs_masked_invariant(xQueue, N, M, is_isr), currentThread, 1/2) &*&
+	queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
+	queuelists(xQueue);@*/
+{
+	/*@open queuehandle(xQueue, N, M, is_isr);@*/
+	mutex_acquire(xQueue->irqMask);
+	/*@open irqs_masked_invariant(xQueue, N, M, is_isr)();@*/
+}
+
+void clearInterruptMask(QueueHandle_t xQueue)
+/*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
+	[1/2]xQueue->irqMask |-> ?m &*&
+	mutex_held(m, irqs_masked_invariant(xQueue, N, M, false), currentThread, 1/2) &*&
+	queuelists(xQueue);@*/
+/*@ensures [1/2]queuehandle(xQueue, N, M, false);@*/
+{
+	/*@close irqs_masked_invariant(xQueue, N, M, false)();@*/
+	mutex_release(xQueue->irqMask);
+	/*@close [1/2]queuehandle(xQueue, N, M, false);@*/
+}
+
+#define taskENTER_CRITICAL() setInterruptMask(xQueue)
+#define taskEXIT_CRITICAL() clearInterruptMask(xQueue)
+#define portYIELD_WITHIN_API()
+#define queueYIELD_IF_USING_PREEMPTION()
+
+UBaseType_t setInterruptMaskFromISR(QueueHandle_t xQueue)
+/*@requires [1/2]queuehandle(xQueue, ?N, ?M, ?is_isr) &*& is_isr == true;@*/
+/*@ensures [1/2]xQueue->irqMask |-> ?m &*&
+	mutex_held(m, irqs_masked_invariant(xQueue, N, M, is_isr), currentThread, 1/2) &*&
+	queue(xQueue, ?Storage, N, M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
+	(is_locked ? true : queuelists(xQueue));@*/
+{
+	/*@open queuehandle(xQueue, N, M, is_isr);@*/
+	mutex_acquire(xQueue->irqMask);
+	/*@open irqs_masked_invariant(xQueue, N, M, is_isr)();@*/
+	return 0;
+}
+
+void clearInterruptMaskFromISR(QueueHandle_t xQueue, UBaseType_t uxSavedInterruptStatus)
+/*@requires queue(xQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
+	[1/2]xQueue->irqMask |-> ?m &*&
+	mutex_held(m, irqs_masked_invariant(xQueue, N, M, true), currentThread, 1/2) &*&
+	(is_locked ? true : queuelists(xQueue));@*/
+/*@ensures [1/2]queuehandle(xQueue, N, M, true);@*/
+{
+	/*@close irqs_masked_invariant(xQueue, N, M, true)();@*/
+	mutex_release(xQueue->irqMask);
+	/*@close [1/2]queuehandle(xQueue, N, M, true);@*/
+}
+
+#define portSET_INTERRUPT_MASK_FROM_ISR() setInterruptMaskFromISR(xQueue)
+#define portCLEAR_INTERRUPT_MASK_FROM_ISR(uxSavedInterruptStatus) clearInterruptMaskFromISR(xQueue, uxSavedInterruptStatus)
+
+#endif /* QUEUE_H */

FreeRTOS/Test/VeriFast/include/proof/queuecontracts.h

@@ -0,0 +1,57 @@
+/*
+ * FreeRTOS VeriFast Proofs
+ * Copyright (C) Amazon.com, Inc. or its affiliates.  All Rights Reserved.
+ *
+ * Permission is hereby granted, free of charge, to any person obtaining a copy of
+ * this software and associated documentation files (the "Software"), to deal in
+ * the Software without restriction, including without limitation the rights to
+ * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+ * the Software, and to permit persons to whom the Software is furnished to do so,
+ * subject to the following conditions:
+ *
+ * The above copyright notice and this permission notice shall be included in all
+ * copies or substantial portions of the Software.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+ * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+ * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+ * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+ * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ */
+
+#ifndef QUEUECONTRACTS_H
+#define QUEUECONTRACTS_H
+
+#include "queue.h"
+
+void prvCopyDataFromQueue( Queue_t * const pxQueue, void * const pvBuffer );
+/*@requires queue(pxQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*& 0 < K &*& chars(pvBuffer, M, _);@*/
+/*@ensures queue_after_prvCopyDataFromQueue(pxQueue, Storage, N, M, W, (R+1)%N, K, is_locked, abs) &*&
+	chars(pvBuffer, M, head(abs));@*/
+
+BaseType_t prvCopyDataToQueue( Queue_t * const pxQueue, const void *pvItemToQueue, const BaseType_t xPosition );
+/*@requires queue(pxQueue, ?Storage, ?N, ?M, ?W, ?R, ?K, ?is_locked, ?abs) &*&
+	(K < N || xPosition == queueOVERWRITE) &*&
+	chars(pvItemToQueue, M, ?x) &*&
+	(xPosition == queueSEND_TO_BACK || xPosition == queueSEND_TO_FRONT || (xPosition == queueOVERWRITE && N == 1));@*/
+/*@ensures
+	(xPosition == queueSEND_TO_BACK
+		? queue(pxQueue, Storage, N, M, (W+1)%N, R, (K+1), is_locked, append(abs, singleton(x)))
+		: (xPosition == queueSEND_TO_FRONT
+			? (R == 0
+				? queue(pxQueue, Storage, N, M, W, (N-1), (K+1), is_locked, cons(x, abs))
+				: queue(pxQueue, Storage, N, M, W, (R-1), (K+1), is_locked, cons(x, abs)))
+			: xPosition == queueOVERWRITE &*& queue(pxQueue, Storage, N, M, W, R, 1, is_locked, singleton(x)))
+	) &*&
+	chars(pvItemToQueue, M, x);@*/
+
+BaseType_t prvIsQueueEmpty( Queue_t * pxQueue );
+/*@requires [1/2]queuehandle(pxQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/
+/*@ensures [1/2]queuehandle(pxQueue, N, M, is_isr);@*/
+
+BaseType_t prvIsQueueFull( Queue_t * pxQueue );
+/*@requires [1/2]queuehandle(pxQueue, ?N, ?M, ?is_isr) &*& is_isr == false;@*/
+/*@ensures [1/2]queuehandle(pxQueue, N, M, is_isr);@*/
+
+#endif /* QUEUECONTRACTS_H */