add SV benchmark first folder in for sample testing

src/chooseFile.txt

@@ -1 +1 @@
-/app/code/tests/cFiles/C-master/CmasterFiles.txt
+/app/code/tests/cFiles/SV_benchmark/array-crafted/files.txt

src/experiments/function_calls/data/fcapc_data.csv

@@ -1,4 +1,2 @@
 ,graph_name,fcapc,fcapc_time,naiveMathTime,firstHalfTime
-0,lcs_cfg.lcsbuild,0.229931454098917*1.30793010593**n,2.9640161991119385,2.0807228088378906,0.24903154373168945
-1,cantor_set_cfg.main,2*n/3,0.5628361701965332,0.2335062026977539,0.23923325538635254
-2,lerp_cfg.main,n/3,0.2075512409210205,0.14101839065551758,0.027001380920410156
+0,bAnd1_cfg.bAnd,n/3,8.869931936264038,3.9032583236694336,3.8048882484436035

src/experiments/function_calls/data/getrgfapc_data.csv

@@ -1,3 +1,3 @@
 ,graph_name,getrgfapc,getrgfapc_time,getrgfTime,firstHalfTime,longest for getrgf,longest time,case,gamma
-0,bubble_sort_2_cfg.bubble_sort,0.173947223947289*1.29064880134671**n,0.6065778732299805,0.04432034492492676,0.3974344730377197,gammaTime,0.379,1.0,(-T0*(x**5 + 2*x**4 - 1) + x**3*(x**5 + x**4 - 1))/(x**5 + 2*x**4 - 1)
-1,heap_sort_2_cfg.heapSort,0.0555555555555555*1.0**n*n**2,0.40998339653015137,0.03630542755126953,0.28343868255615234,gammaTime,0.279,1.0,(-T0*(x**6 - 2*x**3 + 1) + x**3*(x**6 - x**3 + 1))/(x**6 - 2*x**3 + 1)
+0,bAnd1_cfg.bAnd,0.333333333333333*1.0**n*n,8.795156240463257,0.6380751132965088,6.468468427658081,gammaTime,5.975,1.0,(-T0*x**3 + T0 - x**3)/(x**3 - 1)
+1,bAnd1_cfg.main,0.000102880658436214*1.0**n*n**5,22.88435387611389,0.5618195533752441,18.45436191558838,gammaTime,18.33,1.0,-(T0*(x**3 - 1)**3*(x**6 - 2*x**3 + 1) + x**15*(2*x + 1))/((x**3 - 1)**3*(x**6 - 2*x**3 + 1))

src/tests/cFiles/SV_benchmark/array-crafted/License.txt

@@ -0,0 +1 @@
+../../LICENSE.Apache-2.0.txt

src/tests/cFiles/SV_benchmark/array-crafted/Makefile

@@ -0,0 +1,3 @@
+LEVEL := ../
+
+include $(LEVEL)/Makefile.config

src/tests/cFiles/SV_benchmark/array-crafted/README.txt

@@ -0,0 +1 @@
+Benchmarks submitted by VeriAbs team, TCS Innovation labs, Pune.

src/tests/cFiles/SV_benchmark/array-crafted/bAnd1.c

@@ -0,0 +1,45 @@
+#define N 100
+#define fun bAnd
+
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern int __VERIFIER_nondet_int();
+
+int bAnd (int x[N])
+{
+  int i;
+  long long res;
+  res = x[0];
+  for (i = 1; i < N; i++) {
+    res = res & x[i];
+  }
+  return res;
+}
+
+int main ()
+{
+  int x[N];
+  int temp;
+  int ret;
+  int ret2;
+  int ret5;
+
+  for (int i = 0; i < N; i++) {
+    x[i] = __VERIFIER_nondet_int();
+  }
+
+  ret = fun(x);
+
+  temp=x[0];x[0] = x[1]; x[1] = temp;
+  ret2 = fun(x);
+  temp=x[0];
+  for(int i =0 ; i<N-1; i++){
+     x[i] = x[i+1];
+  }
+  x[N-1] = temp;
+  ret5 = fun(x);
+
+  if(ret != ret2 || ret !=ret5){ 
+    __VERIFIER_error();
+  }
+  return 1;
+}

src/tests/cFiles/SV_benchmark/array-crafted/bAnd1.i

@@ -0,0 +1,45 @@
+
+
+
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern int __VERIFIER_nondet_int();
+
+int bAnd (int x[100])
+{
+  int i;
+  long long res;
+  res = x[0];
+  for (i = 1; i < 100; i++) {
+    res = res & x[i];
+  }
+  return res;
+}
+
+int main ()
+{
+  int x[100];
+  int temp;
+  int ret;
+  int ret2;
+  int ret5;
+
+  for (int i = 0; i < 100; i++) {
+    x[i] = __VERIFIER_nondet_int();
+  }
+
+  ret = bAnd(x);
+
+  temp=x[0];x[0] = x[1]; x[1] = temp;
+  ret2 = bAnd(x);
+  temp=x[0];
+  for(int i =0 ; i<100 -1; i++){
+     x[i] = x[i+1];
+  }
+  x[100 -1] = temp;
+  ret5 = bAnd(x);
+
+  if(ret != ret2 || ret !=ret5){
+    __VERIFIER_error();
+  }
+  return 1;
+}

src/tests/cFiles/SV_benchmark/array-crafted/bAnd1.yml

@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: bAnd1_true-unreach-call.i
+input_files: 'bAnd1.i'
+
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/coverage-branches.prp
+  - property_file: ../properties/coverage-conditions.prp
+  - property_file: ../properties/coverage-statements.prp

src/tests/cFiles/SV_benchmark/array-crafted/bAnd2.c

@@ -0,0 +1,45 @@
+#define N 1000
+#define fun bAnd
+
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern int __VERIFIER_nondet_int();
+
+int bAnd (int x[N])
+{
+  int i;
+  long long res;
+  res = x[0];
+  for (i = 1; i < N; i++) {
+    res = res & x[i];
+  }
+  return res;
+}
+
+int main ()
+{
+  int x[N];
+  int temp;
+  int ret;
+  int ret2;
+  int ret5;
+
+  for (int i = 0; i < N; i++) {
+    x[i] = __VERIFIER_nondet_int();
+  }
+
+  ret = fun(x);
+
+  temp=x[0];x[0] = x[1]; x[1] = temp;
+  ret2 = fun(x);
+  temp=x[0];
+  for(int i =0 ; i<N-1; i++){
+     x[i] = x[i+1];
+  }
+  x[N-1] = temp;
+  ret5 = fun(x);
+
+  if(ret != ret2 || ret !=ret5){ 
+    __VERIFIER_error();
+  }
+  return 1;
+}

src/tests/cFiles/SV_benchmark/array-crafted/bAnd2.i

@@ -0,0 +1,45 @@
+
+
+
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern int __VERIFIER_nondet_int();
+
+int bAnd (int x[1000])
+{
+  int i;
+  long long res;
+  res = x[0];
+  for (i = 1; i < 1000; i++) {
+    res = res & x[i];
+  }
+  return res;
+}
+
+int main ()
+{
+  int x[1000];
+  int temp;
+  int ret;
+  int ret2;
+  int ret5;
+
+  for (int i = 0; i < 1000; i++) {
+    x[i] = __VERIFIER_nondet_int();
+  }
+
+  ret = bAnd(x);
+
+  temp=x[0];x[0] = x[1]; x[1] = temp;
+  ret2 = bAnd(x);
+  temp=x[0];
+  for(int i =0 ; i<1000 -1; i++){
+     x[i] = x[i+1];
+  }
+  x[1000 -1] = temp;
+  ret5 = bAnd(x);
+
+  if(ret != ret2 || ret !=ret5){
+    __VERIFIER_error();
+  }
+  return 1;
+}

src/tests/cFiles/SV_benchmark/array-crafted/bAnd2.yml

@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: bAnd2_true-unreach-call.i
+input_files: 'bAnd2.i'
+
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/coverage-branches.prp
+  - property_file: ../properties/coverage-conditions.prp
+  - property_file: ../properties/coverage-statements.prp

src/tests/cFiles/SV_benchmark/array-crafted/bAnd3.c

@@ -0,0 +1,45 @@
+#define N 10000
+#define fun bAnd
+
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern int __VERIFIER_nondet_int();
+
+int bAnd (int x[N])
+{
+  int i;
+  long long res;
+  res = x[0];
+  for (i = 1; i < N; i++) {
+    res = res & x[i];
+  }
+  return res;
+}
+
+int main ()
+{
+  int x[N];
+  int temp;
+  int ret;
+  int ret2;
+  int ret5;
+
+  for (int i = 0; i < N; i++) {
+    x[i] = __VERIFIER_nondet_int();
+  }
+
+  ret = fun(x);
+
+  temp=x[0];x[0] = x[1]; x[1] = temp;
+  ret2 = fun(x);
+  temp=x[0];
+  for(int i =0 ; i<N-1; i++){
+     x[i] = x[i+1];
+  }
+  x[N-1] = temp;
+  ret5 = fun(x);
+
+  if(ret != ret2 || ret !=ret5){ 
+    __VERIFIER_error();
+  }
+  return 1;
+}

src/tests/cFiles/SV_benchmark/array-crafted/bAnd3.i

@@ -0,0 +1,45 @@
+
+
+
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern int __VERIFIER_nondet_int();
+
+int bAnd (int x[10000])
+{
+  int i;
+  long long res;
+  res = x[0];
+  for (i = 1; i < 10000; i++) {
+    res = res & x[i];
+  }
+  return res;
+}
+
+int main ()
+{
+  int x[10000];
+  int temp;
+  int ret;
+  int ret2;
+  int ret5;
+
+  for (int i = 0; i < 10000; i++) {
+    x[i] = __VERIFIER_nondet_int();
+  }
+
+  ret = bAnd(x);
+
+  temp=x[0];x[0] = x[1]; x[1] = temp;
+  ret2 = bAnd(x);
+  temp=x[0];
+  for(int i =0 ; i<10000 -1; i++){
+     x[i] = x[i+1];
+  }
+  x[10000 -1] = temp;
+  ret5 = bAnd(x);
+
+  if(ret != ret2 || ret !=ret5){
+    __VERIFIER_error();
+  }
+  return 1;
+}

src/tests/cFiles/SV_benchmark/array-crafted/bAnd3.yml

@@ -0,0 +1,11 @@
+format_version: '1.0'
+
+# old file name: bAnd3_true-unreach-call.i
+input_files: 'bAnd3.i'
+
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/coverage-branches.prp
+  - property_file: ../properties/coverage-conditions.prp
+  - property_file: ../properties/coverage-statements.prp

src/tests/cFiles/SV_benchmark/array-crafted/bAnd4.c

@@ -0,0 +1,45 @@
+#define N 100000
+#define fun bAnd
+
+extern void __VERIFIER_error() __attribute__ ((__noreturn__));
+extern int __VERIFIER_nondet_int();
+
+int bAnd (int x[N])
+{
+  int i;
+  long long res;
+  res = x[0];
+  for (i = 1; i < N; i++) {
+    res = res & x[i];
+  }
+  return res;
+}
+
+int main ()
+{
+  int x[N];
+  int temp;
+  int ret;
+  int ret2;
+  int ret5;
+
+  for (int i = 0; i < N; i++) {
+    x[i] = __VERIFIER_nondet_int();
+  }
+
+  ret = fun(x);
+
+  temp=x[0];x[0] = x[1]; x[1] = temp;
+  ret2 = fun(x);
+  temp=x[0];
+  for(int i =0 ; i<N-1; i++){
+     x[i] = x[i+1];
+  }
+  x[N-1] = temp;
+  ret5 = fun(x);
+
+  if(ret != ret2 || ret !=ret5){ 
+    __VERIFIER_error();
+  }
+  return 1;
+}