source: CIVL/examples/languageFeatures/duffs.cvl

/* Commandline execution:
 *              civl verify duffs.cvl
 * */
#include <civlc.cvh>

$input int a[8];

// This is Stroustrup's version of Duff's device.
void send(int *to, int *from, int count)
{
        int n = (count + 7) / 8;
        switch(count % 8) {
        case 0: do {    *to++ = *from++;
        case 7:         *to++ = *from++;
        case 6:         *to++ = *from++;
        case 5:         *to++ = *from++;
        case 4:         *to++ = *from++;
        case 3:         *to++ = *from++;
        case 2:         *to++ = *from++;
        case 1:         *to++ = *from++;
                            --n;
                } while(n > 0);
        }
}

void main() {
  int b[8];
  send(b, a, 8);
  for (int i = 0; i < 8; i++) {
    $assert(a[i] == b[i]);
  }
}