RiSE4fun samples for VccList of built-in samples for the Vcc in RiSE4funen-USrise4fun &copy; 2017 Microsoft Corporationhttp://rise4fun.com//Images/Rise.gifRiSE4fun samples for Vcchttp://rise4fun.com/Vcc/hellohello#include <vcc.h> int main() { int x, y; _(assert x >= y) return 0; } http://rise4fun.com/Vcc/lsearchlsearch#include <vcc.h> #include <limits.h> unsigned lsearch(int elt, int *ar, unsigned sz) _(requires \thread_local_array(ar, sz)) _(ensures \result != UINT_MAX ==> ar[\result] == elt) _(ensures \forall unsigned i; i < sz && i < \result ==> ar[i] != elt) { unsigned i; for (i = 0; i < sz; i++) _(invariant \forall unsigned j; j < i ==> ar[j] != elt) { if (ar[i] == elt) return i; } return UINT_MAX; } http://rise4fun.com/Vcc/safestringsafestring#include <vcc.h> #include <stdlib.h> struct SafeString { unsigned capacity, len; char *content; _(invariant len < capacity) _(invariant content[len] == '\0') _(invariant \mine((char[capacity])content)) }; void sstr_append_char(struct SafeString *s, char c) _(requires \wrapped(s)) _(requires s->len < s->capacity - 1) _(ensures \wrapped(s)) _(writes s) { _(unwrapping s) { _(unwrapping (char[s->capacity])(s->content)) { s->content[s->len++] = c; s->content[s->len] = '\0'; } } } struct SafeString *sstr_alloc(unsigned capacity) _(requires capacity > 0) _(ensures \result != NULL ==> \wrapped(\result)) { struct SafeString *s; s = malloc(sizeof(*s)); if (s == NULL) return NULL; s->content = malloc(capacity); if (s->content == NULL) { free(s); return NULL; } s->capacity = capacity; s->len = 0; s->content[0] = '\0'; _(wrap (char[capacity])(s->content)) _(wrap s) return s; } http://rise4fun.com/Vcc/bozosortbozosort#include <vcc.h> #include <stdlib.h> unsigned random(unsigned bound) _(requires bound > 0) _(ensures \result < bound) { return _(unchecked)((unsigned)rand()) % bound; } _(logic \bool sorted(int *buf, unsigned len) = \forall unsigned i, j; i < j && j < len ==> buf[i] <= buf[j]) _(typedef unsigned perm_t[unsigned]; ) _(logic \bool is_permutation(perm_t perm, unsigned len) = (\forall unsigned i, j; i < j && j < len ==> perm[i] != perm[j])) _(logic \bool is_permuted(\state s, int *buf, unsigned len, perm_t perm) = \forall unsigned i; i < len ==> perm[i] < len && \at(s, buf[ perm[i] ]) == buf[i]) _(logic perm_t swap(perm_t p, unsigned i, unsigned j) = \lambda unsigned k; k == i ? p[j] : k == j ? p[i] : p[k]) void bozo_sort(int *buf, unsigned len _(out perm_t perm)) _(writes \array_range(buf, len)) _(ensures sorted(buf, len)) _(ensures is_permutation(perm, len)) _(ensures is_permuted(\old(\now()), buf, len, perm)) { _(ghost \state s0 = \now() ) _(ghost perm = \lambda unsigned i; i) if (len == 0) return; for (;;) _(invariant \mutable_array(buf, len)) _(invariant is_permutation(perm, len)) _(invariant is_permuted(s0, buf, len, perm)) { int tmp; unsigned i = random(len), j = random(len); tmp = buf[i]; buf[i] = buf[j]; buf[j] = tmp; _(ghost perm = swap(perm, i, j) ) for (i = 0; i < len - 1; ++i) _(invariant sorted(buf, i + 1)) { if (buf[i] > buf[i + 1]) break; } if (i == len - 1) break; } } http://rise4fun.com/Vcc/spinlockspinlock#include <vcc.h> _(claimable, volatile_owns) struct Lock { volatile int locked; _(ghost \object protected_obj;) _(invariant locked == 0 ==> \mine(protected_obj)) }; void InitializeLock(struct Lock *l _(ghost \object obj)) _(writes \span(l), obj) _(requires \wrapped(obj)) _(ensures \wrapped(l) && l->protected_obj == obj) { l->locked = 0; _(ghost { l->protected_obj = obj; l->\owns = {obj}; _(wrap l) }) } _(atomic_inline) int InterlockedCompareExchange(volatile int *Destination, int Exchange, int Comparand) { if (*Destination == Comparand) { *Destination = Exchange; return Comparand; } else { return *Destination; } } void Acquire(struct Lock *l _(ghost \claim c)) _(always c, l->\closed) _(ensures \wrapped(l->protected_obj) && \fresh(l->protected_obj)) { int stop = 0; do { _(atomic c, l) { stop = InterlockedCompareExchange(&l->locked, 1, 0) == 0; _(ghost if (stop) l->\owns -= l->protected_obj) } } while (!stop); } void Release(struct Lock *l _(ghost \claim c)) _(always c, l->\closed) _(requires l->protected_obj != c) _(writes l->protected_obj) _(requires \wrapped(l->protected_obj)) { _(atomic c, l) { l->locked = 0; _(ghost l->\owns += l->protected_obj) } } typedef struct _DATA { int a; int b; _(invariant a + b > 0) } DATA; _(ghost _(claimable) struct _DATA_CONTAINER { int dummy; _(invariant \mine(&DataLock)) _(invariant DataLock.protected_obj == &Data) } DataContainer;) struct Lock DataLock; DATA Data; void testit(_(ghost \claim c)) _(always c, (&DataContainer)->\closed) { Acquire(&DataLock _(ghost c)); _(unwrapping &Data) { Data.a = 5; Data.b = 7; } Release(&DataLock _(ghost c)); } void boot() _(writes \universe()) _(requires \program_entry_point()) { _(ghost \claim c;) Data.a = 42; Data.b = 17; _(wrap &Data) InitializeLock(&DataLock _(ghost &Data)); _(ghost (&DataContainer)->\owns = {&DataLock, &DataContainer}) _(wrap &DataContainer) _(ghost c = \make_claim({&DataContainer}, (&DataContainer)->\closed);) testit(_(ghost c)); }