sosy-lab/sv-benchmarks

Undefined behaviors in aws_array_list_pop_front_n_harness.i

zvonimir opened this issue · 2 comments

zvonimir commented

Here is one offending line: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/aws-c-common/aws_array_list_pop_front_n_harness.i#L8025

The variable n is later used (read) without being initialized. I am not sure what I should initialize it to. If I initialize it to nondet, I believe that leads to a bug/error trace.

There is another one here: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/aws-c-common/aws_array_list_pop_front_n_harness.i#L8012

Again, I am not sure how this structure should be initialized. Putting nondeterministic values into it it seems leads to a bug later on.

Any suggestions/clues what to do about this?

zvonimir commented

I fixed this in the referenced pull request.