Termination analysis: Wrong result

[pwnchaser]

Hi, I noticed that theta returns also spurious warnings even with the latest version 6.24.3:

int main() {
  int b = 0;
  int *unused = &b;
  if (b != 0) 
      while(1) 
        ;
}

Here theta prints

$ "/home/Theta/theta-start.sh" "test.c"  "--backend" "LIVENESS_CEGAR"  "--property" "termination.prp" 
Verifying input 'test.c' using arguments '--backend LIVENESS_CEGAR --property termination.prp'
LD_LIBRARY_PATH=/home/Theta/lib java -Xss120m -Xmx14210m -jar /home/Theta/theta.jar --backend LIVENESS_CEGAR --property termination.prp --input test.c --smt-home /home/Theta/solvers
ParsingResult Success
Arithmetic: []
ParsingResult Success
Iteration 1
| Checking abstraction...
| Checking abstraction done, result: (AbstractorResult Unsafe)
| Refining abstraction...
Refining abstraction done, result: (RefinerResult Unsafe)
! Precision did NOT change in this iteration
(SafetyResult Unsafe Trace length: 0)
(Property termination)
(SafetyResult Unsafe Trace length: 0)

Interestingly, the pointer initialization triggers this behavior.
Maybe you want to take this into account for the svcomp26 version.
Cheers :)

[leventeBajczi]

Thanks!
It seems like we don't do well with pointers and termination using the liveness checker -- good to know!
@AdamZsofi or @mondokm will know more about this problem, but it seems like we don't properly check loop feasibility when pointers are present.
And pointers are present, because we do a reference elimination -- basically ,we take all referred variables, and push them to memory, by rewriting all variable accesses to dereferences, and all references to variable accesses, turning this program into:

int main() {
  int *b = malloc(sizeof(int));
  int *unused = b;
  if (*b != 0) 
      while(1) 
        ;
}

I just checked, and this can be circumvented for now by using a different engine to verify termination, for example, k-induction or IMC:
./theta-start.sh test.c --backend IMC --property termination.prp