A bug in 2ls?

[theyoucheng]

Let us consider the code below

int main(void) {
  int i=0;
  int x=0;
  x=5;
  while(i<1000) {
    i++;
    x--;
    assert(x>=5);
    assert(x<=5);
    assert(x>=0);
    assert(x<=0);
  }
 return 0;
}

If I run 2ls main.c, results are like

[main.assertion.1] assertion x >= 5: FAILURE
[main.assertion.2] assertion x <= 5: OK
[main.assertion.3] assertion x >= 0: OK
[main.assertion.4] assertion x <= 0: OK

Which part of the 2ls is likely to be responsible for this bug?

[peterschrammel]

What is the command line?

[theyoucheng]

On 4/13/17 4:10 PM, Peter Schrammel wrote: What is the command line?

2ls main.c

…

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#81 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ATYfm0Y_ia_s5DOF1swbmRS_YTKzaPGdks5rvjr4gaJpZM4M80ZZ>.

-- Youcheng Sun Research Assistant Department of Computer Science University of Oxford Wolfson Building, Parks Road Oxford OX1 3QD https://sites.google.com/site/theyoucheng/

[peterschrammel]

There are at least two bugs.

This works correctly and produces the correct invariant:

int main(void) {
  int i=0;
  int x=0;
  x=5;
  while(i<1000) {
    i++;
    x=x; // !!!
    assert(x>=5);
    assert(x<=5);
    assert(x>=0);
//    assert(x<=0);
  }
 return 0;
}

This does not produce the correct invariant:

int main(void) {
  int i=0;
  int x=0;
  x=5;
  while(i<1000) {
    i++;
    x=x; // !!!
    assert(x>=5);
    assert(x<=5);
    assert(x>=0);
    assert(x<=0);
  }
 return 0;
}

This does not produce the correct invariant:

int main(void) {
  int i=0;
  int x=0;
  x=5;
  while(i<1000) {
    i++;
    x--;
    assert(x>=5);
    assert(x<=5);
    assert(x>=0);
    //assert(x<=0);
  }
 return 0;
}

Please add these tests to regressions/invariants

[theyoucheng]

On 4/13/17 4:27 PM, Peter Schrammel wrote: There are at least two bugs. This works correctly and produces the correct invariant: |int main(void) { int i=0; int x=0; x=5; while(i<1000) { i++; x=x; // !!! assert(x>=5); assert(x<=5); assert(x>=0); // assert(x<=0); } return 0; } | This does not produce the correct invariant: |int main(void) { int i=0; int x=0; x=5; while(i<1000) { i++; x=x; // !!! assert(x>=5); assert(x<=5); assert(x>=0); assert(x<=0); } return 0; } | This does not produce the correct invariant: |int main(void) { int i=0; int x=0; x=5; while(i<1000) { i++; x--; assert(x>=5); assert(x<=5); assert(x>=0); //assert(x<=0); } return 0; } | Please add these tests to regressions/invariants

OK.

…

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#81 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ATYfm3EMjfksjCVC8NXeaDyQSgl5kIa_ks5rvj7OgaJpZM4M80ZZ>.

-- Youcheng Sun Research Assistant Department of Computer Science University of Oxford Wolfson Building, Parks Road Oxford OX1 3QD https://sites.google.com/site/theyoucheng/

[peterschrammel]

The expected invariant with intervals (default) would be 0<=i<=1000. x can have any value. The last assertion should fail the others be unknown.
With --octagons, the second assertion should hold, the last one fail and the others be unknown.