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 behavior in two AWS benchmarks #1280

Closed mchalupa closed 3 years ago

mchalupa commented 3 years ago

The following two benchmarks use uninitialized variables with automatic storage which is undefined behavior:

aws_priority_queue_init_dynamic_harness-1.i uses initial_item_allocation without inicialization: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/aws-c-common/aws_priority_queue_init_dynamic_harness-1.i#L7919

aws_byte_buf_write_from_whole_buffer_harness-1.i uses the structure buf without inicialization here: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/aws-c-common/aws_byte_buf_write_from_whole_buffer_harness-1.i#L8987