Problem with ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--videobuf-vmalloc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c about sv-benchmarks HOT 2 CLOSED

What should we do with this? @dbeyer https://github.com/dbeyer who sent this problem report?

Aws Albarghouthi on Oct. 17, 2012, via the (previous) e-mail list.
Subject was "[SV-COMP: 59] DeviceDrivers64 issues"

On 2016-10-31 09:12 AM, Philipp Wendler wrote:

4 years ago in 8344f7e 8344f7e there was a report that the
file
|ldv-linux-3.4-simple/32_1_cilled_true-unreach-call_ok_nondet_linux-3.4-32_1-drivers--media--video--videobuf-vmalloc.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c|
might contain a counterexample:

|We find a counter-example because this example assumes a specific memory model. In my opinion, it is not a good example for the competition.
void main(void) { // -- assumed to be uninitialized disjoint memory region struct vm_area_struct *var_group1; ... videobuf_vm_close
(var_group1); ... } static void videobuf_vm_close(struct vm_area_struct *vma ) { q = ((struct videobuf_mapping *)vma->vm_private_data)->q; ...
videobuf_queue_lock(q); ... // code that writes memory through pointers videobuf_queue_lock(q); } __inline static void
videobuf_queue_lock(struct videobuf_queue *q ) { if (!q->ext_lock) mutex_lock (&(q->vb_lock)) } __inline static void
videobuf_queue_unlock(struct videobuf_queue *q ) { if (!q->ext_lock) mutex_unlock (&(q->vb_lock)) } A counterexample here is an execution in
which exactly one of mutex_lock()/mutex_unlock() is called. The problem with this example is that var_group1 is not allocated. So, our semantics
is to assume that it occupies a non-deterministically chosen memory regions (i.e., chosen by __VERIFIER_nondet_pointer()). However, under this
assumption, it is possible that the code between videobuf_queue_lock() and videobuf_queue_unlock() writes into q->ext_lock field. |

What should we do with this? @dbeyer https://github.com/dbeyer who sent this problem report?

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub #174, or mute the thread
https://github.com/notifications/unsubscribe-auth/ACzgUAEGWXi150SQMvoloT3DGnYcxKtAks5q5aLSgaJpZM4Kkw9N.

from sv-benchmarks.

I think it is better to remove the benchmark

from sv-benchmarks.