diff --git a/regression/goto-analyzer/sensitivity-test-common-files/array_of_array_sensitivity_tests.c b/regression/goto-analyzer/sensitivity-test-common-files/array_of_array_sensitivity_tests.c new file mode 100644 index 00000000000..63af187ade2 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-common-files/array_of_array_sensitivity_tests.c @@ -0,0 +1,150 @@ +#include + +int main(int argc, char *argv[]) +{ + // A uniform constant array + int a[3][3]={{0, 0, 0}, {0, 0, 0}, {0, 0, 0}}; + // A non-uniform constant array + int b[3][3]={{0, 1, 2}, {3, 4, 5}, {6, 7, 8}}; + + // Test if we can represent uniform constant arrays + assert(a[1][2]==0); + assert(a[1][2]==1); + + // Test if we can represent constant arrays which aren't uniform + assert(b[1][2]==5); + assert(b[1][2]==0); + + // Test alternative syntax for accessing an array value + assert(*(b[1]+2)==5); + assert(*(b[1]+2)==0); + assert((*(b+1))[2]==5); + assert((*(b+1))[2]==0); + assert(*(*(b+1)+2)==5); + assert(*(*(b+1)+2)==0); + assert(1[b][2]==5); + assert(1[b][2]==0); + assert(*(1[b]+2)==5); + assert(*(1[b]+2)==0); + assert((*(1+b))[2]==5); + assert((*(1+b))[2]==0); + assert(*(*(1+b)+2)==5); + assert(*(*(1+b)+2)==0); + assert(2[1[b]]==5); + assert(2[1[b]]==0); + assert(*(2+1[b])==5); + assert(*(2+1[b])==0); + assert(*(2+*(1+b))==5); + assert(*(2+*(1+b))==0); + + // Test how well we can deal with merging for an array value when there is one + // possible value + if(argc>2) + { + a[0][1]=0; + } + assert(a[0][1]==0); + assert(a[0][1]==1); + assert(a[0][2]==0); + + // Test how well we can deal with merging for an array value when there are + // two possible values + if(argc>2) + { + b[0][1]=2; + } + assert(b[0][1]==2); + assert(b[0][1]==3); + assert(b[0][2]==2); + + // Reset this change to ensure tests later work as expected + b[0][1]=1; + + // The variables i, j and k will be used as indexes into arrays of size 3. + // They all require merging paths in the CFG. For i there is only one value on + // both paths, which is a valid index. The rest can each take two different + // values. For j both of these values are valid indexes. For k one is and one + // isn't. + int i=0; + int j=0; + int k=0; + if(argc>3) + { + i=0; + j=1; + k=100; + } + + // Test how well we can deal with merging for an index on a uniform array when + // the index has one possible value + assert(a[i][1]==0); + assert(a[i][1]==1); + assert(a[1][i]==0); + assert(a[1][i]==1); + assert(a[i][i]==0); + assert(a[i][i]==1); + + // Test how well we can deal with merging for an index on a uniform array when + // the index has two possible values + assert(a[j][1]==0); + assert(a[j][1]==1); + assert(a[1][j]==0); + assert(a[1][j]==1); + assert(a[j][j]==0); + assert(a[j][j]==1); + + // Test how well we can deal with merging for an index on a non-uniform array + + assert(b[i][1]==1); + assert(b[i][1]==11); + assert(b[1][i]==3); + assert(b[1][i]==11); + assert(b[i][i]==0); + assert(b[i][i]==11); + + // Test how well we can deal with merging for an index on a non-uniform array + assert(b[j][1]==1); + assert(b[j][1]==11); + assert(b[1][j]==3); + assert(b[1][j]==11); + assert(b[j][j]==0); + assert(b[j][j]==11); + + // Test how we deal with reading off the end of an array + assert(a[100][0]==0); + assert(a[0][100]==0); + + // Test how we deal with writing off the end of an array + int c=0; + a[100][0]=1; + assert(c==0); + c=0; + a[0][100]=1; + assert(c==0); + + // Test how we deal with merging for an index with one possible value when + // writing to an array + int ei[3][3]={{0, 0, 0}, {0, 0, 0}, {0, 0, 0}}; + ei[i][1]=1; + assert(ei[0][1]==1); + assert(ei[0][1]==0); + assert(ei[2][1]==0); + assert(ei[2][1]==1); + + // Test how we deal with merging for an index with two possible values when + // writing to an array + int ej[3][3]={{0, 0, 0}, {0, 0, 0}, {0, 0, 0}}; + ej[j][1]=1; + assert(ej[0][1]==0); + assert(ej[2][1]==0); + + // Test how we deal with merging for an index with two possible values when + // it means writing to an array element that may be out of bounds + int ek[3][3]={{0, 0, 0}, {0, 0, 0}, {0, 0, 0}}; + c=0; + ek[k][1]=1; + assert(ek[0][1]==0); + assert(c==0); + + return 0; +} diff --git a/regression/goto-analyzer/sensitivity-test-common-files/array_of_pointer_sensitivity_tests.c b/regression/goto-analyzer/sensitivity-test-common-files/array_of_pointer_sensitivity_tests.c new file mode 100644 index 00000000000..907fc4180ad --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-common-files/array_of_pointer_sensitivity_tests.c @@ -0,0 +1,156 @@ +#include + +int main(int argc, char *argv[]) +{ + // Test how well we can represent arrays of pointers + int a0=0; + int a1=1; + int a2=2; + int a3=3; + int b0=10; + int b1=11; + int b2=12; + int b3=13; + int c0=20; + int c1=21; + int c2=22; + int c3=23; + int d0=30; + int d1=31; + int d2=32; + int d3=33; + // A uniform constant array + int *a[3]={&a0, &a0, &a0}; + // A non-uniform constant array + int *b[3]={&b0, &b1, &b2}; + + // Test if we can represent uniform constant arrays + assert(a[1]==&a0); + assert(a[1]==&a3); + assert(*a[1]==0); + assert(*a[1]==3); + + // Test if we can represent constant arrays which aren't uniform + assert(b[1]==&b1); + assert(b[1]==&b3); + assert(*b[1]==11); + assert(*b[1]==13); + + // Test alternative syntax for accessing an array value + assert(*(b+1)==&b1); + assert(*(b+1)==&b3); + assert(*(1+b)==&b1); + assert(*(1+b)==&b3); + assert(1[b]==&b1); + assert(1[b]==&b3); + assert(**(b+1)==11); + assert(**(b+1)==13); + assert(**(1+b)==11); + assert(**(1+b)==13); + assert(*1[b]==11); + assert(*1[b]==13); + + // c and d are arrays whose values requiring merging paths in the CFG. For + // c[0] there is only one possibility after merging and for d[0] there are + // two. + int *c[3]={&c0, &c1, &c2}; + int *d[3]={&d0, &d1, &d2}; + if(argc>2) + { + c[0]=&c3; + d[0]=&d3; + } + + // Test how well we can deal with merging for an array value + assert(c[0]==&c0); + assert(c[0]==&c3); + assert(d[0]==&d0); + assert(d[0]==&d3); + assert(*c[0]==20); + assert(*c[0]==23); + assert(*d[0]==30); + assert(*d[0]==33); + + // The variables i, j and k will be used as indexes into arrays of size 3. + // They all require merging paths in the CFG. For i there is only one value on + // both paths, which is a valid index. The rest can each take two different + // values. For j both of these values are valid indexes. For k one is and one + // isn't. + int i=0; + int j=0; + int k=0; + if(argc>3) + { + i=0; + j=1; + k=100; + } + + // Test how well we can deal with merging for an index on a uniform array + assert(a[i]==&a0); + assert(a[i]==&a3); + assert(a[j]==&a0); + assert(a[j]==&a3); + assert(*a[i]==0); + assert(*a[i]==3); + assert(*a[j]==0); + assert(*a[j]==3); + + // Test how well we can deal with merging for an index on a non-uniform array + assert(b[i]==&b0); + assert(b[i]==&b1); + assert(b[j]==&b0); + assert(b[j]==&b3); + assert(*b[i]==10); + assert(*b[i]==11); + assert(*b[j]==10); + assert(*b[j]==13); + + // Test how we deal with reading off the end of an array + assert(a[100]==&a2); + assert(*a[100]==2); + + // Test how we deal with writing off the end of an array + a[100]=&a2; + assert(b[1]==&b1); + assert(*b[1]==11); + + // Test how we deal with merging for an index with one possible value when + // writing to an array + int ei0=40; + int ei1=41; + int *ei[3]={&ei0, &ei0, &ei0}; + ei[i]=&ei1; + assert(ei[0]==&ei1); + assert(ei[0]==&ei0); + assert(ei[2]==&ei0); + assert(ei[2]==&ei1); + assert(*ei[0]==41); + assert(*ei[0]==40); + assert(*ei[2]==40); + assert(*ei[2]==41); + + // Test how we deal with merging for an index with two possible values when + // writing to an array + int ej0=50; + int ej1=51; + int *ej[3]={&ej0, &ej0, &ej0}; + ej[j]=&ej1; + assert(ej[0]==&ej0); + assert(ej[2]==&ej0); + assert(ej[2]==&ej1); + assert(*ej[0]==50); + assert(*ej[2]==50); + assert(*ej[2]==51); + + // Test how we deal with merging for an index with two possible values when + // it means writing to an array element that may be out of bounds + int ek0=60; + int ek1=61; + int *ek[3]={&ek0, &ek0, &ek0}; + ek[k]=&ek1; + assert(ek[0]==&ek0); + assert(*ek[0]==60); + + return 0; +} diff --git a/regression/goto-analyzer/sensitivity-test-common-files/array_sensitivity_tests.c b/regression/goto-analyzer/sensitivity-test-common-files/array_sensitivity_tests.c new file mode 100644 index 00000000000..68bace194c8 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-common-files/array_sensitivity_tests.c @@ -0,0 +1,101 @@ +#include + +int main(int argc, char *argv[]) +{ + // A uniform constant array + int a[3]={0, 0, 0}; + // A non-uniform constant array + int b[3]={1, 0, 0}; + + // Test if we can represent uniform constant arrays + assert(a[1]==0); + assert(a[1]==1); + + // Test if we can represent constant arrays which aren't uniform + assert(b[1]==0); + assert(b[1]==1); + + // Test alternative syntax for accessing an array value + assert(*(b+1)==0); + assert(*(b+1)==1); + assert(*(1+b)==0); + assert(*(1+b)==1); + assert(1[b]==0); + assert(1[b]==1); + + // c and d are arrays whose values requiring merging paths in the CFG. For + // c[0] there is only one possibility after merging and for d[0] there are + // two. + int c[3]={0, 0, 0}; + int d[3]={0, 0, 0}; + if(argc>2) + { + c[0]=0; + d[0]=1; + } + + // Test how well we can deal with merging for an array value + assert(c[0]==0); + assert(c[0]==1); + assert(d[0]==0); + assert(d[0]==2); + assert(d[1]==0); + + // The variables i, j and k will be used as indexes into arrays of size 3. + // They all require merging paths in the CFG. For i there is only one value on + // both paths, which is a valid index. The rest can each take two different + // values. For j both of these values are valid indexes. For k one is and one + // isn't. + int i=0; + int j=0; + int k=0; + if(argc>3) + { + i=0; + j=1; + k=100; + } + + // Test how well we can deal with merging for an index on a uniform array + assert(a[i]==0); + assert(a[i]==1); + assert(a[j]==0); + assert(a[j]==1); + + // Test how well we can deal with merging for an index on a non-uniform array + assert(b[i]==1); + assert(b[i]==0); + assert(b[j]==0); + assert(b[j]==1); + + // Test how we deal with reading off the end of an array + assert(a[100]==0); + + // Test how we deal with writing off the end of an array + a[100]=1; + assert(b[1]==0); + + // Test how we deal with merging for an index with one possible value when + // writing to an array + int ei[3]={0, 0, 0}; + ei[i]=1; + assert(ei[0]==1); + assert(ei[0]==0); + assert(ei[2]==0); + assert(ei[2]==1); + + // Test how we deal with merging for an index with two possible values when + // writing to an array + int ej[3]={0, 0, 0}; + ej[j]=1; + assert(ej[0]==0); + assert(ej[2]==0); + + // Test how we deal with merging for an index with two possible values when + // it means writing to an array element that may be out of bounds + int ek[3]={0, 0, 0}; + ek[k]=1; + assert(ek[0]==0); + + return 0; +} diff --git a/regression/goto-analyzer/sensitivity-test-common-files/char_sensitivity_tests.c b/regression/goto-analyzer/sensitivity-test-common-files/char_sensitivity_tests.c new file mode 100644 index 00000000000..9e87454b68e --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-common-files/char_sensitivity_tests.c @@ -0,0 +1,10 @@ +#include + +int main(int argc, char *argv[]) +{ + // Test if we can represent constant chars + char x='a'; + assert(x=='a'); + assert(x=='b'); + return 0; +} diff --git a/regression/goto-analyzer/sensitivity-test-common-files/float_sensitivity_tests.c b/regression/goto-analyzer/sensitivity-test-common-files/float_sensitivity_tests.c new file mode 100644 index 00000000000..1f73fae4a6c --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-common-files/float_sensitivity_tests.c @@ -0,0 +1,10 @@ +#include + +int main(int argc, char *argv[]) +{ + // Test if we can represent constant floats + float x=0.0; + assert(x==0.0); + assert(x==1.0); + return 0; +} diff --git a/regression/goto-analyzer/sensitivity-test-common-files/int_sensitivity_tests.c b/regression/goto-analyzer/sensitivity-test-common-files/int_sensitivity_tests.c new file mode 100644 index 00000000000..ab4265a051f --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-common-files/int_sensitivity_tests.c @@ -0,0 +1,55 @@ +#include + +int main(int argc, char *argv[]) +{ + // Test how well we can represent ints, and also that the transformers are + // working correctly. + int x=0; + int y=0; + if(argc>2) + { + y=1; + } + assert(x==0); + assert(x==1); + assert(x==y); + + assert(x<1); + assert(x<-1); + assert(x-1); + assert(x>1); + assert(x>y); + + assert(x!=1); + assert(x!=0); + assert(x!=y); + + assert(!(x==1)); + assert(!(x==0)); + assert(!(x==y)); + + // Test how well we can represent an int when it has more than one possible + // value + assert(y<2); + assert(y>2); + assert(y==1); + + // Try copying a variable and then modifying the original + int z=x; + x=10; + assert(z==0); + assert(z==10); + + // Test how we treat assertions in unreachable code + x=0; + if(0) + { + assert(x==0); + assert(x==1); + assert(y==0); + } + + return 0; +} diff --git a/regression/goto-analyzer/sensitivity-test-common-files/pointer_sensitivity_tests.c b/regression/goto-analyzer/sensitivity-test-common-files/pointer_sensitivity_tests.c new file mode 100644 index 00000000000..be328fa4a5d --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-common-files/pointer_sensitivity_tests.c @@ -0,0 +1,53 @@ +#include + +int main(int argc, char *argv[]) +{ + // Test how well we can represent pointers + // Basic use of addresses + int a=0; + int b=0; + int c=0; + int *x=&a; + int *x2=&a; + int *y=&b; + assert(x==&a); + assert(x==&b); + assert(x==x2); + assert(x==y); + + // Reading from a dereferenced pointer + assert(*x==0); + assert(*x==1); + + // Modify the referenced value and access it through the pointer again + a=1; + assert(*x==1); + assert(*x==0); + + // Writing to a dereferenced pointer + *x=2; + assert(a==2); + assert(a==0); + + // Conditionally reassign the pointer, but to the same value + if(argc>2) + { + x=&a; + } + assert(x==&a); + + // Conditionally reassign the pointer, to a different value this time + if(argc>3) + { + x=&b; + } + else + { + x=&c; + } + assert(*x==0); + assert(x==&a); + assert(x==&b); + + return 0; +} diff --git a/regression/goto-analyzer/sensitivity-test-common-files/pointer_to_array_sensitivity_tests.c b/regression/goto-analyzer/sensitivity-test-common-files/pointer_to_array_sensitivity_tests.c new file mode 100644 index 00000000000..db9fe720e15 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-common-files/pointer_to_array_sensitivity_tests.c @@ -0,0 +1,59 @@ +#include +#include + +int main(int argc, char *argv[]) +{ + // Test reading from an array using a pointer + int a[3]={1, 2, 3}; + int *p=a; + assert(p==&a[0]); + assert(*p==1); + + // Test pointer arithmetic + int *q=&a[1]; + assert(q==p+1); + assert(*q==2); + + // Test pointer diffs + ptrdiff_t x=1; + assert(q-p==x); + + // Test writing into an array using a pointer + *q=4; + assert(a[1]==4); + a[1]=2; + + // We now explore pointers and indexes each with more than one possible value + int *r=&a[1]; + int b[3]={0, 0, 0}; + int *s=&b[1]; + int i=1; + if (argc>2) + { + r=&a[2]; + s=&b[2]; + i=2; + } + + // Test reading from an array using a pointer with more than one possible + // value + assert(*r==2); + assert(*r==1); + assert(*s==0); + assert(*s==1); + + // Test pointer arithmetic with an unknown index + int *t=&a[i]; + assert(t==p+i); + + // Test pointer diffs with an unknown index + ptrdiff_t y=i; + assert(t-p==y); + + // Test writing into an array using a pointer with an unknown index + *r=5; + assert(a[i]==5); + assert(a[1]==5); + + return 0; +} diff --git a/regression/goto-analyzer/sensitivity-test-common-files/pointer_to_pointer_sensitivity_tests.c b/regression/goto-analyzer/sensitivity-test-common-files/pointer_to_pointer_sensitivity_tests.c new file mode 100644 index 00000000000..ee29a7059db --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-common-files/pointer_to_pointer_sensitivity_tests.c @@ -0,0 +1,24 @@ +#include + +int main(int argc, char *argv[]) +{ + // Test how well we can represent pointers to pointers + // Basic use of addresses + int a=0; + int *p=&a; + int **x=&p; + + // Reading from a pointer to a pointer that's been dereferenced twice + assert(**x==0); + assert(**x==1); + a=1; + assert(**x==1); + assert(**x==0); + + // Writing to a pointer to a pointer that's been dereferenced twice + **x=2; + assert(a==2); + assert(a==1); + + return 0; +} diff --git a/regression/goto-analyzer/sensitivity-test-common-files/pointer_to_struct_sensitivity_tests.c b/regression/goto-analyzer/sensitivity-test-common-files/pointer_to_struct_sensitivity_tests.c new file mode 100644 index 00000000000..e0092afae4a --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-common-files/pointer_to_struct_sensitivity_tests.c @@ -0,0 +1,28 @@ +#include + +int main(int argc, char *argv[]) +{ + // Test how well we can represent pointers to structs + struct int_float + { + int a; + float b; + }; + struct int_float x={0, 1.0}; + x.a=0; + x.b=1.0; + struct int_float *p=&x; + assert((*p).a==0); + assert((*p).a==1); + + // Test alternative syntax + assert(p->a==0); + assert(p->a==1); + + // Test writing to the struct through the pointer + p->b=2.0; + assert(p->b==2.0); + assert(p->b==1.0); + + return 0; +} diff --git a/regression/goto-analyzer/sensitivity-test-common-files/struct_of_array_sensitivity_tests.c b/regression/goto-analyzer/sensitivity-test-common-files/struct_of_array_sensitivity_tests.c new file mode 100644 index 00000000000..d5924b71ed7 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-common-files/struct_of_array_sensitivity_tests.c @@ -0,0 +1,58 @@ +#include + +int main(int argc, char *argv[]) +{ + // Test how well we can represent structs + struct int_array_float_array + { + int a[3]; + float b[3]; + }; + struct int_array_float_array x={{0, 1, 2}, {3.0f, 4.0f, 5.0f}}; + x.a[0]=0; + x.a[1]=1; + x.a[2]=2; + x.b[0]=3.0f; + x.b[1]=4.0f; + x.b[2]=5.0f; + assert(x.a[0]==0); + assert(*(x.a+0)==0); + assert(*(0+x.a)==0); + assert(0[x.a]==0); + + // Test merging when there is only one value on both paths + if(argc>2) + { + x.a[0]=0; + } + assert(x.a[0]==0); + assert(x.a[1]==1); + assert(x.b[0]==3.0f); + + // Test merging when there is one value for a and two values for b, to test if + // we are representing them separately + if(argc>3) + { + x.a[0]=0; + x.b[2]=15.0f; + } + assert(x.a[0]==0); + assert(x.a[1]==1); + assert(x.b[2]>0.0f); + assert(x.b[2]==15.0f); + assert(x.b[2]==1.0f); + assert(x.b[0]==3.0f); + + // Test merging when there are two values for a and b + if(argc>4) + { + x.a[0]=11; + x.b[2]=25.0f; + } + assert(x.a[0]<12); + assert(x.a[0]>2); + assert(x.a[0]==0); + assert(x.a[1]==1); + + return 0; +} diff --git a/regression/goto-analyzer/sensitivity-test-common-files/struct_of_pointer_sensitivity_tests.c b/regression/goto-analyzer/sensitivity-test-common-files/struct_of_pointer_sensitivity_tests.c new file mode 100644 index 00000000000..3cde8011c2b --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-common-files/struct_of_pointer_sensitivity_tests.c @@ -0,0 +1,71 @@ +#include + +int main(int argc, char *argv[]) +{ + // Test how well we can represent structs of pointers + int a1=0; + int a2=1; + int a3=2; + float b1=10.0f; + float b2=11.0f; + float b3=12.0f; + float b4=13.0f; + struct int_float + { + int *a; + float *b; + }; + struct int_float x; + x.a=&a1; + x.b=&b1; + assert(x.a==&a1); + assert(x.a==&a2); + assert(x.b==&b1); + assert(x.b==&b2); + assert(*x.a==0); + assert(*x.a==100); + assert(*x.b==10.0f); + assert(*x.b==110.0f); + + // Test merging when there is only one value on both paths + if(argc>2) + { + x.a=&a1; + x.b=&b1; + } + assert(x.a==&a1); + assert(x.a==&a2); + assert(*x.a==0); + assert(*x.a==100); + + // Test merging when there is one value for a and two values for b, to test if + // we are representing them separately + if(argc>3) + { + x.a=&a1; + x.b=&b2; + } + assert(x.a==&a1); + assert(x.b==&b2); + assert(x.b==&b3); + assert(*x.a==0); + assert(*x.b==11.0f); + assert(*x.b==12.0f); + + // Test merging when there are two values for a and b + if(argc>4) + { + x.a=&a2; + x.b=&b3; + } + assert(x.a==&a2); + assert(x.a==&a3); + assert(x.b==&b3); + assert(x.b==&b4); + assert(*x.a==1); + assert(*x.a==2); + assert(*x.b==12.0f); + assert(*x.b==13.0f); + + return 0; +} diff --git a/regression/goto-analyzer/sensitivity-test-common-files/struct_of_struct_sensitivity_tests.c b/regression/goto-analyzer/sensitivity-test-common-files/struct_of_struct_sensitivity_tests.c new file mode 100644 index 00000000000..ac6a32a0086 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-common-files/struct_of_struct_sensitivity_tests.c @@ -0,0 +1,55 @@ +#include + +int main(int argc, char *argv[]) +{ + // Test how well we can represent structs of structs + struct int_float + { + int a; + float b; + }; + struct two_int_floats + { + struct int_float s1; + struct int_float s2; + }; + struct two_int_floats x; + x.s1.a=0; + x.s1.b=1.0; + x.s2.a=2; + x.s2.b=3.0f; + assert(x.s1.a==0); + assert(x.s2.b==3.0f); + + // Test merging when there is only one value on both paths + if(argc>2) + { + x.s1.a=0; + } + assert(x.s1.a==0); + assert(x.s1.a==10); + + // Test merging when there is one value for s1 and two values for s2, to test + // if we are representing them separately + if(argc>3) + { + x.s1.b=1.0f; + x.s2.b=13.0f; + } + assert(x.s1.b==1.0f); + assert(x.s2.b==3.0f); + assert(x.s2.b==0.0f); + + // Test merging when there are two values for s1 and s2 + if(argc>4) + { + x.s1.a=20; + x.s2.a=22; + } + assert(x.s1.a==20); + assert(x.s1.a<30); + assert(x.s2.a==22); + assert(x.s2.a<30); + + return 0; +} diff --git a/regression/goto-analyzer/sensitivity-test-common-files/struct_sensitivity_tests.c b/regression/goto-analyzer/sensitivity-test-common-files/struct_sensitivity_tests.c new file mode 100644 index 00000000000..a4ad229e34c --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-common-files/struct_sensitivity_tests.c @@ -0,0 +1,47 @@ +#include + +int main(int argc, char *argv[]) +{ + // Test how well we can represent structs + struct int_float + { + int a; + float b; + }; + struct int_float x={0, 1.0f}; + x.a=0; + x.b=1.0f; + assert(x.a==0); + assert(x.a==1); + + // Test merging when there is only one value on both paths + if(argc>2) + { + x.a=0; + x.b=1.0f; + } + assert(x.a==0); + + // Test merging when there is one value for a and two values for b, to test if + // we are representing them separately + if(argc>3) + { + x.a=0; + x.b=2.0f; + } + assert(x.a==0); + assert(x.b>0.0f); + assert(x.b==1.0f); + + // Test merging when there are two values for a and b + if(argc>4) + { + x.a=1; + x.b=2.0f; + } + assert(x.a<2); + assert(x.a>2); + assert(x.a==1); + + return 0; +} diff --git a/regression/goto-analyzer/sensitivity-test-constants-array-of-constants-array/sensitivity_test_constants_array_of_constants_array.c b/regression/goto-analyzer/sensitivity-test-constants-array-of-constants-array/sensitivity_test_constants_array_of_constants_array.c new file mode 100644 index 00000000000..103849f7a32 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-array-of-constants-array/sensitivity_test_constants_array_of_constants_array.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/array_of_array_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-array-of-constants-array/test.desc b/regression/goto-analyzer/sensitivity-test-constants-array-of-constants-array/test.desc new file mode 100644 index 00000000000..c8db44a2c09 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-array-of-constants-array/test.desc @@ -0,0 +1,73 @@ +FUTURE +sensitivity_test_constants_array_of_constants_array.c +--variable --arrays --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion a\[1\]\[2\]==0: Success$ +^\[main.assertion.2\] .* assertion a\[1\]\[2\]==1: Failure \(if reachable\)$ +^\[main.assertion.3\] .* assertion b\[1\]\[2\]==5: Success$ +^\[main.assertion.4\] .* assertion b\[1\]\[2\]==0: Failure \(if reachable\)$ +^\[main.assertion.5\] .* assertion \*\(b\[1\]\+2\)==5: Success$ +^\[main.assertion.6\] .* assertion \*\(b\[1\]\+2\)==0: Failure \(if reachable\)$ +^\[main.assertion.7\] .* assertion \(\*\(b\+1\)\)\[2\]==5: Success$ +^\[main.assertion.8\] .* assertion \(\*\(b\+1\)\)\[2\]==0: Failure \(if reachable\)$ +^\[main.assertion.9\] .* assertion \*\(\*\(b\+1\)\+2\)==5: Success$ +^\[main.assertion.10\] .* assertion \*\(\*\(b\+1\)\+2\)==0: Failure \(if reachable\)$ +^\[main.assertion.11\] .* assertion 1\[b\]\[2\]==5: Success$ +^\[main.assertion.12\] .* assertion 1\[b\]\[2\]==0: Failure \(if reachable\)$ +^\[main.assertion.13\] .* assertion \*\(1\[b\]\+2\)==5: Success$ +^\[main.assertion.14\] .* assertion \*\(1\[b\]\+2\)==0: Failure \(if reachable\)$ +^\[main.assertion.15\] .* assertion \(\*\(1\+b\)\)\[2\]==5: Unknown$ +^\[main.assertion.16\] .* assertion \(\*\(1\+b\)\)\[2\]==0: Unknown$ +^\[main.assertion.17\] .* assertion \*\(\*\(1\+b\)\+2\)==5: Unknown$ +^\[main.assertion.18\] .* assertion \*\(\*\(1\+b\)\+2\)==0: Unknown$ +^\[main.assertion.19\] .* assertion 2\[1\[b\]\]==5: Success$ +^\[main.assertion.20\] .* assertion 2\[1\[b\]\]==0: Failure \(if reachable\)$ +^\[main.assertion.21\] .* assertion \*\(2\+1\[b\]\)==5: Unknown$ +^\[main.assertion.22\] .* assertion \*\(2\+1\[b\]\)==0: Unknown$ +^\[main.assertion.23\] .* assertion \*\(2\+\*\(1\+b\)\)==5: Unknown$ +^\[main.assertion.24\] .* assertion \*\(2\+\*\(1\+b\)\)==0: Unknown$ +^\[main.assertion.25\] .* assertion a\[0\]\[1\]==0: Success$ +^\[main.assertion.26\] .* assertion a\[0\]\[1\]==1: Failure \(if reachable\)$ +^\[main.assertion.27\] .* assertion a\[0\]\[2\]==0: Success$ +^\[main.assertion.28\] .* assertion b\[0\]\[1\]==2: Unknown$ +^\[main.assertion.29\] .* assertion b\[0\]\[1\]==3: Unknown$ +^\[main.assertion.30\] .* assertion b\[0\]\[2\]==2: Success$ +^\[main.assertion.31\] .* assertion a\[i\]\[1\]==0: Success$ +^\[main.assertion.32\] .* assertion a\[i\]\[1\]==1: Failure \(if reachable\)$ +^\[main.assertion.33\] .* assertion a\[1\]\[i\]==0: Success$ +^\[main.assertion.34\] .* assertion a\[1\]\[i\]==1: Failure \(if reachable\)$ +^\[main.assertion.35\] .* assertion a\[i\]\[i\]==0: Success$ +^\[main.assertion.36\] .* assertion a\[i\]\[i\]==1: Failure \(if reachable\)$ +^\[main.assertion.37\] .* assertion a\[j\]\[1\]==0: Unknown$ +^\[main.assertion.38\] .* assertion a\[j\]\[1\]==1: Unknown$ +^\[main.assertion.39\] .* assertion a\[1\]\[j\]==0: Unknown$ +^\[main.assertion.40\] .* assertion a\[1\]\[j\]==1: Unknown$ +^\[main.assertion.41\] .* assertion a\[j\]\[j\]==0: Unknown$ +^\[main.assertion.42\] .* assertion a\[j\]\[j\]==1: Unknown$ +^\[main.assertion.43\] .* assertion b\[i\]\[1\]==1: Success$ +^\[main.assertion.44\] .* assertion b\[i\]\[1\]==11: Failure \(if reachable\)$ +^\[main.assertion.45\] .* assertion b\[1\]\[i\]==3: Success$ +^\[main.assertion.46\] .* assertion b\[1\]\[i\]==11: Failure \(if reachable\)$ +^\[main.assertion.47\] .* assertion b\[i\]\[i\]==0: Success$ +^\[main.assertion.48\] .* assertion b\[i\]\[i\]==11: Failure \(if reachable\)$ +^\[main.assertion.49\] .* assertion b\[j\]\[1\]==1: Unknown$ +^\[main.assertion.50\] .* assertion b\[j\]\[1\]==11: Unknown$ +^\[main.assertion.51\] .* assertion b\[1\]\[j\]==3: Unknown$ +^\[main.assertion.52\] .* assertion b\[1\]\[j\]==11: Unknown$ +^\[main.assertion.53\] .* assertion b\[j\]\[j\]==0: Unknown$ +^\[main.assertion.54\] .* assertion b\[j\]\[j\]==11: Unknown$ +^\[main.assertion.55\] .* assertion a\[100\]\[0\]==0: Unknown$ +^\[main.assertion.56\] .* assertion a\[0\]\[100\]==0: Unknown$ +^\[main.assertion.57\] .* assertion c==0: Success$ +^\[main.assertion.58\] .* assertion c==0: Success$ +^\[main.assertion.59\] .* assertion ei\[0\]\[1\]==1: Success$ +^\[main.assertion.60\] .* assertion ei\[0\]\[1\]==0: Failure \(if reachable\)$ +^\[main.assertion.61\] .* assertion ei\[2\]\[1\]==0: Success$ +^\[main.assertion.62\] .* assertion ei\[2\]\[1\]==1: Failure \(if reachable\)$ +^\[main.assertion.63\] .* assertion ej\[0\]\[1\]==0: Unknown$ +^\[main.assertion.64\] .* assertion ej\[2\]\[1\]==0: Unknown$ +^\[main.assertion.65\] .* assertion ek\[0\]\[1\]==0: Unknown$ +^\[main.assertion.66\] .* assertion c==0: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-array-of-constants-pointer/sensitivity_test_constants_array_of_constants_pointer.c b/regression/goto-analyzer/sensitivity-test-constants-array-of-constants-pointer/sensitivity_test_constants_array_of_constants_pointer.c new file mode 100644 index 00000000000..66edcccfbfb --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-array-of-constants-pointer/sensitivity_test_constants_array_of_constants_pointer.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/array_of_pointer_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-array-of-constants-pointer/test.desc b/regression/goto-analyzer/sensitivity-test-constants-array-of-constants-pointer/test.desc new file mode 100644 index 00000000000..9242552c707 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-array-of-constants-pointer/test.desc @@ -0,0 +1,71 @@ +FUTURE +sensitivity_test_constants_array_of_constants_pointer.c +--variable --arrays --pointers --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion a\[1\]==&a0: Success$ +^\[main.assertion.2\] .* assertion a\[1\]==&a3: Failure \(if reachable\)$ +^\[main.assertion.3\] .* assertion \*a\[1\]==0: Success$ +^\[main.assertion.4\] .* assertion \*a\[1\]==3: Failure \(if reachable\)$ +^\[main.assertion.5\] .* assertion b\[1\]==&b1: Success$ +^\[main.assertion.6\] .* assertion b\[1\]==&b3: Failure \(if reachable\)$ +^\[main.assertion.7\] .* assertion \*b\[1\]==11: Success$ +^\[main.assertion.8\] .* assertion \*b\[1\]==13: Failure \(if reachable\)$ +^\[main.assertion.9\] .* assertion \*\(b\+1\)==&b1: Success$ +^\[main.assertion.10\] .* assertion \*\(b\+1\)==&b3: Failure \(if reachable\)$ +^\[main.assertion.11\] .* assertion \*\(1\+b\)==&b1: Unknown$ +^\[main.assertion.12\] .* assertion \*\(1\+b\)==&b3: Unknown$ +^\[main.assertion.13\] .* assertion 1\[b\]==&b1: Success$ +^\[main.assertion.14\] .* assertion 1\[b\]==&b3: Failure \(if reachable\)$ +^\[main.assertion.15\] .* assertion \*\*\(b\+1\)==11: Success$ +^\[main.assertion.16\] .* assertion \*\*\(b\+1\)==13: Failure \(if reachable\)$ +^\[main.assertion.17\] .* assertion \*\*\(1\+b\)==11: Unknown$ +^\[main.assertion.18\] .* assertion \*\*\(1\+b\)==13: Unknown$ +^\[main.assertion.19\] .* assertion \*1\[b\]==11: Success$ +^\[main.assertion.20\] .* assertion \*1\[b\]==13: Failure \(if reachable\)$ +^\[main.assertion.21\] .* assertion c\[0\]==&c0: Unknown$ +^\[main.assertion.22\] .* assertion c\[0\]==&c3: Unknown$ +^\[main.assertion.23\] .* assertion d\[0\]==&d0: Unknown$ +^\[main.assertion.24\] .* assertion d\[0\]==&d3: Unknown$ +^\[main.assertion.25\] .* assertion \*c\[0\]==20: Unknown$ +^\[main.assertion.26\] .* assertion \*c\[0\]==23: Unknown$ +^\[main.assertion.27\] .* assertion \*d\[0\]==30: Unknown$ +^\[main.assertion.28\] .* assertion \*d\[0\]==33: Unknown$ +^\[main.assertion.29\] .* assertion a\[i\]==&a0: Success$ +^\[main.assertion.30\] .* assertion a\[i\]==&a3: Failure \(if reachable\)$ +^\[main.assertion.31\] .* assertion a\[j\]==&a0: Unknown$ +^\[main.assertion.32\] .* assertion a\[j\]==&a3: Unknown$ +^\[main.assertion.33\] .* assertion \*a\[i\]==0: Success$ +^\[main.assertion.34\] .* assertion \*a\[i\]==3: Failure \(if reachable\)$ +^\[main.assertion.35\] .* assertion \*a\[j\]==0: Unknown$ +^\[main.assertion.36\] .* assertion \*a\[j\]==3: Unknown$ +^\[main.assertion.37\] .* assertion b\[i\]==&b0: Success$ +^\[main.assertion.38\] .* assertion b\[i\]==&b1: Failure \(if reachable\)$ +^\[main.assertion.39\] .* assertion b\[j\]==&b0: Unknown$ +^\[main.assertion.40\] .* assertion b\[j\]==&b3: Unknown$ +^\[main.assertion.41\] .* assertion \*b\[i\]==10: Success$ +^\[main.assertion.42\] .* assertion \*b\[i\]==11: Failure \(if reachable\)$ +^\[main.assertion.43\] .* assertion \*b\[j\]==10: Unknown$ +^\[main.assertion.44\] .* assertion \*b\[j\]==13: Unknown$ +^\[main.assertion.45\] .* assertion a\[100\]==&a2: Unknown$ +^\[main.assertion.46\] .* assertion \*a\[100\]==2: Unknown$ +^\[main.assertion.47\] .* assertion b\[1\]==&b1: Success$ +^\[main.assertion.48\] .* assertion \*b\[1\]==11: Success$ +^\[main.assertion.49\] .* assertion ei\[0\]==&ei1: Success$ +^\[main.assertion.50\] .* assertion ei\[0\]==&ei0: Failure \(if reachable\)$ +^\[main.assertion.51\] .* assertion ei\[2\]==&ei0: Success$ +^\[main.assertion.52\] .* assertion ei\[2\]==&ei1: Failure \(if reachable\)$ +^\[main.assertion.53\] .* assertion \*ei\[0\]==41: Success$ +^\[main.assertion.54\] .* assertion \*ei\[0\]==40: Failure \(if reachable\)$ +^\[main.assertion.55\] .* assertion \*ei\[2\]==40: Success$ +^\[main.assertion.56\] .* assertion \*ei\[2\]==41: Failure \(if reachable\)$ +^\[main.assertion.57\] .* assertion ej\[0\]==&ej0: Unknown$ +^\[main.assertion.58\] .* assertion ej\[2\]==&ej0: Unknown$ +^\[main.assertion.59\] .* assertion ej\[2\]==&ej1: Unknown$ +^\[main.assertion.60\] .* assertion \*ej\[0\]==50: Unknown$ +^\[main.assertion.61\] .* assertion \*ej\[2\]==50: Unknown$ +^\[main.assertion.62\] .* assertion \*ej\[2\]==51: Unknown$ +^\[main.assertion.63\] .* assertion ek\[0\]==&ek0: Unknown$ +^\[main.assertion.64\] .* assertion \*ek\[0\]==60: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-array-of-two-value-pointer/sensitivity_test_constants_array_of_two_value_pointer.c b/regression/goto-analyzer/sensitivity-test-constants-array-of-two-value-pointer/sensitivity_test_constants_array_of_two_value_pointer.c new file mode 100644 index 00000000000..66edcccfbfb --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-array-of-two-value-pointer/sensitivity_test_constants_array_of_two_value_pointer.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/array_of_pointer_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-array-of-two-value-pointer/test.desc b/regression/goto-analyzer/sensitivity-test-constants-array-of-two-value-pointer/test.desc new file mode 100644 index 00000000000..74f5f128ed6 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-array-of-two-value-pointer/test.desc @@ -0,0 +1,71 @@ +FUTURE +sensitivity_test_constants_array_of_two_value_pointer.c +--variable --arrays --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion a\[1\]==&a0: Unknown$ +^\[main.assertion.2\] .* assertion a\[1\]==&a3: Unknown$ +^\[main.assertion.3\] .* assertion \*a\[1\]==0: Unknown$ +^\[main.assertion.4\] .* assertion \*a\[1\]==3: Unknown$ +^\[main.assertion.5\] .* assertion b\[1\]==&b1: Unknown$ +^\[main.assertion.6\] .* assertion b\[1\]==&b3: Unknown$ +^\[main.assertion.7\] .* assertion \*b\[1\]==11: Unknown$ +^\[main.assertion.8\] .* assertion \*b\[1\]==13: Unknown$ +^\[main.assertion.9\] .* assertion \*\(b\+1\)==&b1: Unknown$ +^\[main.assertion.10\] .* assertion \*\(b\+1\)==&b3: Unknown$ +^\[main.assertion.11\] .* assertion \*\(1\+b\)==&b1: Unknown$ +^\[main.assertion.12\] .* assertion \*\(1\+b\)==&b3: Unknown$ +^\[main.assertion.13\] .* assertion 1\[b\]==&b1: Unknown$ +^\[main.assertion.14\] .* assertion 1\[b\]==&b3: Unknown$ +^\[main.assertion.15\] .* assertion \*\*\(b\+1\)==11: Unknown$ +^\[main.assertion.16\] .* assertion \*\*\(b\+1\)==13: Unknown$ +^\[main.assertion.17\] .* assertion \*\*\(1\+b\)==11: Unknown$ +^\[main.assertion.18\] .* assertion \*\*\(1\+b\)==13: Unknown$ +^\[main.assertion.19\] .* assertion \*1\[b\]==11: Unknown$ +^\[main.assertion.20\] .* assertion \*1\[b\]==13: Unknown$ +^\[main.assertion.21\] .* assertion c\[0\]==&c0: Unknown$ +^\[main.assertion.22\] .* assertion c\[0\]==&c3: Unknown$ +^\[main.assertion.23\] .* assertion d\[0\]==&d0: Unknown$ +^\[main.assertion.24\] .* assertion d\[0\]==&d3: Unknown$ +^\[main.assertion.25\] .* assertion \*c\[0\]==20: Unknown$ +^\[main.assertion.26\] .* assertion \*c\[0\]==23: Unknown$ +^\[main.assertion.27\] .* assertion \*d\[0\]==30: Unknown$ +^\[main.assertion.28\] .* assertion \*d\[0\]==33: Unknown$ +^\[main.assertion.29\] .* assertion a\[i\]==&a0: Unknown$ +^\[main.assertion.30\] .* assertion a\[i\]==&a3: Unknown$ +^\[main.assertion.31\] .* assertion a\[j\]==&a0: Unknown$ +^\[main.assertion.32\] .* assertion a\[j\]==&a3: Unknown$ +^\[main.assertion.33\] .* assertion \*a\[i\]==0: Unknown$ +^\[main.assertion.34\] .* assertion \*a\[i\]==3: Unknown$ +^\[main.assertion.35\] .* assertion \*a\[j\]==0: Unknown$ +^\[main.assertion.36\] .* assertion \*a\[j\]==3: Unknown$ +^\[main.assertion.37\] .* assertion b\[i\]==&b0: Unknown$ +^\[main.assertion.38\] .* assertion b\[i\]==&b1: Unknown$ +^\[main.assertion.39\] .* assertion b\[j\]==&b0: Unknown$ +^\[main.assertion.40\] .* assertion b\[j\]==&b3: Unknown$ +^\[main.assertion.41\] .* assertion \*b\[i\]==10: Unknown$ +^\[main.assertion.42\] .* assertion \*b\[i\]==11: Unknown$ +^\[main.assertion.43\] .* assertion \*b\[j\]==10: Unknown$ +^\[main.assertion.44\] .* assertion \*b\[j\]==13: Unknown$ +^\[main.assertion.45\] .* assertion a\[100\]==&a2: Unknown$ +^\[main.assertion.46\] .* assertion \*a\[100\]==2: Unknown$ +^\[main.assertion.47\] .* assertion b\[1\]==&b1: Unknown$ +^\[main.assertion.48\] .* assertion \*b\[1\]==11: Unknown$ +^\[main.assertion.49\] .* assertion ei\[0\]==&ei1: Unknown$ +^\[main.assertion.50\] .* assertion ei\[0\]==&ei0: Unknown$ +^\[main.assertion.51\] .* assertion ei\[2\]==&ei0: Unknown$ +^\[main.assertion.52\] .* assertion ei\[2\]==&ei1: Unknown$ +^\[main.assertion.53\] .* assertion \*ei\[0\]==41: Unknown$ +^\[main.assertion.54\] .* assertion \*ei\[0\]==40: Unknown$ +^\[main.assertion.55\] .* assertion \*ei\[2\]==40: Unknown$ +^\[main.assertion.56\] .* assertion \*ei\[2\]==41: Unknown$ +^\[main.assertion.57\] .* assertion ej\[0\]==&ej0: Unknown$ +^\[main.assertion.58\] .* assertion ej\[2\]==&ej0: Unknown$ +^\[main.assertion.59\] .* assertion ej\[2\]==&ej1: Unknown$ +^\[main.assertion.60\] .* assertion \*ej\[0\]==50: Unknown$ +^\[main.assertion.61\] .* assertion \*ej\[2\]==50: Unknown$ +^\[main.assertion.62\] .* assertion \*ej\[2\]==51: Unknown$ +^\[main.assertion.63\] .* assertion ek\[0\]==&ek0: Unknown$ +^\[main.assertion.64\] .* assertion \*ek\[0\]==60: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-array/sensitivity_test_constants_array.c b/regression/goto-analyzer/sensitivity-test-constants-array/sensitivity_test_constants_array.c new file mode 100644 index 00000000000..e0a5a37a2a2 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-array/sensitivity_test_constants_array.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/array_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-array/test.desc b/regression/goto-analyzer/sensitivity-test-constants-array/test.desc new file mode 100644 index 00000000000..b48a2c823ca --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-array/test.desc @@ -0,0 +1,39 @@ +FUTURE +sensitivity_test_constants_array.c +--variable --arrays --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion a\[1\]==0: Success$ +^\[main.assertion.2\] .* assertion a\[1\]==1: Failure \(if reachable\)$ +^\[main.assertion.3\] .* assertion b\[1\]==0: Success$ +^\[main.assertion.4\] .* assertion b\[1\]==1: Failure \(if reachable\)$ +^\[main.assertion.5\] .* assertion \*\(b\+1\)==0: Success$ +^\[main.assertion.6\] .* assertion \*\(b\+1\)==1: Failure \(if reachable\)$ +^\[main.assertion.7\] .* assertion \*\(1\+b\)==0: Unknown$ +^\[main.assertion.8\] .* assertion \*\(1\+b\)==1: Unknown$ +^\[main.assertion.9\] .* assertion 1\[b\]==0: Success$ +^\[main.assertion.10\] .* assertion 1\[b\]==1: Failure \(if reachable\)$ +^\[main.assertion.11\] .* assertion c\[0\]==0: Success$ +^\[main.assertion.12\] .* assertion c\[0\]==1: Failure \(if reachable\)$ +^\[main.assertion.13\] .* assertion d\[0\]==0: Unknown$ +^\[main.assertion.14\] .* assertion d\[0\]==2: Unknown$ +^\[main.assertion.15\] .* assertion d\[1\]==0: Success$ +^\[main.assertion.16\] .* assertion a\[i\]==0: Success$ +^\[main.assertion.17\] .* assertion a\[i\]==1: Failure \(if reachable\)$ +^\[main.assertion.18\] .* assertion a\[j\]==0: Unknown$ +^\[main.assertion.19\] .* assertion a\[j\]==1: Unknown$ +^\[main.assertion.20\] .* assertion b\[i\]==1: Success$ +^\[main.assertion.21\] .* assertion b\[i\]==0: Failure \(if reachable\)$ +^\[main.assertion.22\] .* assertion b\[j\]==0: Unknown$ +^\[main.assertion.23\] .* assertion b\[j\]==1: Unknown$ +^\[main.assertion.24\] .* assertion a\[100\]==0: Unknown$ +^\[main.assertion.25\] .* assertion b\[1\]==0: Success$ +^\[main.assertion.26\] .* assertion ei\[0\]==1: Success$ +^\[main.assertion.27\] .* assertion ei\[0\]==0: Failure \(if reachable\)$ +^\[main.assertion.28\] .* assertion ei\[2\]==0: Success$ +^\[main.assertion.29\] .* assertion ei\[2\]==1: Failure \(if reachable\)$ +^\[main.assertion.30\] .* assertion ej\[0\]==0: Unknown$ +^\[main.assertion.31\] .* assertion ej\[2\]==0: Unknown$ +^\[main.assertion.32\] .* assertion ek\[0\]==0: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-char/sensitivity_test_constants_char.c b/regression/goto-analyzer/sensitivity-test-constants-char/sensitivity_test_constants_char.c new file mode 100644 index 00000000000..b97be63e211 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-char/sensitivity_test_constants_char.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/char_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-char/test.desc b/regression/goto-analyzer/sensitivity-test-constants-char/test.desc new file mode 100644 index 00000000000..4ae7832010b --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-char/test.desc @@ -0,0 +1,9 @@ +FUTURE +sensitivity_test_constants_char.c +--variable --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x=='a': Success$ +^\[main.assertion.2\] .* assertion x=='b': Failure \(if reachable\)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-float/sensitivity_test_constants_float.c b/regression/goto-analyzer/sensitivity-test-constants-float/sensitivity_test_constants_float.c new file mode 100644 index 00000000000..4e801235552 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-float/sensitivity_test_constants_float.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/float_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-float/test.desc b/regression/goto-analyzer/sensitivity-test-constants-float/test.desc new file mode 100644 index 00000000000..634ea862f56 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-float/test.desc @@ -0,0 +1,9 @@ +FUTURE +sensitivity_test_constants_float.c +--variable --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x==0.0: Success$ +^\[main.assertion.2\] .* assertion x==1.0: Failure \(if reachable\)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-int/sensitivity_test_constants_int.c b/regression/goto-analyzer/sensitivity-test-constants-int/sensitivity_test_constants_int.c new file mode 100644 index 00000000000..8a0f75feb97 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-int/sensitivity_test_constants_int.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/int_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-int/test.desc b/regression/goto-analyzer/sensitivity-test-constants-int/test.desc new file mode 100644 index 00000000000..d3c274a9447 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-int/test.desc @@ -0,0 +1,30 @@ +FUTURE +sensitivity_test_constants_int.c +--variable --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x==0: Success$ +^\[main.assertion.2\] .* assertion x==1: Failure \(if reachable\)$ +^\[main.assertion.3\] .* assertion x==y: Unknown$ +^\[main.assertion.4\] .* assertion x<1: Success$ +^\[main.assertion.5\] .* assertion x<-1: Failure \(if reachable\)$ +^\[main.assertion.6\] .* assertion x-1: Success$ +^\[main.assertion.8\] .* assertion x>1: Failure \(if reachable\)$ +^\[main.assertion.9\] .* assertion x>y: Unknown$ +^\[main.assertion.10\] .* assertion x!=1: Success$ +^\[main.assertion.11\] .* assertion x!=0: Failure \(if reachable\)$ +^\[main.assertion.12\] .* assertion x!=y: Unknown$ +^\[main.assertion.13\] .* assertion !\(x==1\): Success$ +^\[main.assertion.14\] .* assertion !\(x==0\): Failure \(if reachable\)$ +^\[main.assertion.15\] .* assertion !\(x==y\): Unknown$ +^\[main.assertion.16\] .* assertion y<2: Unknown$ +^\[main.assertion.17\] .* assertion y>2: Unknown$ +^\[main.assertion.18\] .* assertion y==1: Unknown$ +^\[main.assertion.19\] .* assertion z==0: Success$ +^\[main.assertion.20\] .* assertion z==10: Failure \(if reachable\)$ +^\[main.assertion.21\] .* assertion x==0: Success \(unreachable\)$ +^\[main.assertion.22\] .* assertion x==1: Success \(unreachable\)$ +^\[main.assertion.23\] .* assertion y==0: Success \(unreachable\)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-array/sensitivity_test_constants_pointer_to_constants_array.c b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-array/sensitivity_test_constants_pointer_to_constants_array.c new file mode 100644 index 00000000000..082fe2e62c8 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-array/sensitivity_test_constants_pointer_to_constants_array.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/pointer_to_array_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-array/test.desc b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-array/test.desc new file mode 100644 index 00000000000..7ccb164ab0f --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-array/test.desc @@ -0,0 +1,21 @@ +FUTURE +sensitivity_test_constants_pointer_to_constants_array.c +--variable --pointers --arrays --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion p==&a\[0\]: Success$ +^\[main.assertion.2\] .* assertion \*p==1: Success$ +^\[main.assertion.3\] .* assertion q==p\+1: Unknown$ +^\[main.assertion.4\] .* assertion \*q==2: Unknown$ +^\[main.assertion.5\] .* assertion q-p==x: Unknown$ +^\[main.assertion.6\] .* assertion a\[1\]==4: Unknown$ +^\[main.assertion.7\] .* assertion \*r==2: Unknown$ +^\[main.assertion.8\] .* assertion \*r==1: Unknown$ +^\[main.assertion.9\] .* assertion \*s==0: Unknown$ +^\[main.assertion.10\] .* assertion \*s==1: Unknown$ +^\[main.assertion.11\] .* assertion t==p\+i: Unknown$ +^\[main.assertion.12\] .* assertion t-p==y: Unknown$ +^\[main.assertion.13\] .* assertion a\[i\]==5: Unknown$ +^\[main.assertion.14\] .* assertion a\[1\]==5: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-pointer/sensitivity_test_constants_pointer_to_constants_pointer.c b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-pointer/sensitivity_test_constants_pointer_to_constants_pointer.c new file mode 100644 index 00000000000..56e6edc1093 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-pointer/sensitivity_test_constants_pointer_to_constants_pointer.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/pointer_to_pointer_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-pointer/test.desc b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-pointer/test.desc new file mode 100644 index 00000000000..f7fa1706d6a --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-pointer/test.desc @@ -0,0 +1,13 @@ +FUTURE +sensitivity_test_constants_pointer_to_constants_pointer.c +--variable --pointers --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion \*\*x==0: Success$ +^\[main.assertion.2\] .* assertion \*\*x==1: Failure \(if reachable\)$ +^\[main.assertion.3\] .* assertion \*\*x==1: Success$ +^\[main.assertion.4\] .* assertion \*\*x==0: Failure \(if reachable\)$ +^\[main.assertion.5\] .* assertion a==2: Success$ +^\[main.assertion.6\] .* assertion a==1: Failure \(if reachable\)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-struct/sensitivity_test_constants_pointer_to_constants_struct.c b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-struct/sensitivity_test_constants_pointer_to_constants_struct.c new file mode 100644 index 00000000000..8f86047a407 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-struct/sensitivity_test_constants_pointer_to_constants_struct.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/pointer_to_struct_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-struct/test.desc b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-struct/test.desc new file mode 100644 index 00000000000..c7abd5e6821 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-constants-struct/test.desc @@ -0,0 +1,16 @@ +KNOWNBUG +sensitivity_test_constants_pointer_to_constants_struct.c +--variable --pointers --structs --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion \(\*p\).a==0: Success$ +^\[main.assertion.2\] .* assertion \(\*p\).a==1: Failure \(if reachable\)$ +^\[main.assertion.3\] .* assertion p->a==0: Success$ +^\[main.assertion.4\] .* assertion p->a==1: Failure \(if reachable\)$ +^\[main.assertion.5\] .* assertion p->b==2.0: Success$ +^\[main.assertion.6\] .* assertion p->b==1.0: Failure \(if reachable\)$ +-- +^warning: ignoring +-- +The final two assertions are the wrong way round as modifying the pointer +does not seem to be propogating through. See #96 diff --git a/regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-array/sensitivity_test_constants_pointer_to_two_value_array.c b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-array/sensitivity_test_constants_pointer_to_two_value_array.c new file mode 100644 index 00000000000..082fe2e62c8 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-array/sensitivity_test_constants_pointer_to_two_value_array.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/pointer_to_array_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-array/test.desc b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-array/test.desc new file mode 100644 index 00000000000..7121e17040d --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-array/test.desc @@ -0,0 +1,21 @@ +FUTURE +sensitivity_test_constants_pointer_to_two_value_array.c +--variable --pointers --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion p==&a\[0\]: Success$ +^\[main.assertion.2\] .* assertion \*p==1: Unknown$ +^\[main.assertion.3\] .* assertion q==p\+1: Unknown$ +^\[main.assertion.4\] .* assertion \*q==2: Unknown$ +^\[main.assertion.5\] .* assertion q-p==x: Unknown$ +^\[main.assertion.6\] .* assertion a\[1\]==4: Unknown$ +^\[main.assertion.7\] .* assertion \*r==2: Unknown$ +^\[main.assertion.8\] .* assertion \*r==1: Unknown$ +^\[main.assertion.9\] .* assertion \*s==0: Unknown$ +^\[main.assertion.10\] .* assertion \*s==1: Unknown$ +^\[main.assertion.11\] .* assertion t==p\+i: Unknown$ +^\[main.assertion.12\] .* assertion t-p==y: Unknown$ +^\[main.assertion.13\] .* assertion a\[i\]==5: Unknown$ +^\[main.assertion.14\] .* assertion a\[1\]==5: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-struct/sensitivity_test_constants_pointer_to_two_value_struct.c b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-struct/sensitivity_test_constants_pointer_to_two_value_struct.c new file mode 100644 index 00000000000..8f86047a407 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-struct/sensitivity_test_constants_pointer_to_two_value_struct.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/pointer_to_struct_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-struct/test.desc b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-struct/test.desc new file mode 100644 index 00000000000..a214499b34b --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-pointer-to-two-value-struct/test.desc @@ -0,0 +1,13 @@ +FUTURE +sensitivity_test_constants_pointer_to_two_value_struct.c +--variable --pointers --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion \(\*p\).a==0: Unknown$ +^\[main.assertion.2\] .* assertion \(\*p\).a==1: Unknown$ +^\[main.assertion.3\] .* assertion p->a==0: Unknown$ +^\[main.assertion.4\] .* assertion p->a==1: Unknown$ +^\[main.assertion.5\] .* assertion p->b==2.0: Unknown$ +^\[main.assertion.6\] .* assertion p->b==1.0: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-pointer/sensitivity_test_constants_pointer.c b/regression/goto-analyzer/sensitivity-test-constants-pointer/sensitivity_test_constants_pointer.c new file mode 100644 index 00000000000..a2167bc68f4 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-pointer/sensitivity_test_constants_pointer.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/pointer_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-pointer/test.desc b/regression/goto-analyzer/sensitivity-test-constants-pointer/test.desc new file mode 100644 index 00000000000..22c179f2233 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-pointer/test.desc @@ -0,0 +1,21 @@ +FUTURE +sensitivity_test_constants_pointer.c +--variable --pointers --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x==&a: Success$ +^\[main.assertion.2\] .* assertion x==&b: Failure \(if reachable\)$ +^\[main.assertion.3\] .* assertion x==x2: Success$ +^\[main.assertion.4\] .* assertion x==y: Failure \(if reachable\)$ +^\[main.assertion.5\] .* assertion \*x==0: Success$ +^\[main.assertion.6\] .* assertion \*x==1: Failure \(if reachable\)$ +^\[main.assertion.7\] .* assertion \*x==1: Success$ +^\[main.assertion.8\] .* assertion \*x==0: Failure \(if reachable\)$ +^\[main.assertion.9\] .* assertion a==2: Success$ +^\[main.assertion.10\] .* assertion a==0: Failure \(if reachable\)$ +^\[main.assertion.11\] .* assertion x==&a: Success$ +^\[main.assertion.12\] .* assertion \*x==0: Unknown$ +^\[main.assertion.13\] .* assertion x==&a: Unknown$ +^\[main.assertion.14\] .* assertion x==&b: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-array/sensitivity_test_constants_struct_of_constants_array.c b/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-array/sensitivity_test_constants_struct_of_constants_array.c new file mode 100644 index 00000000000..d50aea1ea24 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-array/sensitivity_test_constants_struct_of_constants_array.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/struct_of_array_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-array/test.desc b/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-array/test.desc new file mode 100644 index 00000000000..7b6ae24bf61 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-array/test.desc @@ -0,0 +1,24 @@ +FUTURE +sensitivity_test_constants_struct_of_constants_array.c +--variable --structs --arrays --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x.a\[0\]==0: Success$ +^\[main.assertion.2\] .* assertion \*\(x.a\+0\)==0: Success$ +^\[main.assertion.3\] .* assertion \*\(0\+x.a\)==0: Success$ +^\[main.assertion.4\] .* assertion 0\[x.a\]==0: Success$ +^\[main.assertion.5\] .* assertion x.a\[0\]==0: Success$ +^\[main.assertion.6\] .* assertion x.a\[1\]==1: Success$ +^\[main.assertion.7\] .* assertion x.b\[0\]==3.0f: Success$ +^\[main.assertion.8\] .* assertion x.a\[0\]==0: Success$ +^\[main.assertion.9\] .* assertion x.a\[1\]==1: Success$ +^\[main.assertion.10\] .* assertion x.b\[2\]>0.0f: Unknown$ +^\[main.assertion.11\] .* assertion x.b\[2\]==15.0f: Unknown$ +^\[main.assertion.12\] .* assertion x.b\[2\]==1.0f: Unknown$ +^\[main.assertion.13\] .* assertion x.b\[0\]==3.0f: Success$ +^\[main.assertion.14\] .* assertion x.a\[0\]<12: Unknown$ +^\[main.assertion.15\] .* assertion x.a\[0\]>2: Unknown$ +^\[main.assertion.16\] .* assertion x.a\[0\]==0: Unknown$ +^\[main.assertion.17\] .* assertion x.a\[1\]==1: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-pointer/sensitivity_test_constants_struct_of_constants_pointer.c b/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-pointer/sensitivity_test_constants_struct_of_constants_pointer.c new file mode 100644 index 00000000000..ab7d896ae5d --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-pointer/sensitivity_test_constants_struct_of_constants_pointer.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/struct_of_pointer_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-pointer/test.desc b/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-pointer/test.desc new file mode 100644 index 00000000000..b278a7ed47c --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-pointer/test.desc @@ -0,0 +1,33 @@ +FUTURE +sensitivity_test_constants_struct_of_constants_pointer.c +--variable --structs --pointers --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x.a==&a1: Success$ +^\[main.assertion.2\] .* assertion x.a==&a2: Failure \(if reachable\)$ +^\[main.assertion.3\] .* assertion x.b==&b1: Success$ +^\[main.assertion.4\] .* assertion x.b==&b2: Failure \(if reachable\)$ +^\[main.assertion.5\] .* assertion \*x.a==0: Success$ +^\[main.assertion.6\] .* assertion \*x.a==100: Failure \(if reachable\)$ +^\[main.assertion.7\] .* assertion \*x.b==10.0f: Success$ +^\[main.assertion.8\] .* assertion \*x.b==110.0f: Failure \(if reachable\)$ +^\[main.assertion.9\] .* assertion x.a==&a1: Success$ +^\[main.assertion.10\] .* assertion x.a==&a2: Failure \(if reachable\)$ +^\[main.assertion.11\] .* assertion \*x.a==0: Success$ +^\[main.assertion.12\] .* assertion \*x.a==100: Failure \(if reachable\)$ +^\[main.assertion.13\] .* assertion x.a==&a1: Success$ +^\[main.assertion.14\] .* assertion x.b==&b2: Unknown$ +^\[main.assertion.15\] .* assertion x.b==&b3: Unknown$ +^\[main.assertion.16\] .* assertion \*x.a==0: Success$ +^\[main.assertion.17\] .* assertion \*x.b==11.0f: Unknown$ +^\[main.assertion.18\] .* assertion \*x.b==12.0f: Unknown$ +^\[main.assertion.19\] .* assertion x.a==&a2: Unknown$ +^\[main.assertion.20\] .* assertion x.a==&a3: Unknown$ +^\[main.assertion.21\] .* assertion x.b==&b3: Unknown$ +^\[main.assertion.22\] .* assertion x.b==&b4: Unknown$ +^\[main.assertion.23\] .* assertion \*x.a==1: Unknown$ +^\[main.assertion.24\] .* assertion \*x.a==2: Unknown$ +^\[main.assertion.25\] .* assertion \*x.b==12.0f: Unknown$ +^\[main.assertion.26\] .* assertion \*x.b==13.0f: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-struct/sensitivity_test_constants_struct_of_constants_struct.c b/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-struct/sensitivity_test_constants_struct_of_constants_struct.c new file mode 100644 index 00000000000..ae2ab34d038 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-struct/sensitivity_test_constants_struct_of_constants_struct.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/struct_of_struct_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-struct/test.desc b/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-struct/test.desc new file mode 100644 index 00000000000..28f2e09614a --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-struct-of-constants-struct/test.desc @@ -0,0 +1,18 @@ +FUTURE +sensitivity_test_constants_struct_of_constants_struct.c +--variable --structs --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x.s1.a==0: Success$ +^\[main.assertion.2\] .* assertion x.s2.b==3.0f: Success$ +^\[main.assertion.3\] .* assertion x.s1.a==0: Success$ +^\[main.assertion.4\] .* assertion x.s1.a==10: Failure \(if reachable\)$ +^\[main.assertion.5\] .* assertion x.s1.b==1.0f: Success$ +^\[main.assertion.6\] .* assertion x.s2.b==3.0f: Unknown$ +^\[main.assertion.7\] .* assertion x.s2.b==0.0f: Unknown$ +^\[main.assertion.8\] .* assertion x.s1.a==20: Unknown$ +^\[main.assertion.9\] .* assertion x.s1.a<30: Unknown$ +^\[main.assertion.10\] .* assertion x.s2.a==22: Unknown$ +^\[main.assertion.11\] .* assertion x.s2.a<30: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-struct-of-two-value-array/sensitivity_test_constants_struct_of_two_value_array.c b/regression/goto-analyzer/sensitivity-test-constants-struct-of-two-value-array/sensitivity_test_constants_struct_of_two_value_array.c new file mode 100644 index 00000000000..d50aea1ea24 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-struct-of-two-value-array/sensitivity_test_constants_struct_of_two_value_array.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/struct_of_array_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-struct-of-two-value-array/test.desc b/regression/goto-analyzer/sensitivity-test-constants-struct-of-two-value-array/test.desc new file mode 100644 index 00000000000..30edb4b598c --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-struct-of-two-value-array/test.desc @@ -0,0 +1,24 @@ +FUTURE +sensitivity_test_constants_struct_of_two_value_array.c +--variable --structs --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x.a\[0\]==0: Unknown$ +^\[main.assertion.2\] .* assertion \*\(x.a\+0\)==0: Unknown$ +^\[main.assertion.3\] .* assertion \*\(0\+x.a\)==0: Unknown$ +^\[main.assertion.4\] .* assertion 0\[x.a\]==0: Unknown$ +^\[main.assertion.5\] .* assertion x.a\[0\]==0: Unknown$ +^\[main.assertion.6\] .* assertion x.a\[1\]==1: Unknown$ +^\[main.assertion.7\] .* assertion x.b\[0\]==3.0f: Unknown$ +^\[main.assertion.8\] .* assertion x.a\[0\]==0: Unknown$ +^\[main.assertion.9\] .* assertion x.a\[1\]==1: Unknown$ +^\[main.assertion.10\] .* assertion x.b\[2\]>0.0f: Unknown$ +^\[main.assertion.11\] .* assertion x.b\[2\]==15.0f: Unknown$ +^\[main.assertion.12\] .* assertion x.b\[2\]==1.0f: Unknown$ +^\[main.assertion.13\] .* assertion x.b\[0\]==3.0f: Unknown$ +^\[main.assertion.14\] .* assertion x.a\[0\]<12: Unknown$ +^\[main.assertion.15\] .* assertion x.a\[0\]>2: Unknown$ +^\[main.assertion.16\] .* assertion x.a\[0\]==0: Unknown$ +^\[main.assertion.17\] .* assertion x.a\[1\]==1: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-struct-of-two-value-pointer/sensitivity_test_constants_struct_of_two_value_pointer.c b/regression/goto-analyzer/sensitivity-test-constants-struct-of-two-value-pointer/sensitivity_test_constants_struct_of_two_value_pointer.c new file mode 100644 index 00000000000..ab7d896ae5d --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-struct-of-two-value-pointer/sensitivity_test_constants_struct_of_two_value_pointer.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/struct_of_pointer_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-struct-of-two-value-pointer/test.desc b/regression/goto-analyzer/sensitivity-test-constants-struct-of-two-value-pointer/test.desc new file mode 100644 index 00000000000..ea3a9cadb69 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-struct-of-two-value-pointer/test.desc @@ -0,0 +1,33 @@ +FUTURE +sensitivity_test_constants_struct_of_two_value_pointer.c +--variable --structs --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x.a==&a1: Unknown$ +^\[main.assertion.2\] .* assertion x.a==&a2: Unknown$ +^\[main.assertion.3\] .* assertion x.b==&b1: Unknown$ +^\[main.assertion.4\] .* assertion x.b==&b2: Unknown$ +^\[main.assertion.5\] .* assertion \*x.a==0: Unknown$ +^\[main.assertion.6\] .* assertion \*x.a==100: Unknown$ +^\[main.assertion.7\] .* assertion \*x.b==10.0f: Unknown$ +^\[main.assertion.8\] .* assertion \*x.b==110.0f: Unknown$ +^\[main.assertion.9\] .* assertion x.a==&a1: Unknown$ +^\[main.assertion.10\] .* assertion x.a==&a2: Unknown$ +^\[main.assertion.11\] .* assertion \*x.a==0: Unknown$ +^\[main.assertion.12\] .* assertion \*x.a==100: Unknown$ +^\[main.assertion.13\] .* assertion x.a==&a1: Unknown$ +^\[main.assertion.14\] .* assertion x.b==&b2: Unknown$ +^\[main.assertion.15\] .* assertion x.b==&b3: Unknown$ +^\[main.assertion.16\] .* assertion \*x.a==0: Unknown$ +^\[main.assertion.17\] .* assertion \*x.b==11.0f: Unknown$ +^\[main.assertion.18\] .* assertion \*x.b==12.0f: Unknown$ +^\[main.assertion.19\] .* assertion x.a==&a2: Unknown$ +^\[main.assertion.20\] .* assertion x.a==&a3: Unknown$ +^\[main.assertion.21\] .* assertion x.b==&b3: Unknown$ +^\[main.assertion.22\] .* assertion x.b==&b4: Unknown$ +^\[main.assertion.23\] .* assertion \*x.a==1: Unknown$ +^\[main.assertion.24\] .* assertion \*x.a==2: Unknown$ +^\[main.assertion.25\] .* assertion \*x.b==12.0f: Unknown$ +^\[main.assertion.26\] .* assertion \*x.b==13.0f: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-constants-struct/sensitivity_test_constants_struct.c b/regression/goto-analyzer/sensitivity-test-constants-struct/sensitivity_test_constants_struct.c new file mode 100644 index 00000000000..946ec769d9e --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-struct/sensitivity_test_constants_struct.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/struct_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-constants-struct/test.desc b/regression/goto-analyzer/sensitivity-test-constants-struct/test.desc new file mode 100644 index 00000000000..64a15fcae85 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-constants-struct/test.desc @@ -0,0 +1,16 @@ +FUTURE +sensitivity_test_constants_struct.c +--variable --structs --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x.a==0: Success$ +^\[main.assertion.2\] .* assertion x.a==1: Failure \(if reachable\)$ +^\[main.assertion.3\] .* assertion x.a==0: Success$ +^\[main.assertion.4\] .* assertion x.a==0: Success$ +^\[main.assertion.5\] .* assertion x.b>0.0f: Unknown$ +^\[main.assertion.6\] .* assertion x.b==1.0f: Unknown$ +^\[main.assertion.7\] .* assertion x.a<2: Unknown$ +^\[main.assertion.8\] .* assertion x.a>2: Unknown$ +^\[main.assertion.9\] .* assertion x.a==1: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-two-value-array-of-two-value-array/sensitivity_test_two_value_array_of_two_value_array.c b/regression/goto-analyzer/sensitivity-test-two-value-array-of-two-value-array/sensitivity_test_two_value_array_of_two_value_array.c new file mode 100644 index 00000000000..103849f7a32 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-array-of-two-value-array/sensitivity_test_two_value_array_of_two_value_array.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/array_of_array_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-two-value-array-of-two-value-array/test.desc b/regression/goto-analyzer/sensitivity-test-two-value-array-of-two-value-array/test.desc new file mode 100644 index 00000000000..2c2c3ed15a8 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-array-of-two-value-array/test.desc @@ -0,0 +1,73 @@ +FUTURE +sensitivity_test_two_value_array_of_two_value_array.c +--variable --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion a\[1\]\[2\]==0: Unknown$ +^\[main.assertion.2\] .* assertion a\[1\]\[2\]==1: Unknown$ +^\[main.assertion.3\] .* assertion b\[1\]\[2\]==5: Unknown$ +^\[main.assertion.4\] .* assertion b\[1\]\[2\]==0: Unknown$ +^\[main.assertion.5\] .* assertion \*\(b\[1\]\+2\)==5: Unknown$ +^\[main.assertion.6\] .* assertion \*\(b\[1\]\+2\)==0: Unknown$ +^\[main.assertion.7\] .* assertion \(\*\(b\+1\)\)\[2\]==5: Unknown$ +^\[main.assertion.8\] .* assertion \(\*\(b\+1\)\)\[2\]==0: Unknown$ +^\[main.assertion.9\] .* assertion \*\(\*\(b\+1\)\+2\)==5: Unknown$ +^\[main.assertion.10\] .* assertion \*\(\*\(b\+1\)\+2\)==0: Unknown$ +^\[main.assertion.11\] .* assertion 1\[b\]\[2\]==5: Unknown$ +^\[main.assertion.12\] .* assertion 1\[b\]\[2\]==0: Unknown$ +^\[main.assertion.13\] .* assertion \*\(1\[b\]\+2\)==5: Unknown$ +^\[main.assertion.14\] .* assertion \*\(1\[b\]\+2\)==0: Unknown$ +^\[main.assertion.15\] .* assertion \(\*\(1\+b\)\)\[2\]==5: Unknown$ +^\[main.assertion.16\] .* assertion \(\*\(1\+b\)\)\[2\]==0: Unknown$ +^\[main.assertion.17\] .* assertion \*\(\*\(1\+b\)\+2\)==5: Unknown$ +^\[main.assertion.18\] .* assertion \*\(\*\(1\+b\)\+2\)==0: Unknown$ +^\[main.assertion.19\] .* assertion 2\[1\[b\]\]==5: Unknown$ +^\[main.assertion.20\] .* assertion 2\[1\[b\]\]==0: Unknown$ +^\[main.assertion.21\] .* assertion \*\(2\+1\[b\]\)==5: Unknown$ +^\[main.assertion.22\] .* assertion \*\(2\+1\[b\]\)==0: Unknown$ +^\[main.assertion.23\] .* assertion \*\(2\+\*\(1\+b\)\)==5: Unknown$ +^\[main.assertion.24\] .* assertion \*\(2\+\*\(1\+b\)\)==0: Unknown$ +^\[main.assertion.25\] .* assertion a\[0\]\[1\]==0: Unknown$ +^\[main.assertion.26\] .* assertion a\[0\]\[1\]==1: Unknown$ +^\[main.assertion.27\] .* assertion a\[0\]\[2\]==0: Unknown$ +^\[main.assertion.28\] .* assertion b\[0\]\[1\]==2: Unknown$ +^\[main.assertion.29\] .* assertion b\[0\]\[1\]==3: Unknown$ +^\[main.assertion.30\] .* assertion b\[0\]\[2\]==2: Unknown$ +^\[main.assertion.31\] .* assertion a\[i\]\[1\]==0: Unknown$ +^\[main.assertion.32\] .* assertion a\[i\]\[1\]==1: Unknown$ +^\[main.assertion.33\] .* assertion a\[1\]\[i\]==0: Unknown$ +^\[main.assertion.34\] .* assertion a\[1\]\[i\]==1: Unknown$ +^\[main.assertion.35\] .* assertion a\[i\]\[i\]==0: Unknown$ +^\[main.assertion.36\] .* assertion a\[i\]\[i\]==1: Unknown$ +^\[main.assertion.37\] .* assertion a\[j\]\[1\]==0: Unknown$ +^\[main.assertion.38\] .* assertion a\[j\]\[1\]==1: Unknown$ +^\[main.assertion.39\] .* assertion a\[1\]\[j\]==0: Unknown$ +^\[main.assertion.40\] .* assertion a\[1\]\[j\]==1: Unknown$ +^\[main.assertion.41\] .* assertion a\[j\]\[j\]==0: Unknown$ +^\[main.assertion.42\] .* assertion a\[j\]\[j\]==1: Unknown$ +^\[main.assertion.43\] .* assertion b\[i\]\[1\]==1: Unknown$ +^\[main.assertion.44\] .* assertion b\[i\]\[1\]==11: Unknown$ +^\[main.assertion.45\] .* assertion b\[1\]\[i\]==3: Unknown$ +^\[main.assertion.46\] .* assertion b\[1\]\[i\]==11: Unknown$ +^\[main.assertion.47\] .* assertion b\[i\]\[i\]==0: Unknown$ +^\[main.assertion.48\] .* assertion b\[i\]\[i\]==11: Unknown$ +^\[main.assertion.49\] .* assertion b\[j\]\[1\]==1: Unknown$ +^\[main.assertion.50\] .* assertion b\[j\]\[1\]==11: Unknown$ +^\[main.assertion.51\] .* assertion b\[1\]\[j\]==3: Unknown$ +^\[main.assertion.52\] .* assertion b\[1\]\[j\]==11: Unknown$ +^\[main.assertion.53\] .* assertion b\[j\]\[j\]==0: Unknown$ +^\[main.assertion.54\] .* assertion b\[j\]\[j\]==11: Unknown$ +^\[main.assertion.55\] .* assertion a\[100\]\[0\]==0: Unknown$ +^\[main.assertion.56\] .* assertion a\[0\]\[100\]==0: Unknown$ +^\[main.assertion.57\] .* assertion c==0: Success$ +^\[main.assertion.58\] .* assertion c==0: Success$ +^\[main.assertion.59\] .* assertion ei\[0\]\[1\]==1: Unknown$ +^\[main.assertion.60\] .* assertion ei\[0\]\[1\]==0: Unknown$ +^\[main.assertion.61\] .* assertion ei\[2\]\[1\]==0: Unknown$ +^\[main.assertion.62\] .* assertion ei\[2\]\[1\]==1: Unknown$ +^\[main.assertion.63\] .* assertion ej\[0\]\[1\]==0: Unknown$ +^\[main.assertion.64\] .* assertion ej\[2\]\[1\]==0: Unknown$ +^\[main.assertion.65\] .* assertion ek\[0\]\[1\]==0: Unknown$ +^\[main.assertion.66\] .* assertion c==0: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-two-value-array-of-two-value-pointer/sensitivity_test_two_value_array_of_two_value_pointer.c b/regression/goto-analyzer/sensitivity-test-two-value-array-of-two-value-pointer/sensitivity_test_two_value_array_of_two_value_pointer.c new file mode 100644 index 00000000000..66edcccfbfb --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-array-of-two-value-pointer/sensitivity_test_two_value_array_of_two_value_pointer.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/array_of_pointer_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-two-value-array-of-two-value-pointer/test.desc b/regression/goto-analyzer/sensitivity-test-two-value-array-of-two-value-pointer/test.desc new file mode 100644 index 00000000000..f9de8e20a03 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-array-of-two-value-pointer/test.desc @@ -0,0 +1,71 @@ +FUTURE +sensitivity_test_two_value_array_of_two_value_pointer.c +--variable --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion a\[1\]==&a0: Unknown$ +^\[main.assertion.2\] .* assertion a\[1\]==&a3: Unknown$ +^\[main.assertion.3\] .* assertion \*a\[1\]==0: Unknown$ +^\[main.assertion.4\] .* assertion \*a\[1\]==3: Unknown$ +^\[main.assertion.5\] .* assertion b\[1\]==&b1: Unknown$ +^\[main.assertion.6\] .* assertion b\[1\]==&b3: Unknown$ +^\[main.assertion.7\] .* assertion \*b\[1\]==11: Unknown$ +^\[main.assertion.8\] .* assertion \*b\[1\]==13: Unknown$ +^\[main.assertion.9\] .* assertion \*\(b\+1\)==&b1: Unknown$ +^\[main.assertion.10\] .* assertion \*\(b\+1\)==&b3: Unknown$ +^\[main.assertion.11\] .* assertion \*\(1\+b\)==&b1: Unknown$ +^\[main.assertion.12\] .* assertion \*\(1\+b\)==&b3: Unknown$ +^\[main.assertion.13\] .* assertion 1\[b\]==&b1: Unknown$ +^\[main.assertion.14\] .* assertion 1\[b\]==&b3: Unknown$ +^\[main.assertion.15\] .* assertion \*\*\(b\+1\)==11: Unknown$ +^\[main.assertion.16\] .* assertion \*\*\(b\+1\)==13: Unknown$ +^\[main.assertion.17\] .* assertion \*\*\(1\+b\)==11: Unknown$ +^\[main.assertion.18\] .* assertion \*\*\(1\+b\)==13: Unknown$ +^\[main.assertion.19\] .* assertion \*1\[b\]==11: Unknown$ +^\[main.assertion.20\] .* assertion \*1\[b\]==13: Unknown$ +^\[main.assertion.21\] .* assertion c\[0\]==&c0: Unknown$ +^\[main.assertion.22\] .* assertion c\[0\]==&c3: Unknown$ +^\[main.assertion.23\] .* assertion d\[0\]==&d0: Unknown$ +^\[main.assertion.24\] .* assertion d\[0\]==&d3: Unknown$ +^\[main.assertion.25\] .* assertion \*c\[0\]==20: Unknown$ +^\[main.assertion.26\] .* assertion \*c\[0\]==23: Unknown$ +^\[main.assertion.27\] .* assertion \*d\[0\]==30: Unknown$ +^\[main.assertion.28\] .* assertion \*d\[0\]==33: Unknown$ +^\[main.assertion.29\] .* assertion a\[i\]==&a0: Unknown$ +^\[main.assertion.30\] .* assertion a\[i\]==&a3: Unknown$ +^\[main.assertion.31\] .* assertion a\[j\]==&a0: Unknown$ +^\[main.assertion.32\] .* assertion a\[j\]==&a3: Unknown$ +^\[main.assertion.33\] .* assertion \*a\[i\]==0: Unknown$ +^\[main.assertion.34\] .* assertion \*a\[i\]==3: Unknown$ +^\[main.assertion.35\] .* assertion \*a\[j\]==0: Unknown$ +^\[main.assertion.36\] .* assertion \*a\[j\]==3: Unknown$ +^\[main.assertion.37\] .* assertion b\[i\]==&b0: Unknown$ +^\[main.assertion.38\] .* assertion b\[i\]==&b1: Unknown$ +^\[main.assertion.39\] .* assertion b\[j\]==&b0: Unknown$ +^\[main.assertion.40\] .* assertion b\[j\]==&b3: Unknown$ +^\[main.assertion.41\] .* assertion \*b\[i\]==10: Unknown$ +^\[main.assertion.42\] .* assertion \*b\[i\]==11: Unknown$ +^\[main.assertion.43\] .* assertion \*b\[j\]==10: Unknown$ +^\[main.assertion.44\] .* assertion \*b\[j\]==13: Unknown$ +^\[main.assertion.45\] .* assertion a\[100\]==&a2: Unknown$ +^\[main.assertion.46\] .* assertion \*a\[100\]==2: Unknown$ +^\[main.assertion.47\] .* assertion b\[1\]==&b1: Unknown$ +^\[main.assertion.48\] .* assertion \*b\[1\]==11: Unknown$ +^\[main.assertion.49\] .* assertion ei\[0\]==&ei1: Unknown$ +^\[main.assertion.50\] .* assertion ei\[0\]==&ei0: Unknown$ +^\[main.assertion.51\] .* assertion ei\[2\]==&ei0: Unknown$ +^\[main.assertion.52\] .* assertion ei\[2\]==&ei1: Unknown$ +^\[main.assertion.53\] .* assertion \*ei\[0\]==41: Unknown$ +^\[main.assertion.54\] .* assertion \*ei\[0\]==40: Unknown$ +^\[main.assertion.55\] .* assertion \*ei\[2\]==40: Unknown$ +^\[main.assertion.56\] .* assertion \*ei\[2\]==41: Unknown$ +^\[main.assertion.57\] .* assertion ej\[0\]==&ej0: Unknown$ +^\[main.assertion.58\] .* assertion ej\[2\]==&ej0: Unknown$ +^\[main.assertion.59\] .* assertion ej\[2\]==&ej1: Unknown$ +^\[main.assertion.60\] .* assertion \*ej\[0\]==50: Unknown$ +^\[main.assertion.61\] .* assertion \*ej\[2\]==50: Unknown$ +^\[main.assertion.62\] .* assertion \*ej\[2\]==51: Unknown$ +^\[main.assertion.63\] .* assertion ek\[0\]==&ek0: Unknown$ +^\[main.assertion.64\] .* assertion \*ek\[0\]==60: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-two-value-array/sensitivity_test_two_value_array.c b/regression/goto-analyzer/sensitivity-test-two-value-array/sensitivity_test_two_value_array.c new file mode 100644 index 00000000000..e0a5a37a2a2 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-array/sensitivity_test_two_value_array.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/array_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-two-value-array/test.desc b/regression/goto-analyzer/sensitivity-test-two-value-array/test.desc new file mode 100644 index 00000000000..23ee78bd74f --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-array/test.desc @@ -0,0 +1,39 @@ +FUTURE +sensitivity_test_two_value_array.c +--variable --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion a\[1\]==0: Unknown$ +^\[main.assertion.2\] .* assertion a\[1\]==1: Unknown$ +^\[main.assertion.3\] .* assertion b\[1\]==0: Unknown$ +^\[main.assertion.4\] .* assertion b\[1\]==1: Unknown$ +^\[main.assertion.5\] .* assertion \*\(b\+1\)==0: Unknown$ +^\[main.assertion.6\] .* assertion \*\(b\+1\)==1: Unknown$ +^\[main.assertion.7\] .* assertion \*\(1\+b\)==0: Unknown$ +^\[main.assertion.8\] .* assertion \*\(1\+b\)==1: Unknown$ +^\[main.assertion.9\] .* assertion 1\[b\]==0: Unknown$ +^\[main.assertion.10\] .* assertion 1\[b\]==1: Unknown$ +^\[main.assertion.11\] .* assertion c\[0\]==0: Unknown$ +^\[main.assertion.12\] .* assertion c\[0\]==1: Unknown$ +^\[main.assertion.13\] .* assertion d\[0\]==0: Unknown$ +^\[main.assertion.14\] .* assertion d\[0\]==2: Unknown$ +^\[main.assertion.15\] .* assertion d\[1\]==0: Unknown$ +^\[main.assertion.16\] .* assertion a\[i\]==0: Unknown$ +^\[main.assertion.17\] .* assertion a\[i\]==1: Unknown$ +^\[main.assertion.18\] .* assertion a\[j\]==0: Unknown$ +^\[main.assertion.19\] .* assertion a\[j\]==1: Unknown$ +^\[main.assertion.20\] .* assertion b\[i\]==1: Unknown$ +^\[main.assertion.21\] .* assertion b\[i\]==0: Unknown$ +^\[main.assertion.22\] .* assertion b\[j\]==0: Unknown$ +^\[main.assertion.23\] .* assertion b\[j\]==1: Unknown$ +^\[main.assertion.24\] .* assertion a\[100\]==0: Unknown$ +^\[main.assertion.25\] .* assertion b\[1\]==0: Unknown$ +^\[main.assertion.26\] .* assertion ei\[0\]==1: Unknown$ +^\[main.assertion.27\] .* assertion ei\[0\]==0: Unknown$ +^\[main.assertion.28\] .* assertion ei\[2\]==0: Unknown$ +^\[main.assertion.29\] .* assertion ei\[2\]==1: Unknown$ +^\[main.assertion.30\] .* assertion ej\[0\]==0: Unknown$ +^\[main.assertion.31\] .* assertion ej\[2\]==0: Unknown$ +^\[main.assertion.32\] .* assertion ek\[0\]==0: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-array/sensitivity_test_two_value_pointer_to_two_value_array.c b/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-array/sensitivity_test_two_value_pointer_to_two_value_array.c new file mode 100644 index 00000000000..082fe2e62c8 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-array/sensitivity_test_two_value_pointer_to_two_value_array.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/pointer_to_array_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-array/test.desc b/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-array/test.desc new file mode 100644 index 00000000000..974705f9fc1 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-array/test.desc @@ -0,0 +1,21 @@ +FUTURE +sensitivity_test_two_value_pointer_to_two_value_array.c +--variable --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion p==&a\[0\]: Unknown$ +^\[main.assertion.2\] .* assertion \*p==1: Unknown$ +^\[main.assertion.3\] .* assertion q==p\+1: Unknown$ +^\[main.assertion.4\] .* assertion \*q==2: Unknown$ +^\[main.assertion.5\] .* assertion q-p==x: Unknown$ +^\[main.assertion.6\] .* assertion a\[1\]==4: Unknown$ +^\[main.assertion.7\] .* assertion \*r==2: Unknown$ +^\[main.assertion.8\] .* assertion \*r==1: Unknown$ +^\[main.assertion.9\] .* assertion \*s==0: Unknown$ +^\[main.assertion.10\] .* assertion \*s==1: Unknown$ +^\[main.assertion.11\] .* assertion t==p\+i: Unknown$ +^\[main.assertion.12\] .* assertion t-p==y: Unknown$ +^\[main.assertion.13\] .* assertion a\[i\]==5: Unknown$ +^\[main.assertion.14\] .* assertion a\[1\]==5: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-pointer/sensitivity_test_two_value_pointer_to_two_value_pointer.c b/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-pointer/sensitivity_test_two_value_pointer_to_two_value_pointer.c new file mode 100644 index 00000000000..56e6edc1093 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-pointer/sensitivity_test_two_value_pointer_to_two_value_pointer.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/pointer_to_pointer_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-pointer/test.desc b/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-pointer/test.desc new file mode 100644 index 00000000000..e3582834688 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-pointer/test.desc @@ -0,0 +1,13 @@ +FUTURE +sensitivity_test_two_value_pointer_to_two_value_pointer.c +--variable --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion \*\*x==0: Unknown$ +^\[main.assertion.2\] .* assertion \*\*x==1: Unknown$ +^\[main.assertion.3\] .* assertion \*\*x==1: Unknown$ +^\[main.assertion.4\] .* assertion \*\*x==0: Unknown$ +^\[main.assertion.5\] .* assertion a==2: Unknown$ +^\[main.assertion.6\] .* assertion a==1: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-struct/sensitivity_test_two_value_pointer_to_two_value_struct.c b/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-struct/sensitivity_test_two_value_pointer_to_two_value_struct.c new file mode 100644 index 00000000000..8f86047a407 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-struct/sensitivity_test_two_value_pointer_to_two_value_struct.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/pointer_to_struct_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-struct/test.desc b/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-struct/test.desc new file mode 100644 index 00000000000..56a0be48407 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-pointer-to-two-value-struct/test.desc @@ -0,0 +1,13 @@ +FUTURE +sensitivity_test_two_value_pointer_to_two_value_struct.c +--variable --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion \(\*p\).a==0: Unknown$ +^\[main.assertion.2\] .* assertion \(\*p\).a==1: Unknown$ +^\[main.assertion.3\] .* assertion p->a==0: Unknown$ +^\[main.assertion.4\] .* assertion p->a==1: Unknown$ +^\[main.assertion.5\] .* assertion p->b==2.0: Unknown$ +^\[main.assertion.6\] .* assertion p->b==1.0: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-two-value-pointer/sensitivity_test_two_value_pointer.c b/regression/goto-analyzer/sensitivity-test-two-value-pointer/sensitivity_test_two_value_pointer.c new file mode 100644 index 00000000000..a2167bc68f4 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-pointer/sensitivity_test_two_value_pointer.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/pointer_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-two-value-pointer/test.desc b/regression/goto-analyzer/sensitivity-test-two-value-pointer/test.desc new file mode 100644 index 00000000000..da9abe2464f --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-pointer/test.desc @@ -0,0 +1,21 @@ +FUTURE +sensitivity_test_two_value_pointer.c +--variable --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x==&a: Unknown$ +^\[main.assertion.2\] .* assertion x==&b: Unknown$ +^\[main.assertion.3\] .* assertion x==x2: Unknown$ +^\[main.assertion.4\] .* assertion x==y: Unknown$ +^\[main.assertion.5\] .* assertion \*x==0: Unknown$ +^\[main.assertion.6\] .* assertion \*x==1: Unknown$ +^\[main.assertion.7\] .* assertion \*x==1: Unknown$ +^\[main.assertion.8\] .* assertion \*x==0: Unknown$ +^\[main.assertion.9\] .* assertion a==2: Unknown$ +^\[main.assertion.10\] .* assertion a==0: Unknown$ +^\[main.assertion.11\] .* assertion x==&a: Unknown$ +^\[main.assertion.12\] .* assertion \*x==0: Unknown$ +^\[main.assertion.13\] .* assertion x==&a: Unknown$ +^\[main.assertion.14\] .* assertion x==&b: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-array/sensitivity_test_two_value_struct_of_two_value_array.c b/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-array/sensitivity_test_two_value_struct_of_two_value_array.c new file mode 100644 index 00000000000..d50aea1ea24 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-array/sensitivity_test_two_value_struct_of_two_value_array.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/struct_of_array_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-array/test.desc b/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-array/test.desc new file mode 100644 index 00000000000..e8773cf68fc --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-array/test.desc @@ -0,0 +1,24 @@ +FUTURE +sensitivity_test_two_value_struct_of_two_value_array.c +--variable --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x.a\[0\]==0: Unknown$ +^\[main.assertion.2\] .* assertion \*\(x.a\+0\)==0: Unknown$ +^\[main.assertion.3\] .* assertion \*\(0\+x.a\)==0: Unknown$ +^\[main.assertion.4\] .* assertion 0\[x.a\]==0: Unknown$ +^\[main.assertion.5\] .* assertion x.a\[0\]==0: Unknown$ +^\[main.assertion.6\] .* assertion x.a\[1\]==1: Unknown$ +^\[main.assertion.7\] .* assertion x.b\[0\]==3.0f: Unknown$ +^\[main.assertion.8\] .* assertion x.a\[0\]==0: Unknown$ +^\[main.assertion.9\] .* assertion x.a\[1\]==1: Unknown$ +^\[main.assertion.10\] .* assertion x.b\[2\]>0.0f: Unknown$ +^\[main.assertion.11\] .* assertion x.b\[2\]==15.0f: Unknown$ +^\[main.assertion.12\] .* assertion x.b\[2\]==1.0f: Unknown$ +^\[main.assertion.13\] .* assertion x.b\[0\]==3.0f: Unknown$ +^\[main.assertion.14\] .* assertion x.a\[0\]<12: Unknown$ +^\[main.assertion.15\] .* assertion x.a\[0\]>2: Unknown$ +^\[main.assertion.16\] .* assertion x.a\[0\]==0: Unknown$ +^\[main.assertion.17\] .* assertion x.a\[1\]==1: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-pointer/sensitivity_test_two_value_struct_of_two_value_pointer.c b/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-pointer/sensitivity_test_two_value_struct_of_two_value_pointer.c new file mode 100644 index 00000000000..ab7d896ae5d --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-pointer/sensitivity_test_two_value_struct_of_two_value_pointer.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/struct_of_pointer_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-pointer/test.desc b/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-pointer/test.desc new file mode 100644 index 00000000000..06ebb29d047 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-pointer/test.desc @@ -0,0 +1,33 @@ +FUTURE +sensitivity_test_two_value_struct_of_two_value_pointer.c +--variable --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x.a==&a1: Unknown$ +^\[main.assertion.2\] .* assertion x.a==&a2: Unknown$ +^\[main.assertion.3\] .* assertion x.b==&b1: Unknown$ +^\[main.assertion.4\] .* assertion x.b==&b2: Unknown$ +^\[main.assertion.5\] .* assertion \*x.a==0: Unknown$ +^\[main.assertion.6\] .* assertion \*x.a==100: Unknown$ +^\[main.assertion.7\] .* assertion \*x.b==10.0f: Unknown$ +^\[main.assertion.8\] .* assertion \*x.b==110.0f: Unknown$ +^\[main.assertion.9\] .* assertion x.a==&a1: Unknown$ +^\[main.assertion.10\] .* assertion x.a==&a2: Unknown$ +^\[main.assertion.11\] .* assertion \*x.a==0: Unknown$ +^\[main.assertion.12\] .* assertion \*x.a==100: Unknown$ +^\[main.assertion.13\] .* assertion x.a==&a1: Unknown$ +^\[main.assertion.14\] .* assertion x.b==&b2: Unknown$ +^\[main.assertion.15\] .* assertion x.b==&b3: Unknown$ +^\[main.assertion.16\] .* assertion \*x.a==0: Unknown$ +^\[main.assertion.17\] .* assertion \*x.b==11.0f: Unknown$ +^\[main.assertion.18\] .* assertion \*x.b==12.0f: Unknown$ +^\[main.assertion.19\] .* assertion x.a==&a2: Unknown$ +^\[main.assertion.20\] .* assertion x.a==&a3: Unknown$ +^\[main.assertion.21\] .* assertion x.b==&b3: Unknown$ +^\[main.assertion.22\] .* assertion x.b==&b4: Unknown$ +^\[main.assertion.23\] .* assertion \*x.a==1: Unknown$ +^\[main.assertion.24\] .* assertion \*x.a==2: Unknown$ +^\[main.assertion.25\] .* assertion \*x.b==12.0f: Unknown$ +^\[main.assertion.26\] .* assertion \*x.b==13.0f: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-struct/sensitivity_test_two_value_struct_of_two_value_struct.c b/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-struct/sensitivity_test_two_value_struct_of_two_value_struct.c new file mode 100644 index 00000000000..ae2ab34d038 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-struct/sensitivity_test_two_value_struct_of_two_value_struct.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/struct_of_struct_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-struct/test.desc b/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-struct/test.desc new file mode 100644 index 00000000000..450055d2be6 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-struct-of-two-value-struct/test.desc @@ -0,0 +1,18 @@ +FUTURE +sensitivity_test_two_value_struct_of_two_value_struct.c +--variable --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x.s1.a==0: Unknown$ +^\[main.assertion.2\] .* assertion x.s2.b==3.0f: Unknown$ +^\[main.assertion.3\] .* assertion x.s1.a==0: Unknown$ +^\[main.assertion.4\] .* assertion x.s1.a==10: Unknown$ +^\[main.assertion.5\] .* assertion x.s1.b==1.0f: Unknown$ +^\[main.assertion.6\] .* assertion x.s2.b==3.0f: Unknown$ +^\[main.assertion.7\] .* assertion x.s2.b==0.0f: Unknown$ +^\[main.assertion.8\] .* assertion x.s1.a==20: Unknown$ +^\[main.assertion.9\] .* assertion x.s1.a<30: Unknown$ +^\[main.assertion.10\] .* assertion x.s2.a==22: Unknown$ +^\[main.assertion.11\] .* assertion x.s2.a<30: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/sensitivity-test-two-value-struct/sensitivity_test_two_value_struct.c b/regression/goto-analyzer/sensitivity-test-two-value-struct/sensitivity_test_two_value_struct.c new file mode 100644 index 00000000000..946ec769d9e --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-struct/sensitivity_test_two_value_struct.c @@ -0,0 +1 @@ +#include "../sensitivity-test-common-files/struct_sensitivity_tests.c" diff --git a/regression/goto-analyzer/sensitivity-test-two-value-struct/test.desc b/regression/goto-analyzer/sensitivity-test-two-value-struct/test.desc new file mode 100644 index 00000000000..157a3b25968 --- /dev/null +++ b/regression/goto-analyzer/sensitivity-test-two-value-struct/test.desc @@ -0,0 +1,16 @@ +FUTURE +sensitivity_test_two_value_struct.c +--variable --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] .* assertion x.a==0: Unknown$ +^\[main.assertion.2\] .* assertion x.a==1: Unknown$ +^\[main.assertion.3\] .* assertion x.a==0: Unknown$ +^\[main.assertion.4\] .* assertion x.a==0: Unknown$ +^\[main.assertion.5\] .* assertion x.b>0.0f: Unknown$ +^\[main.assertion.6\] .* assertion x.b==1.0f: Unknown$ +^\[main.assertion.7\] .* assertion x.a<2: Unknown$ +^\[main.assertion.8\] .* assertion x.a>2: Unknown$ +^\[main.assertion.9\] .* assertion x.a==1: Unknown$ +-- +^warning: ignoring