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

Undefined behaviors in aws_array_list_pop_front_n_harness.i #1181

Closed zvonimir closed 3 years ago

zvonimir commented 4 years ago

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?

PhilippWendler commented 4 years ago

@gernst?

zvonimir commented 3 years ago

I fixed this in the referenced pull request.