search

sosy-lab / sv-benchmarks

Collection of Verification Tasks (MOVED, please follow the link)
https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
184 stars 169 forks source link

why can echo-2.i overflow? #1295

Closed Cglasses closed 3 years ago

Cglasses commented 3 years ago

Its corresponding YML file states that the expected result of the no-overflow property is false. I wonder under what circumstances will the program overflow? echo-2.zip

holznerst commented 3 years ago

Link to file: echo-2.c

MartinSpiessl commented 3 years ago

Hi, from the blame log of the file @holznerst linked I see that I created it. In the commit message https://github.com/sosy-lab/sv-benchmarks/commit/97299d4b5fefdaf2cb4e53ecf94bd61eb9eabab4 I mention issue https://github.com/sosy-lab/sv-benchmarks/issues/535, which contains a detailed description of the overflow.

tl;dr is that strlen(strerr) can lead to an integer close to INT_MAX, which is used in a signed integer addition to determine the length of the error message in bb_perror_msg, which will be the length of strerr plus some added stuff around that:

(unsigned long int)(applet_len + used + strerr_len + msgeol_len + 3) // overflow!