Commit c091a35c authored by Marek Chalupa's avatar Marek Chalupa
Browse files

tests: add new tests 

Regression tests that I forgot to add.
parent 091f883d

tests/c/array-static-2.c

0 → 100644
+24 −0
Original line number Original line Diff line number Diff line 
#include <assert.h>



// UNSUPPORTED: se

// UNSUPPORTED: kind

// UNSUPPORTED: kindse

// RUN: clang %s -emit-llvm -g -c -o %t.bc

// RUN: rm -rf %t-out

// RUN: timeout 30 sb -out-dir=%t-out %opts %t.bc &>%t.log

// RUN: cat %t.log | FileCheck %s



unsigned int nondet();



unsigned x[100];



int main() {  

  unsigned int k = nondet();

  if (k < 0 || k >= 100)

      return 0;

  assert(x[k] == 0);

  // CHECK-NOT: assertion failed!

  // CHECK-NOT: Error found.

  // CHECK: Found errors: 0

  return 0;

}

tests/c/array-static-false.c

0 → 100644
+22 −0
Original line number Original line Diff line number Diff line 
#include <assert.h>



// UNSUPPORTED: se

// UNSUPPORTED: kind

// UNSUPPORTED: kindse

// RUN: clang %s -emit-llvm -g -c -o %t.bc

// RUN: rm -rf %t-out

// RUN: timeout 30 sb -out-dir=%t-out %opts %t.bc &>%t.log

// RUN: cat %t.log | FileCheck %s



int __VERIFIER_nondet_int();



unsigned x[100];



int main() {  

  int k = __VERIFIER_nondet_int();

  unsigned i = 0;

  assert(x[i] != 0);

  // CHECK: Error found.

  // CHECK: Found errors: 1

  return 0;

}

tests/c/array-static.c

0 → 100644
+20 −0
Original line number Original line Diff line number Diff line 
#include <assert.h>



// RUN: clang %s -emit-llvm -g -c -o %t.bc

// RUN: rm -rf %t-out

// RUN: timeout 30 sb -out-dir=%t-out %opts %t.bc &>%t.log

// RUN: cat %t.log | FileCheck %s



int __VERIFIER_nondet_int();



unsigned x[100];



int main() {  

  int k = __VERIFIER_nondet_int();

  unsigned i = 0;

  assert(x[i] == 0);

  // CHECK-NOT: assertion failed!

  // CHECK-NOT: Error found.

  // CHECK: Found errors: 0

  return 0;

}

tests/c/inde.c

0 → 100644
+28 −0
Original line number Original line Diff line number Diff line 
#include <assert.h>



// UNSUPPORTED: se

// UNSUPPORTED: bse

// UNSUPPORTED: kind

// RUN: clang %s -emit-llvm -g -c -o %t.bc

// RUN: rm -rf %t-out

// RUN: timeout 60 sb -out-dir=%t-out %opts %t.bc &>%t.log

// RUN: cat %t.log | FileCheck %s





unsigned __VERIFIER_nondet_uint(void);

int main()

{

  unsigned int n = __VERIFIER_nondet_uint();

  unsigned int x=n, y=0, z;

  while(x>0)

  {

    //assert(n == x + y);

    x--;

    y++;

  }

  assert(x == 0 && (y == 0 || n == y));

  // CHECK-NOT: assertion failed!

  // CHECK-NOT: Error found.

  // CHECK: Found errors: 0

  return 0;

}