search

sosy-lab / sv-benchmarks

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

veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i has tautological compare #44

Open delcypher opened 9 years ago

delcypher commented 9 years ago 
clang building /loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i
veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i:29:24: warning: comparison of unsigned expression >= 0 is always true [-Wtautological-compare]
  __VERIFIER_assert (i >= 0);
                     ~ ^  ~
1 warning generated.
tautschnig commented 7 years ago

This benchmark is almost the same as c/bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.c, if it weren't for the declaration of "i" as unsigned. Both of which exist in verisec (cf. https://github.com/cirosantilli/frama-c/tree/439bddd91e0686429a585ec3ae28200b60a31e8b/tests/verisec/suite/programs/apps/sendmail/CVE-2001-0653/tTflag).

As it is, it could either be used to rule out dumb tools (not really useful, I believe), or exclusively as a termination benchmark. @dbeyer Thoughts?