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

Passing size of 0 to malloc leads to assertion violation #1221

Closed zvonimir closed 3 years ago

zvonimir commented 3 years ago

This commit avoids the situation where size of 0 can be passed to malloc. I think it does not alter the spirit of the benchmark.

This is related to the unresolved mailing list discussion with the subject line "Can malloc return 0 when 0 is passed as size?". As I wrote there, if we assume that malloc(0) can return NULL, which C standard allows, then these two benchmarks have an interesting (in my opinion) corner case bug. However, since we have not resolved the discussion, and in my opinion the current SVCOMP spec for malloc does not adequately cover this corner case, I am disabling 0 being passed to malloc.

If we decide that malloc(0) can return NULL, I will create buggy versions of these benchmarks.