PathCrawler Online

Choose any of the programs from the example menu to see an example of test generation. We provide predefined test parameters for each example. You can also elect to customize the test parameters first.

Select an example

Customize test parameters

             /* Should return the type of the triangle 
   which has sides of these lengths.
   3 = not a triangle
   2 = equilateral triangle
   1 = isoceles triangle
   0 = other triangle
*/
int Tritype(double i, double j, double k){
  int trityp = 0;
  if (i < 0.0 || j < 0.0 || k < 0.0)          // line 10  
    return 3;
  if (i + j <= k || j + k <= i || k + i <= j) // line 12 
    return 3;    
  if (i == j) trityp = trityp + 1;            // line 14
  if (i == k) trityp = trityp + 1;            // line 15
  if (j == k) trityp = trityp + 1;            // line 16
  if (trityp >= 2)                            // line 17
      trityp = 2;
  return trityp;
}

             /* Should return the type of the triangle
   which has sides of these lengths.

   2 = equilateral triangle
   1 = isoceles triangle
   0 = other triangle
*/
int Tritype(double i, double j, double k){
  int trityp = 0;
//  if (i < 0.0 || j < 0.0 || k < 0.0)        // line 10  
//    return 3;
//  if (i + j <= k || j + k <= i || k + i <= j)//line 12 
//    return 3; 
  if (i == j) trityp = trityp + 1;            // line 14
  if (i == k) trityp = trityp + 1;            // line 15
  if (j == k) trityp = trityp + 1;            // line 16
  if (trityp >= 2)                            // line 17
      trityp = 2;
  return trityp;
}

             /* Should return the type of the triangle
   which has sides of these lengths.

   2 = equilateral triangle
   1 = isoceles triangle
   0 = other triangle
*/
int Tritype(double i, double j, double k){
  int trityp = 0;
//  if (i < 0.0 || j < 0.0 || k < 0.0)        // line 10  
//    return 3;
//  if (i + j <= k || j + k <= i || k + i <= j)//line 12 
//    return 3; 
  if (i == j) trityp = trityp + 1;            // line 14
  if (i == k) trityp = trityp + 1;            // line 15
  if (j == k) trityp = trityp + 1;            // line 16
  if (trityp >= 2)                            // line 17
      trityp = 2;
  return trityp;
}

             /* Should return the type of the triangle
   which has sides of these lengths.

   2 = equilateral triangle
   1 = isoceles triangle
   0 = other triangle
*/
int Tritype(double i, double j, double k){
  int trityp = 0;
//  if (i < 0.0 || j < 0.0 || k < 0.0)        // line 10  
//    return 3;
//  if (i + j <= k || j + k <= i || k + i <= j)//line 12 
//    return 3; 
  if (i == j) trityp = trityp + 1;            // line 14
  if (i == k) trityp = trityp + 1;            // line 15
  if (j == k) trityp = trityp + 1;            // line 16
  if (trityp >= 2)                            // line 17
      trityp = 2;
  return trityp;
}

int Tritype_precond(double i, double j, double k){
  if (i < 0.0 || j < 0.0 || k < 0.0)          // line 23
    return 0;
  if (i + j <= k || j + k <= i || k + i <= j) // line 25
    return 0;
  return 1;    
}

             /* Should copy all the elements
   of ordered arrays t1 and t2
   into the ordered array t3 */

void Merge(int t1[3], int t2[3], int t3[6]) {

  int i = 0, j = 0, k = 0 ;

  while (i < 3 && j < 3) { // line 09
    if (t1[i] < t2[j]) {   // line 10
      t3[k] = t1[i];
      i++;
    }
    else {
      t3[k] = t2[j];
      j++;
    }
    k++ ;
  }
  while (i < 3) {          // line 20
    t3[k] = t1[i];
    i++;
    k++;
  }
  while (j < 3) {          // line 25
    t3[k] = t2[j];
    j++;
    k++;
  }
}

             /* Should copy all the elements
   of ordered arrays t1 and t2
   into the ordered array t3 */

void Merge(int t1[3], int t2[3], int t3[6]) {

  int i = 0, j = 0, k = 0 ;

  while (i < 3 && j < 3) { // line 09
    if (t1[i] < t2[j]) {   // line 10
      t3[k] = t1[i];
      i++;
    }
    else {
      t3[k] = t2[j];
      j++;
    }
    k++ ;
  }
  while (i < 3) {          // line 20
    t3[k] = t1[i];
    i++;
    k++;
  }
  while (j < 3) {          // line 25
    t3[k] = t2[j];
    j++;
    k++;
  }
}

             /* Should copy all the elements
   of ordered arrays t1 and t2
   of lengths l1 and l2
   into the ordered array t3 */
void Merge (int t1[], int t2[], int t3[], int l1, int l2) {

  int i = 0, j = 0, k = 0 ;

  while (i < l1 && j < l2) { // line 09
    if (t1[i] < t2[j]) {     // line 10
      t3[k] = t1[i];
      i++;
      }
    else {
      t3[k] = t2[j];
      j++;
      }
    k++;
    }
  while (i < l1) {           // line 20
    t3[k] = t1[i];
    i++;

    }
  while (j < l2) {           // line 25
    t3[k] = t2[j];
    j++;
    k++;
    }
}

             /* Should copy all the elements
   of ordered arrays t1 and t2
   of lengths l1 and l2
   into the ordered array t3 */
void Merge (int t1[], int t2[], int t3[], int l1, int l2) {

  int i = 0, j = 0, k = 0 ;

  while (i < l1 && j < l2) { // line 09
    if (t1[i] < t2[j]) {     // line 10
      t3[k] = t1[i];
      i++;
      }
    else {
      t3[k] = t2[j];
      j++;
      }
    k++;
    }
  while (i < l1) {           // line 20
    t3[k] = t1[i];
    i++;

    }
  while (j < l2) {           // line 25
    t3[k] = t2[j];
    j++;
    k++;
    }
}

             /* Should copy all the elements
   of ordered arrays t1 and t2
   of lengths l1 and l2
   into the ordered array t3 */
void Merge (int t1[], int t2[], int t3[], int l1, int l2) {

  int i = 0, j = 0, k = 0 ;

  while (i < l1 && j < l2) { // line 09
    if (t1[i] < t2[j]) {     // line 10
      t3[k] = t1[i];
      i++;
      }
    else {
      t3[k] = t2[j];
      j++;
      }
    k++;
    }
  while (i < l1) {           // line 20
    t3[k] = t1[i];
    i++;

    }
  while (j < l2) {           // line 25
    t3[k] = t2[j];
    j++;
    k++;
    }
}

             /* Should copy all the elements
   of ordered arrays t1 and t2
   of lengths l1 and l2
   into the ordered array t3 */
void Merge (int t1[], int t2[], int t3[], int l1, int l2) {

  int i = 0, j = 0, k = 0 ;

  while (i < l1 && j < l2) { // line 09
    if (t1[i] < t2[j]) {     // line 10
      t3[k] = t1[i];
      i++;
      }
    else {
      t3[k] = t2[j];
      j++;
      }
    k++;
    }
  while (i < l1) {           // line 20
    t3[k] = t1[i];
    i++;

    }
  while (j < l2) {           // line 25
    t3[k] = t2[j];
    j++;
    k++;
    }
}

             /* Should copy all the elements
   of ordered arrays t1 and t2
   of lengths l1 and l2
   into the ordered array t3 */
void Merge (int t1[], int t2[], int t3[], int l1, int l2) {

  int i = 0, j = 0, k = 0 ;

  while (i < l1 && j < l2) { // line 09
    if (t1[i] < t2[j]) {     // line 10
      t3[k] = t1[i];
      i++;
      }
    else {
      t3[k] = t2[j];
      j++;
      }
    k++;
    }
  while (i < l1) {           // line 20
    t3[k] = t1[i];
    i++;

    }
  while (j < l2) {           // line 25
    t3[k] = t2[j];
    j++;
    k++;
    }
}

             /* Should copy all the elements
   of ordered arrays t1 and t2
   of lengths l1 and l2
   into the ordered array t3 */
void Merge (int t1[], int t2[], int t3[], int l1, int l2) {

  int i = 0, j = 0, k = 0 ;

  while (i < l1 && j < l2) { // line 09
    if (t1[i] < t2[j]) {     // line 10
      t3[k] = t1[i];
      i++;
      }
    else {
      t3[k] = t2[j];
      j++;
      }
    k++;
    }
  while (i < l1) {           // line 20
    t3[k] = t1[i];
    i++;

    }
  while (j < l2) {           // line 25
    t3[k] = t2[j];
    j++;
    k++;
    }
}

             int uninit_var(int a[3], int b[3]) {
  int i, k;
  for(i=0; i<2; i++) {     // line 3
      if(a[i] == 0)        // line 4
	return 0;
      if(a[i] != a[i+1])   // line 6
        k = 0;
      else
        if(k == 2)         // line 9
	  return 0;
      while(b[k] != a[i])  // line 11
          if(k == 2)       // line 12
	    return 0;
          else
            k++;
      }
  return 1;
}

             /* Should return 1 if x is an element of ordered array A */
int Bsearch( int A[8], int x) // tested function
{
  int low, high, mid, found ;
  
  low = 0 ;
  high = 7 ;
  found = 0 ;
  while( high > low )                    // line 09
    { mid = (low + high) / 2 ;
    
      if( x == A[mid] )                  // line 12
         found = 1;

      if( x > A[mid] )                   // line 15
        low = mid + 1 ;
      else
        high = mid - 1;
    }  
  mid = (low + high) / 2 ;

  if( ( found != 1)  && ( x == A[mid]) ) // line 22
    found = 1; 
  
  return found ;
}

             /* Should return 1 if x is an element of ordered array A */
int Bsearch( int A[10], int x) // tested function
{
  int low, high, mid, found ;
  
  low = 0 ;
  high = 9 ;
  found = 0 ;
  while( high > low )                    // line 09
    { mid = (low + high) / 2 ;
    
      if( x == A[mid] )                  // line 12
         found = 1;

      if( x > A[mid] )                   // line 15
        low = mid + 1 ;
      else
        high = mid - 1;
    }  
  mid = (low + high) / 2 ;

  if( ( found != 1)  && ( x >= A[mid]) ) // line 22
    found = 1; 
  
  return found ;
}

             /* Should return 1 if x is an element of ordered array A */
int Bsearch( int A[8], int x) // tested function
{
  int low, high, mid, found ;
  
  low = 1 ;
  high = 7 ;
  found = 0 ;
  while( high > low )                    // line 09
    { mid = (low + high) / 2 ;
    
      if( x == A[mid] )                  // line 12
         found = 1;

      if( x > A[mid] )                   // line 15
        low = mid + 1 ;
      else
        high = mid - 1;
    }  
  mid = (low + high) / 2 ;

  if( ( found != 1)  && ( x == A[mid]) ) // line 22
    found = 1; 
  
  return found ;
}

             /* Should return 1 if x is an element of ordered array A */
int Bsearch( int A[8], int x) 
{
  int low, high, mid, found ;
  
  low = 1 ;
  high = 7 ;
  found = 0 ;
  while( high > low )                    // line 09
    { mid = (low + high) / 2 ;
    
      if( x == A[mid] )                  // line 12
         found = 1;

      if( x > A[mid] )                   // line 15
        low = mid + 1 ;
      else
        high = mid - 1;
    }  
  mid = (low + high) / 2 ;

  if( ( found != 1)  && ( x == A[mid]) ) // line 22
    found = 1; 
  
  return found ;
}


int spec_Bsearch(
  int *Pre_A, int *A, 
  int Pre_x, int x, 
  int result_implementation)
{
  int i;
  int present = 0;
  int modif = 8;
  
  for(i=0; i<8; i++)                     // line 38
    {
      if(A[i] != Pre_A[i])               // line 40
        modif = i;
      if(Pre_A[i] == Pre_x)              // line 42
	present = 1;
    }
  if(present==0 && present != result_implementation) {
    return 0; } /* implementation wrongly found x in A */
  else {
    if(present==1 && present != result_implementation) {
      return 0; } /* implementation wrongly said x was not in A */
    else {
      if(modif < 8) {                    // line 51
	return 0; } /* implementation modified A */
      else return 1;
    }
  }
  return 0;
}


int CompareBsearchSpec(int A[8], int x) // tested function
{
  int *Pre_A = (int *)malloc(8 * sizeof(int));
  int i;
  for (i = 0; i < 8; i++)                // line 64
    Pre_A[i] = A[i];
  int result_implementation=Bsearch(A,x);
  return(spec_Bsearch(Pre_A,A,x,x,result_implementation));
}

             int x, y;
int f ( int a ) {
  int sum;  
  if(a == 0){  // line 04
    x = 0; y = 0;
  }else{
    x = 5; y = 5;
  } 
  sum = x + y; // sum can be 0
  pathcrawler_assert( sum != 0 );
  return 10 / sum; // risk of division by 0
}

             int x, y;
int f ( int a ) {
  int sum;  
  if(a == 0){  // line 04
    x = 0; y = 5;
  }else{
    x = 5; y = 0;
  } 
  sum = x + y; // sum cannot be 0
  pathcrawler_assert( sum != 0 );
  return 10 / sum; // risk of division by 0
}

             /* compares (with respect to the lexicographic order) the subarrays
with the first n elements of given arrays t1 and t2,
returns  0 if the subarrays are equal,
         1 if the subarray in t1 is greater than in t2,
        -1 if the subarray in t2 is greater than in t1
*/

int ArrayCmp(int n, int* t1, int* t2) {
  int i;
  for (i = 0; i < n; i++) {   /* line 10 */
    if (t1[i] > t2[i])         /* line 11 */
      return -1;
    else if (t1[i] < t2[i])    /* line 13 */
      return 1;
  }
  return 0;
}

             /* compares (with respect to the lexicographic order) the subarrays
with the first n elements of given arrays t1 and t2,
returns  0 if the subarrays are equal,
         1 if the subarray in t1 is greater than in t2,
        -1 if the subarray in t2 is greater than in t1
*/

int ArrayCmp(int n, int* t1, int* t2) {
  int i;
  for (i = 0; i < n; i++) {   /* line 10 */
    if (t1[i] > t2[i])         /* line 11 */
      return -1;
    else if (t1[i] < t2[i])    /* line 13 */
      return 1;
  }
  return 0;
}

             /* compares (with respect to the lexicographic order) the subarrays 
with the first n elements of given arrays t1 and t2, 
returns  0 if the subarrays are equal,
         1 if the subarray in t1 is greater than in t2,
        -1 if the subarray in t2 is greater than in t1
*/

int ArrayCmp(int n, int* t1, int* t2) {
  int i;
  for (i = 0; i < n; i++) {   /* line 10 */
    if (t1[i] > t2[i])        /* line 11 */
      return -1;
    else if (t1[i] < t2[i])   /* line 13 */
      return 1;
  }
  return 0;
}

             /* compares (with respect to the lexicographic order) the subarrays 
with the first n elements of given arrays t1 and t2, 
returns  0 if the subarrays are equal,
         1 if the subarray in t1 is greater than in t2,
        -1 if the subarray in t2 is greater than in t1
*/

int ArrayCmp(int n, int* t1, int* t2) {
  int i;
  for (i = 0; i < n; i++) {   /* line 10 */
    if (t1[i] > t2[i])        /* line 11 */
      return 1;
    else if (t1[i] < t2[i])   /* line 13 */
      return -1;
  }
  return 0;
}

             /* Bubble sort of a given array 'table' of 
   a given length 'l' in ascending order */

void bsort (int * table, int l) 
{
  int i, temp, nb;
  char done;
  done = 0;
  nb = 0;
  while ( !done && (nb < l-1)){      /* line 10 */
    done = 1;
    for (i=0 ; i<l-1 ; i++)          /* line 12 */
      if (table[i] > table[i+1]){    /* line 13 */
	done = 0;
	temp = table[i];
	table[i + 1] = temp;
      }
    nb++;
  }
}

             int f(int x){ 
  if(x < 0)           // line 2
    x = x + 1; 
  if(x != 1)          // line 4
    x = 2*x; 
  return x; 
} 

int spec_f(int x){ 
  if(x < 1)           // line 10
    x = 2*(x + 1); 
  else 
    x = 2*x; 
  return x; 
} 

int cross_f(int x){
  int imp = f(x);
  int spec = spec_f(x);
  if(imp != spec)     // line 20
    return 0; 
  else return 1;
}

             /* Binary search of a given element in a given ordered array
   returning 1 if the element is present and 0 if not.

   In this example, the array dimension is fixed.
   The example is interesting because of
   - the loop with a varaible number of iterations
   - the precondition that the input array is ordered and
   - an example of an oracle which is a more inefficient implementation
     of the same algorithm. */

int Bsearch( int A[10], int elem)
{
  int low, high, mid, found ;

  low = 0 ;
  high = 9 ;
  found = 0 ;
  while( ( high > low ) )                     /* line 18 */
    { 
      mid = (low + high) / 2 ;
      if( elem == A[mid] )                    /* line 21 */
	found = 1;
      if( elem > A[mid] )                     /* line 23 */
        low = mid + 1 ;
      else
        high = mid - 1;
    }  
  mid = (low + high) / 2 ;

  if( ( found != 1)  && ( elem == A[mid]) )   /* line 30 */
    found = 1; 

  return found ;
}

             
/* Binary search of a given element in a given ordered array
   returning 1 if the element is present and 0 if not.


   This example is like Bsearch
   but gives an example of 
   a precondition coded in C */


int Bsearch( int A[10], int elem)
{
  int low, high, mid, found ;
  
  low = 0 ;
  high = 9 ;
  found = 0 ;
  while( ( high > low ) )                     /* line 18 */
    { 
      mid = (low + high) / 2 ;
      if( elem == A[mid] )                    /* line 21 */
	found = 1;
      if( elem > A[mid] )                     /* line 23 */
        low = mid + 1 ;
      else
        high = mid - 1;
    }  
  mid = (low + high) / 2 ;
  
  if( ( found != 1)  && ( elem == A[mid]) )   /* line 30 */
    found = 1; 
  
  return found ;
}

/* C precondition of function Bsearch
   This must have the name of the tested function suffixed with _precond
   and have the same number of arguments with the same types.
   It must return 1 if the parameter values satisfy the precondition and 0 if not */
int Bsearch_precond( int A[10], int elem) {
  int i;
  for (i = 0; i < 9; i++){
    if (A[i]>A[i+1])
      return 0 ;             /* not ordered by increasing value */
  }
  return 1;
}

             /* Binary search of a given element in a given ordered array
   returning 1 if the element is present and 0 if not.

   This example is like Bsearch but contains an error at line 21
   which causes several cases to have a "failure" verdict.
   
   For most of the failed test cases,
   this implementation returns 1 even though the element is not present in the array,
   which gives an indication of the location of the error. */

int Bsearch( int A[10], int elem)
{
  int low, high, mid, found ;

  low = 0 ;
  high = 9 ;
  found = 0 ;
  while( ( high > low ) )                     /* line 18 */
    { 
      mid = (low + high) / 2 ; /* error, next line should be : if( elem == A[mid] ) */
      if( elem != A[mid] )                    /* line 21 */ 
	found = 1;
      if( elem > A[mid] )                     /* line 23 */
        low = mid + 1 ;
      else
        high = mid - 1;
    }  
  mid = (low + high) / 2 ;

  if( ( found != 1)  && ( elem == A[mid]) )   /* line 30 */
    found = 1; 

  return found ;
}

             /* Binary search of a given element in a given ordered array
   returning 1 if the element is present and 0 if not.

   This example is like Bsearch but contains an error at line 30
   which causes several cases to have a "failure" verdict.
   
   The failed test cases are exactly those which cover the paths
   in which the 1st subcondition of line 30 is satisfied,
   which indicates the location of the error. */

int Bsearch( int A[10], int elem)
{
  int low, high, mid, found ;

  low = 0 ;
  high = 9 ;
  found = 0 ;
  while( ( high > low ) )                     /* line 18 */
    { 
      mid = (low + high) / 2 ;
      if( elem == A[mid] )                    /* line 21 */ 
	found = 1;
      if( elem > A[mid] )                     /* line 23 */
        low = mid + 1 ;
      else
        high = mid - 1;
    }  
  mid = (low + high) / 2 ;
  /* error, next line should be : if( ( found != 1)  && ( elem == A[mid]) ) */
  if( ( found != 1)  && ( elem != A[mid]) )    /* line 30 */
    found = 1; 

  return found ;
}

             /* Binary search of a given element in a given ordered array
   returning 1 if the element is present and 0 if not.

   This example is like Bsearch but contains an error at line 31
   which causes several cases to have a "failure" verdict.
   
   The failed test cases are exactly those which cover the paths
   in which the 2nd subcondition of line 30 is satisfied,
   which indicates the location of the error. */

int Bsearch( int A[10], int elem)
{
  int low, high, mid, found ;

  low = 0 ;
  high = 9 ;
  found = 0 ;
  while( ( high > low ) )                     /* line 18 */
    { 
      mid = (low + high) / 2 ;
      if( elem == A[mid] )                    /* line 21 */ 
	found = 1;
      if( elem > A[mid] )                     /* line 23 */
        low = mid + 1 ;
      else
        high = mid - 1;
    }  
  mid = (low + high) / 2 ;

  if( ( found != 1)  && ( elem == A[mid]) )   /* line 30 */    
    found = 0; /* error, should be: found =  1; */

  return found ;
}

             /* Bubble sort of a given array 'table' of 
   a given length 'l' in descending order

   This example is interesting because of its
   - variable dimension input array
   - loop with a variable number of iterations,
     which is limited by limiting the array dimension
   - oracle which does not sort but checks the result is ordered */

void bsort (int * table, int l) 
{
  int i, temp, nb;
  char fini;
  fini = 0;
  nb = 0;
  while ( !fini && (nb < l-1)){      /* line 16 */
    fini = 1;
    for (i=0 ; i<l-1 ; i++)          /* line 18 */
      if (table[i] < table[i+1]){    /* line 19 */
	fini = 0;
	temp = table[i];
	table[i] = table[i + 1];
	table[i + 1] = temp;
      }
    nb++;
  }
}

             /* Merge of two given ordered arrays t1 and t2 of length l1 and l2 resp.
   into a ordered array t3

   This example is interesting because
   - there are many infeasible paths
   - it inputs arrays of variable length
   - the k-path criterion is used to limit the number of paths
   - it needs a precondition : t1 and t2 must be ordered and
     l1 resp. l2 must be no greater than the dimension of t1 resp. t2 and
     the dimension of t3 must be no smaller than the sum of the dimensions of t1 and t2
   - the oracle can also be quite complicated: t1 and t2 should not be modified
     t3 should contain just the elements of t1 and t2,
     with the same number of occurrences and in order */

void Merge (int t1[], int t2[], int t3[], int l1, int l2) {

  int i = 0;
  int j = 0;
  int k = 0;

  while (i < l1 && j < l2) {     /* line 21 */
    if (t1[i] < t2[j]) {     /* line 22 */
      t3[k] = t1[i];
      i++;
      }
    else {
      t3[k] = t2[j];
      j++;
      }
    k++;
    }
  while (i < l1) {     /* line 32 */
    t3[k] = t1[i];
    i++;
    k++;
    }
  while (j < l2) {     /* line 37 */
    t3[k] = t2[j];
    j++;
    k++;
    }
}

             

/* Merge of two given ordered arrays 
   t1 and t2 of length l1 and l2 resp.
   into a ordered array t3


   This example is like Merge
   but gives an example of a precondition 
   coded in C */




void Merge (int t1[], int t2[], int t3[], int l1, int l2) {

  int i = 0;
  int j = 0;
  int k = 0;

  while (i < l1 && j < l2) {     /* line 21 */
    if (t1[i] < t2[j]) {     /* line 22 */
      t3[k] = t1[i];
      i++;
      }
    else {
      t3[k] = t2[j];
      j++;
    }
    k++;
  }
  while (i < l1) {     /* line 32 */
    t3[k] = t1[i];
    i++;
    k++;
  }
  while (j < l2) {     /* line 37 */
    t3[k] = t2[j];
    j++;
    k++;
  }
}

/* C precondition of function Merge
   This must have the name of the tested function suffixed with _precond
   and have the same number of arguments with the same types.
   It must return 1 if the parameter values satisfy the precondition and 0 if not */
int Merge_precond(int t1[], int t2[], int t3[], int l1, int l2) {
  if (l1 > pathcrawler_dimension(t1)
      || l2 > pathcrawler_dimension(t2)
      || l1+l2 > pathcrawler_dimension(t3)) {
    return 0;
  }
  int i;
  for (i=1; i < l1; i++) {
    if (t1[i-1] > t1[i]) {
      return 0;
    }
  }
  for (i=1; i < l2; i++) {
    if (t2[i-1] > t2[i]) {
      return 0;
    }
  }
  return 1;
}

             

/* Merge of two given ordered arrays t1 and t2 of length l1 and l2 resp.
   into a ordered array t3

   This example is the same as Merge except that it contains an error at line 32
   which provokes a buffer overflow.
   This usually causes Merge to crash when executed on one of the test cases.
   In this case, the trace file (which can be viewed by clicking on the
   "Trace" button at the left-hand side of the Test Session Results window)
   contains a TEST EXECUTION WARNING which explains the cause of the crash.
   ( Attention: it is a cumulative trace
   for the whole user sesssion so examine the end of it) */

void Merge (int t1[], int t2[], int t3[], int l1, int l2) {

  int i = 0;
  int j = 0;
  int k = 0;

  while (i < l1 && j < l2) {     /* line 21 */
    if (t1[i] < t2[j]) {     /* line 22 */
      t3[k] = t1[i];
      i++;
      }
    else {
      t3[k] = t2[j];
      j++;
      }
    k++;
    }     /* error, next line should be : while (i < l1) */
  while (i <= l1) {     /* line 32 */
    t3[k] = t1[i];
    i++;
    k++;
    }
  while (j < l2) {     /* line 37 */
    t3[k] = t2[j];
    j++;
    k++;
    }
}

             

/* Merge of two given ordered arrays t1 and t2 of length l1 and l2 resp.
   into a ordered array t3

   This example is the same as Merge except that it contains an error at line 35
   which means that the index of t3 is not incremented
   and the same element of t3 is overwritten.
   This causes some test-cases to give a "failure" verdict.
   By examining the outputs of these test-cases,
   the user will see that not all elements of t3 are written
   (an error that cannot be directly detected by the oracle).
   This information can be used to locate the bug. */

void Merge (int t1[], int t2[], int t3[], int l1, int l2) {

  int i = 0;
  int j = 0;
  int k = 0;

  while (i < l1 && j < l2) {     /* line 21 */
    if (t1[i] < t2[j]) {     /* line 22 */
      t3[k] = t1[i];
      i++;
      }
    else {
      t3[k] = t2[j];
      j++;
      }
    k++;
    }
  while (i < l1) {     /* line 32 */
    t3[k] = t1[i];
    i++;
/* error : missing instruction k++; here */
    }
  while (j < l2) {     /* line 37 */
    t3[k] = t2[j];
    j++;
    k++;
    }
}

             /* A little example from test generation literature
   containing arrays with fixed dimensions and loops with fixed limits
   but the oracle is more complicated than the implementation !
   
   Returns 0 if at least one element of array a
                and all elements of array b
                are equal to target
   and 1 otherwise */

int sample(int a[4], int b[4], int target)
{
  int i, fa, fb;

  i=0;
  fa=0;  /* found at least one occurrence of target in array a */
  fb=0;  /* found at least one occurrence of target in array a
            and all elements of array b are equal to target */

  while(i<=3){                    /* line 19 */
    if(a[i]==target) fa=1;        /* line 20 */
    ++i;
  }
  if(fa==1){                      /* line 23 */
    i=0;
    fb=1;
    while(i<=3){                  /* line 26 */
      if(b[i]!=target) fb=0;      /* line 27 */
      ++i;
    }
  }
  if(fb==1) return 0;             /* line 31 */
  else return 1;
  
}

             /* A classic example from test generation literature
   which contains no loops or arrays
   but is interesting for its simple example of an oracle.
   This implementation does not handle negative inputs correctly */

/* Determines the type of a triangle given its three edges i,j,k */
/* 4 = Not a triangle         */
/* 3 = Equilateral triangle  */
/* 2 = Isosceles triangle */
/* 1 = Any other triangle */

int tritype(int i, int j, int k){
  int type_code;
  if ((i == 0) || (j == 0) || (k == 0)) type_code = 4;     /* line 14 */
  else {
    type_code = 0;
    if (i == j) type_code = type_code + 1;                 /* line 17 */
    if (i == k) type_code = type_code + 2;                 /* line 18 */
    if (j == k) type_code = type_code + 3;                 /* line 19 */
    if (type_code == 0){                                   /* line 20 */
      if ((i+j <= k) || (j+k <= i) || (i+k <= j))          /* line 21 */
	type_code = 4;
      else
	type_code = 1;
      }
    else if (type_code > 3) type_code = 3;                 /* line 26 */
    else if ((type_code == 1) && (i+j > k)) type_code = 2; /* line 27 */
    else if ((type_code == 2) && (i+k > j)) type_code = 2; /* line 28 */
    else if ((type_code == 3) && (j+k > i)) type_code = 2; /* line 29 */
    else type_code = 4;
    }
  return type_code;
}

Guidelines for code upload

Submit your C source code in a tar or zip archive.
Indicate the function under test and the main file under test with its relative path in the archive.
The main file may include other files using their relative paths.
Absolute paths should not be used.

PathCrawler automatically generates test inputs for your function written in ANSI C. The test set will guarantee coverage of all feasible execution paths under the conditions detailed below. Moreover, if you supply an oracle, PathCrawler will also provide the results according to the oracle when the tests are run on instrumented code on our server.

Automatic testing tools allow huge savings but they do not exonerate the user from thinking carefully about what they want testing to achieve. To successfully use PathCrawler, the user must provide not only the full source code (with C stubs for missing functions), but also must set the test parameters and program the oracle. This demands a different mindset from that used for manual unit testing.

To familiarize yourself with PathCrawler, try the tutorial, which uses these examples. You can then try testing some of the other examples from the Examples page. You should then be ready to try testing your own code, by clicking on Test your code at the top of the Examples page.

Follow 3 steps, explained in more detail below, to generate test-cases:

upload the source code and identify the function to be tested;
define the test context;
automatically generate test-cases.

You must provide the ANSI C source files of the top-level function under test and of all other functions (including library functions) called by the function under test, so that it is possible for PathCrawler to recompile your code using gcc. See below for C constructions not yet treated by PathCrawler. No assembly code must be included in the files. Submit your C source code in a tar (but NOT tar.gz) or zip archive. The main file (including the definition of the function to be tested) may include other files using their relative paths. Absolute paths should not be used.

Indicate the function to be tested and the file containing the definition of this function, with its relative path in the archive.

The context includes

The list of scalar variables and data structure elements which are effective input parameters of the tested function, including global variables and those pointed to by the formal parameters
If an array has one or more variable dimensions and it has elements which are effective input parameters, so that the number of effective input parameters depends on the variable dimensions of the array, then these dimensions are also considered as effective input parameters
The input domain for each of these parameters within which PathCrawler will select a value for each test-case
The preconditions: further restrictions on legitimate input parameter values, including relations between the values of different parameters
The oracle
The coverage criterion

A default test context is automatically constructed by PathCrawler. In this default context

All scalar variables and data structure elements which may be referenced by the tested function are counted as effective input parameters. These include the formal arguments of the function under test and any global variables.
The input domain is any value within the declared C type of the parameter. The default input domain of array dimensions is set to the declared domain, if there is one, and otherwise the interval 0..1. Note that this allows PathCrawler to construct test-cases including NULL pointers.
The precondition accepts as a legitimate test-case all combinations of values in the parameter domains.
The oracle always returns unknown

It is very important to check the default test context and modify it if necessary by clicking on Customize test parameters. If you do not do this then PathCrawler may spend a lot of time generating tests which are of no use to you because they do not correspond to realistic inputs for your function and reveal "false-positive" bugs which do not exist under realistic conditions. Here are a few examples:

do you want test-cases with NULL pointer inputs, i.e. in which the dimension of a pointer is set to 0 ?
do you want test-cases in which an array with a variable dimension is either a NULL pointer or has only one element (dimension = 0 or 1) ?
if a variable represents the speed of a vehicle in km/h, do you really want a test-case in which it is set to 500000 ?
do you really want test-cases which provoke integer overflows in the calculations ?

The example functions in the tutorial and on the Examples page come with examples of test contexts that you can study by clicking on Customize test parameters. Once you have done that, try defining the test context for your code.

List of input parameters and their domains

Start by restricting the domains of input parameters and enlarging those of variable dimensions, as necessary.

If the list of input parameters contains variables or data-structure elements which you are SURE are not really referenced by the tested function, then you can just remove them from the list. Also, by default all elements of the same array are given the same domain (by using a variable name starting with INDEX in the name of the element). If you want to give a specific domain to certain elements then add those elements as separate parameters.

Note that setting an interval for the dimension of an array which includes the value 0 signifies that the effective parameter may be a NULL pointer in some test-cases (remember that C treats all array inputs as pointers).

Definition of the preconditions

Suppose that one input parameter, pt, of the tested function is such a pointer and another input parameter, l, represents the number of elements to treat in the array pointed to by the first parameter. A test-case in which pt is set to 1 and l is set to 3 is likely to provoke a buffer overflow. To ensure that only test-cases which do not provoke a buffer overflow are generated, you must define a precondition to link the dimension of pt to the value of l.

There are three ways to define a precondition in PathCrawler. These mechanisms can be combined but it is easier to start by choosing just one.

Write a C function which returns 1 if the test-case values satisfy the precondition and 0 if not. Include this precondition function in the file containing the definition of the tested function. In order for PathCrawler to recognise the precondition function, it must be called precond_name of the tested function and have the same signature as the tested function, except that its return type is int. See the MergePrecond example (click on Customize test parameters). Note that the precondition does not construct input values but just tests the validity of given combinations. Use the pathcrawler_dimension function to restrict dimension values. It is not currently possible to add a precondition definition to an ongoing PathCrawler session. If your source code did not include a precondition for the tested function and, when inspecting the default test context, you decide that you need a precondition and would like to write it in C, then stop your PathCrawler session, add the precondition function to your source code, start a new PathCrawler session, check that PathCrawler has found your precondition and check the box to indicate you want PathCrawler to use it.
Certain preconditions can be defined as formulae in a subset of 1st order logic. See the Merge example (click on Customize test parameters). Note that in this example, there are 2 types of precondition: simple preconditions and quantified preconditions. The latter apply to several elements of the same array; the element index is "universally quantified" and must be given a name which starts with INDEX. Array dimensions can be referred to in preconditions by using a term of the form dim(name of the array).
You can insert calls to the function pathcrawler_assume in the source-code of the tested function. pathcrawler_assume takes one argument which is an inequality between expressions over the variables in the scope of the tested function and which may also use pathcrawler_dimension.

Oracle

PathCrawler can generate inputs to explore all behaviours of your function but it cannot know whether the results are what you expected. That is the role of the oracle. PathCrawler provides a default oracle program which just says that the verdict of each test-case (when run on instrumented code on our server) is unknown. You can change the default oracle in order to calculate another verdict, based on your knowledge of the expected outputs of the tested function. Look at the oracle for Bsearch to see an example (click on Customize test parameters). The default oracle always returns immediately after calling pathcrawler_verdict_unknown. Your oracle should return immediately after having called pathcrawler_verdict_success or pathcrawler_verdict_failure. Your oracle must have exactly the same name and signature as the default oracle. Its arguments are pathcrawler_retres__name of the tested function> for the value returned by the tested function, the input parameters of the tested function (representing their value after execution of the tested function), and the arguments whose name starts with Pre_ representing the values the input parameters had when the tested function was called.

Indeed, the output of the function under test may overwrite the input in some cases (for example, array sorting algorithms will usually overwrite the initial array) and PathCrawler runs the oracle function after the tested function, when the input may be already overwritten. Since the oracle has to examine both input and output data of the tested function, these additional parameters are added to the oracle function signature. The parameters with no prefix are exactly the variables which were provided while calling the function under test, so at the moment when the oracle function is called, they may contain the output values of the function under test. The parameters with the Pre_ prefix will contain (recursive) copies of the input data provided when the function was called. They are not in the scope of the tested function, so cannot be modified. Although this duplication of parameters is systematic, the difference is only important for pointers and arrays (or structures containing them). Note that the oracle can also use the same Pre_ naming convention to refer to the values before the tested function was called of any global variables that it may access.

You can also insert calls to the function pathcrawler_assert in the source-code of the tested function. This feature may be seen as another way to write an oracle. However, unlike the usual oracle described above, pathcrawler_assert may be used at any location in the program under test, and will force PathCrawler to generate test cases to cover both the case where its argument is true and the case where it is is false. pathcrawler_assert takes one argument which is an inequality between expressions over the variables in the scope of the tested function. This inequality is evaluated when the test-case is run and if its value is false then execution of the test-case is stopped and the violation of the assertion (and the line number of the assertion) is indicated in the test-case results.

Coverage criterion

This defines which items must be covered by the set of tests: set it to all to cover all feasible execution paths or, for a tested function containing loops with a variable number of iterations, it can be set to a positive integer, called k, to cover all k-paths i.e. all feasible execution paths with no more than k iterations of each loop with a variable number of iterations. Note that setting the k-path criterion does not guarantee that no tests with more than k iterations of each loop with a variable number of iterations will be generated. Indeed, PathCrawler may happen to generate such a test because PathCrawler searches for any test to cover a given path prefix, and does not choose the path suffix, so the suffix may contain the kth iteration of a loop. However, PathCrawler will not try to cover any path prefixes containing more than k iterations of a loop with a variable number of iterations.

Once you either click on Test with predefined parameters or confirm the modified test context by clicking Confirm parameters, then test-case generation will begin. Wait until it has finished to examine the results. These include

the confirmation that test generation terminated normally or, if not, an indication of what went wrong in case you need to correct the test context and try again
the inputs, outputs, path covered and verdict of each test-case.

Display of paths and partial paths:

The following notation is used when displaying paths and partial paths: <filename>:+N (resp. -N) means that the (first) condition at line N of C source file <filename> is verified (resp. not verified) in the current path. So, merge.c:+10 means that the first condition at line 10 of file merge.c is verified and merge.c:-21 means that the condition at line 21 of file merge.c is not verified. Since line 10 of the source code of merge.c (see the examples on the Examples page) is while (i < l1 && j < l2) this line actually contains two sub-conditions. Here +10 actually means that the first condition i<l1 is verified and -10b means that the second condition j<l2 is not verified. In the same way +Nc or -Nc would represent the third condition of line N and so on. When a line contains more than one condition, the line number is suffixed with _1, _2, etc. so, for example, -34_2c refers to negation of the third sub-condition of the second if on line 34.

Within the covered path, the path prefix which PathCrawler was trying to cover when this path was generated is displayed in black type, whereas the rest of the path is displayed in grey type. This makes it easier to see the exploration of the tree of execution paths in the Paths explored page.

Verdict of the test-case:

If the test-case runs to completion, then the verdict may be unknown if the default oracle is used or, if you supply an oracle, success or failure (with a message indicating the line number of the failure decision in the oracle source code). If the source code contains calls to pathcrawler_assert then the verdict may also be assertion violated (with a message indicating the line number of the relevant assertion). However, if the test case provokes some problem during execution then the verdict may be hung, crashed or interrupt. If PathCrawler detects what seems to be an attempt to read the value of an uninitialised variable during execution of the test-case, then the verdict will be uninit var (note that this can also arise because you mistakenly removed the variable from the list of effective input parameters in the test context). A test-case which covers a path containing a C language construction that PathCrawler was unable to treat is given the verdict untreated and if it covers a path which attempts to read the value of an uninitialised variable then it is given given the verdict uninit var. Cases whose treatment reveals some bug in PathCrawler are given verdict PC bug and they are saved by the server for analysis. If there is some problem during the execution of the oracle, then the verdict will be assert violated in oracle or bug oracle.

You may also want to look at further information:

The C source file which can be used to run each test-case.
Path predicate: the conditions which the inputs must respect in order to activate the same path as the one covered by this test case.
Symbolic outputs: these are the output values expressed in terms of the input values. Along with the path predicate, they form a "specification" of the calculation implemented by this path.
Statistics (such as duration) of the test generation session and of each test case.
The order of exploration of all the paths and partial paths during test generation and, for each one, whether it was covered by a test-case, found to be infeasible or could not be treated for some reason.

Status of a path prefix:

The status of path prefixes which are successfully covered by a test-case is covered. Note that the path effectively covered by the test-case which was found may well be longer than the prefix. Prefixes which are successfully proved to be infeasible have status infeasible. In this case, all paths which are extensions of such a prefix are also infeasible. Prefixes which are supposed infeasible because constraint solving timed out have status timeout. Prefixes which are not explored because they violate a call to pathcrawler_assume have status assume violated. A path prefix which has status subsumed was originally covered by a test-case which violated a pathcrawler_assume and so one extension of this path prefix was given the status assume violated. Only the alternative extensions, indicated by the explanatory message subsumed by, could therefore be explored.

The test set generated by PathCrawler is guaranteed to cover all feasible execution paths (or k-paths) providing that:

constraint resolution does not time out,
no run-time errors are found in the tested function,
test generation terminates normally within the limits on time and space which we are obliged to impose
and the tested function does not contain certain constructions which PathCrawler does not treat well yet, such as:
- reading data from console or files (scanf, fscanf,...): simulate instructions such as scanf by defining a global array to store the file content and replacing the call to scanf by an array access
- the floating-point type float (but double is treated),
- explicit or implicit casts other than those between integer types (e.g. pointer casts, certain uses of unions),
- assembly language code,
- pointers to functions on input,
- formal parameters which are functions,
- recursive structures on input,
- pointers of type void* on input,
- functions with a variable number of arguments,
- recursive functions,
- volatile variables,
- functions from a standard C library or any other function whose source code is not available may not be treated correctly,
- some conversions of the type of integer constants: we can add the letter L (or l) at the end of the constant to ensure that the type long is used, and we can add U (or u) to specify the attribute unsigned. But we cannot write a positive constant greater than the capacity of unsigned long int type or a negative constant not representable in long int type because then the meaning is unclear and PathCrawler cannot guarantee good behaviour.

This is the online version of the PathCrawler test generation tool developed at CEA LIST. To obtain an unrestricted, executable version of PathCrawler, notably for evaluation or use in research, please contact PathCrawler@cea.fr.

PathCrawler's principal functionality, and the one demonstrated in this online version, is to automate structural unit testing by generating test inputs for full coverage of the C function under test. Full coverage can mean all feasible execution paths or k-path coverage which restricts the all-path criterion to paths with at most k consecutive loop iterations. These are available in this online version. PathCrawler can also be used to satisfy other coverage criteria (such as branch coverage, MC-DC,...), to generate supplementary tests to improve coverage of an existing functional test suite or to generate just the tests necessary to cover the part of the code which has been impacted by a modification.

PathCrawler can be used to ensure, and demonstrate, code coverage when this is imposed by a standard. However, it can also be used even when code coverage is not imposed, as a convenient and rigorous way of debugging code fragments during development.

Apart from generating tests to ensure coverage, PathCrawler can be used to detect all run-time errors, anomalies such as uninitialized variables or integer overflows and unreachable code.

Another use is to cross-check one implementation against another (previous version or implementation for another platform) or to check conformity with a specification coded in C. PathCrawler will either find test-cases to demonstrate any differences between the results of the two codes or else demonstrate that no such differences exist.

The path tests generated by PathCrawler can also be used to measure the effective execution time of an uninterrupted task in a real-time application, and get an accurate estimate of the longest execution time.

PathCrawler is also available as a plug-in of the Frama-C code analysis platform. As such, it can be used in combination with other Frama-C plug-ins. For example, the SANTE prototype combines PathCrawler with the Frama-C Value Analysis and Slicing plug-ins in order to confirm or invalidate possible run-time errors. Another combination currently being investigated at CEA LIST is the use of PathCrawler to test code annotations expressed in the language used by the E-ACSL plug-in.

PathCrawler is based on a method which was subsequently baptized concolic or Dynamic Symbolic Execution, i.e. it uses a combination of concrete test inputs and symbolic reasoning.

PathCrawler differs in two main ways from other tools based on this combination.

Like other tools, PathCrawler runs the program under test on each test-case in order to recover a trace of the execution path. However, in PathCrawler's case actual execution is chosen over symbolic execution merely for reasons of efficiency and to demonstrate that the test does indeed activate the intended execution path. Unlike tools designed mainly for bug-finding, PathCrawler does not use actual execution to recover the concrete results of calculations that it cannot treat. This is because these results can only provide an incomplete model of the program's semantics and PathCrawler aims for complete coverage of a certain class of programs rather than for incomplete coverage of any program.

Indeed, incomplete coverage often enables many bugs to be detected but PathCrawler was designed for use in more formal verification processes where coverage must be quantified and justified. If a branch or path is not covered by a test, then unreachableness of the branch or infeasibility of the path must be demonstrated. Moreover, using Pathcrawler in the other ways mentioned above also necessitates complete coverage.

The second main difference between Pathcrawler and other similar tools is that PathCrawler is based not on a SAT, linear or SMT solver but on the finite domain constraint solver COLIBRI, also developed at CEA LIST. PathCrawler and COLIBRI are both implemented in Constraint Logic Programming (CLP), which facilitates low-level control of constraint resolution and the development of specialized constraints, as well as providing an efficient backtracking mechanism.

COLIBRI can treat non-linear arithmetic and provides specialized constraints for modular integer arithmetic and floating-point arithmetic. Within PathCrawler, further specialized constraints have been developed to treat bit operations, casts, dynamic allocation, arrays with (any number of) variable dimensions and array accesses using variable index values.

The attempt to correctly treat all C instructions is ongoing but PathCrawler can already treat a large class of C programs.

For more information on how PathCrawler is implemented and has been used, as well as current research directions, please consult the following publications:

Nicky Williams, Bruno Marre, Patricia Mouy. On-the-fly generation of k-paths tests for C functions : towards the automation of grey-box testing. In Proc. 19th IEEE Intl. Conference on Automated Software Engineering (ASE 2004), 20-25 September 2004, Linz, Austria, IEEE Computer Society, 2004, ISBN 0-7695-2131-2, pages 290-293 The final publication is available from IEEE
Nicky Williams, Bruno Marre, Patricia Mouy, Muriel. Roger. PathCrawler: automatic generation of path tests by combining static and dynamic analysis. In Proc. 5th European Dependable Computing Conference (EDCC-5), Budapest, Hungary, April 20-22, 2005, Lecture Notes in Computer Science 3463 Springer 2005, ISBN 3-540-25723-3, Budapest, Hungary, April 2005, pages 281-292. The final publication is available at www.springerlink.com.
Nicky Williams. WCET measurement using modified path testing. In Proc. 5th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, Palma de Mallorca, Spain, July 2005, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 2007. The final publication is available at DROPS.
Patricia Mouy, Bruno Marre, Nicky Williams, Pascale Le Gall. Generation of all-paths unit test with function calls. In Proc. 1st Intl. Conference on Software Testing, Verification, and Validation, ICST 2008, Lillehammer, Norway, April 9-11, 2008, IEEE Computer Society, 2008, pages 32-41. The final publication is available from IEEE
Nikolai Kosmatov. All-paths test generation for programs with internal aliases. In Proc. 19th Intl. Symposium on Software Reliability Engineering (ISSRE 2008), Redmond, Seattle, USA, 11-14 November 2008, IEEE Computer Society, 2008, pages 147-156. The final publication is available from IEEE
Bernard Botella, Mickaël Delahaye, Stéphane Hong-Tuan-Ha, Nikolai Kosmatov, Patricia Mouy, Muriel Roger, Nicky Williams. Automating Structural Testing of C Programs: Experience with PathCrawler. In Proc. 4th Intl. Workshop on Automation of Software Test, AST 2009, Vancouver, BC, Canada, May 18-19, 2009, IEEE Computer Society 2009, pages 70-78. The final publication is available from IEEE
Nicky Williams, Muriel Roger. Test Generation Strategies to Measure Worst-Case Execution Time. In Proc. 4th Intl. Workshop on Automation of Software Test, AST 2009, Vancouver, BC, Canada, May 18-19, 2009, IEEE Computer Society, 2009, pages 88-96. The final publication is available from IEEE
Nikolai Kosmatov. On Complexity of All-Paths Test Generation. From Practice to Theory. In Proc Testing: Academic and Industrial Conference - Practice and Research Techniques (TAIC PART 2009), Windsor, United Kingdom, September 2009, IEEE Computer Society Press, 2009, ISBN 978-0-7695-3820-4, pages 144-153. The final publication is available from IEEE
Nicky Williams. Abstract path testing with PathCrawler. ©ACM, 2010. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proc. 5th Workshop on Automation of Software Test (AST'10), Cape Town, South Africa, May 2-8 2010, ACM New York, NY, USA, 2010, ISBN 978-1-60558-970-1, pages 35-42. The final publication is available from ACM
Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand. Combining Static Analysis and Test Generation for C Program Debugging. In Proc. Tests and Proofs, 4th International Conference, TAP 2010, Malaga, Spain, July 1-2, 2010, Springer, Lecture Notes in Computer Science, vol. 6143, 2010, ISBN 978-3-642-13976-5, pages 94-100. The final publication is available at www.springerlink.com.
Nikolai Kosmatov, Bernard Botella, Muriel Roger, Nicky Williams. Online Test Generation with PathCrawler. Tool demo. Best demo award. In Proc. of the 3rd International Workshop on Constraints in Software Testing, Verification, and Analysis (CSTVA 2011), Berlin, Germany, March 2011, IEEE Computer Society Press, 2011, ISBN 978-1-4577-0019-4, pages 316-317. The final publication is available from IEEE
Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand. The SANTE Tool: Value Analysis, Program Slicing and Test Generation for C Program Debugging. In Proc. Tests and Proofs - 5th Intl. Conference, TAP 2011, Zurich, Switzerland, June 30 - July 1, 2011, Springer, Lecture Notes in Computer Science, vol. 6706, 2011, ISBN 978-3-642-21767-8, pages 78-83. The final publication is available at www.springerlink.com.
Nicky Williams, Nikolai Kosmatov. Structural Testing with PathCrawler. Tutorial Synopsis. In Proc. 12th International Conference on Quality Software (QSIC 2012), Xi'an, China, August 27-29, 2012, IEEE Computer Society, 2012, ISBN 978-0-7695-4833-3, pages 289-292. The final publication will be available from IEEE
Omar Chebaro, Nikolai Kosmatov, Alain Giorgetti, Jacques Julliand. Program Slicing Enhances a Verification Technique Combining Static and Dynamic Analysis. © ACM, 2012. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proc. ACM Symposium on Applied Computing, SAC 2012, Riva, Trento, Italy, March 26-30, 2012, ISBN 978-1-4503-0857-1, pages 1284-1291. http://doi.acm.org/10.1145/2245276.2231980
Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger, Omar Chebaro. A Lesson on Structural Testing with PathCrawler-online.com. In Proc. Tests and Proofs - 6th Intl. Conference, TAP 2012, Prague, Czech Republic, May 31 - June 1, 2012, Springer, Lecture Notes in Computer Science, vol. 7305, 2012, ISBN 978-3-642-30472-9, pages 169-175. The final publication is available at www.springerlink.com.
Pascal Cuoq, Florent Kirchner, Nikolai Kosmatov, Virgile Prevosto, Julien Signoles, and Boris Yakobowski. Frama-C: A Program Analysis Perspective. In Proc. 10th Intl. Conference on Software Engineering and Formal Methods (SEFM 2012), Thessaloniki, Greece, October 1-5, 2012, Springer, Lecture Notes in Computer Science, vol. 7504, ISBN 978-3-642-33825-0, pages 233-247. The final publication is available at www.springerlink.com.
Nikolai Kosmatov, Nicky Williams, Bernard Botella, Muriel Roger. Structural Unit Testing as a Service with PathCrawler-online.com. In Proc. 7th IEEE Intl. Symposium on Service Oriented System Engineering (SOSE 2013), San Francisco Bay, USA, March 2013, pages 435-440, ISBN 978-0-7695-4944-6. This is the authors' final version of the work. The final publication is available from IEEE
Omar Chebaro, Pascal Cuoq, Nikolai Kosmatov, Bruno Marre, Anne Pacalet, Nicky Williams, Boris Yakobowski. Behind the Scenes in SANTE: A Combination of Static and Dynamic Analyses. In Automated Software Engineering Journal, vol. 21(1), pages 107-143. 2014. The final publication is available at www.springerlink.com.
Sebastien Bardin, Nikolai Kosmatov, Bruno Marre, David Mentre, Nicky Williams. Test Case Generation with Pathcrawler/LTest: How to Automate an Industrial Testing Process. In Proc. 9th Intl. Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA 2018), Limassol, Cyprus, November 2018, LNCS, vol. 11247, pages 104-120. The final publication is available at www.springerlink.com.
Nicky Williams. Towards exhaustive branch coverage with PathCrawler In Proc. 2nd IEEE/ACM International Conference on Automation of Software Test, AST@ICSE 2021, Madrid, Spain, May 20-21, 2021. IEEE 2021, ISBN 978-1-6654-3567-3
Nicky Williams. Exhaustive branch coverage with TreeFrog (slides) In Proc. 38th ACM/SIGAPP Symposium On Applied Computing, ACM (SIgapp), Mar 2023, Tallinn, Estonia. DOI 10.1145/3555776.3577738 HAL cea-04057580

Guidelines for code upload

Upload the source code and identify the function to be tested

Definition of the test context

List of input parameters and their domains

Definition of the preconditions

Oracle

Coverage criterion

Automatic generation of test-cases

Display of paths and partial paths:

Verdict of the test-case:

You may also want to look at further information:

Status of a path prefix:

Limitations of PathCrawler

What's it for ?

How does it work ?

Publications on the PathCrawler Method and Applications