Experiments

Source Code used for Queries Q1-Q24 in ASE’10 Publication

list2.c:

int partition(int a[], int left, int right) {
  int v = a[right], i = left - 1, j = right, t;
  for (;;) {
    while (a[++i] < v) ;
    while (j > left && a[--j] > v) ;
    if (i >= j) break;
    t = a[i]; a[i] = a[j]; a[j] = t;
  }
  t = a[i]; a[i] = a[right]; a[right] = t;
  return i;
}

int main(int argc, char * argv[]) {
  int A[3];
  partition(A, 0, 2);
}

sort1.c:

#include <stdio.h>
int compare(int a, int b) {
    if (a <= b) return 1;
    return 0;
}

int unfinished();

void sort(int * a, int len) {
    int i, t;
    for (i=1; i<len; ++i) {
        if (compare(a[i-1], a[i])) continue;
        unfinished();
        t=a[i]; a[i]=a[i-1]; a[i-1]=t;
    }
    return;
}

void eval(int * a, int len) {
    int i;
    for (i=0; i < 3; ++i)
        printf("a[%d]=%d\n", i, a[i]);
    return;
}

int main(int argc, char * argv[]) {
    int i; int A[3];
    int verify;
    for (i=0; i < 3; ++i)
        sort(A, 3);
    if (verify) {
        assert(compare(A[0],A[1]));
        assert(compare(A[1],A[2]));
    }
    eval(A, 3);
    return 0;
}

sort2.c:

#include <stdio.h>

int rand_init;

void insert(int * a, int pos) {
    int rand;
    a[pos] = rand%rand_init;
    return;
}

void eval(int * a, int first, int last) {
    if (first > last) return;
    printf("a[%d]=%d\n", first, a[first]);
    eval(a+1, first+1, last);
    return;
}

int precond() {
    return (rand_init == 7);
}

int postcond() {
    return (rand_init == 7);
}

int main(int argc, char * argv[]) {
    int i;
    int A[3];
    int max;

    if(max > 0)
        init: rand_init = 7;

    for (i=0; i<max; ++i)
        insert(A, i);

    eval(A, 0, max);

    return 0;
}

Experiments Performed for our VMCAI’09 Publication

To demonstrate the power of our approach,we considered queries on autopilot.i that
enforce a certain function call stack and focus coverage criteria to single functions:

  > in periodic_task/ cover  passing
    @entry -> / & @entry -> / & @entry -> @exit

queries for a test suite satisfying coverage criteria , where all test cases
start in periodic task passing its entry, thereafter the entry of , the entry
of and finally an exitpoint of periodic task. The following table shows the results.
The last two coverage criteria combine basic block and condition coverage at different
locations in the source code.