Hernan Ponce de Leon

geo1-ll.c can overflow

3

The following program can overflow ``` int main() { int z, k; long long x, y, c; z = __VERIFIER_nondet_int(); k = __VERIFIER_nondet_int(); assume_abort_if_not(z >= 1); assume_abort_if_not(k >= 1); x...

Benchmarks for weak memory models

3

This issue is to keep track of discussions about adding new benchmarks to the repository exposing weak memory behaviours and the creation of a new SVCOMP category for weak memory...

Half of the benchmarks in this folder are tagged *.opt and half *.oepc. According to the README these are two optimisations to minimise the amount of instrumentation. These benchmarks were...

Reachability benchmarks with overflow

4

I recently found many benchmarks from the reachability category which contain overflow and thus undefined behaviours. These include `nla-digbench/hard.c` as mentioned in #1105 and the ones I mentioned in #1159....

When using smack to convert C code to boogie (`smack -t ...`), the generated boogie codecontains "debug information" such as from which file and line in the code an instructions...

If CP is enabled, the assertion in [this benchmark](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/pthread-demo-datarace-2.c/c/pthread-C-DAC/pthread-demo-datarace-2.c) is completely removed, making the program trivially safe (which is not).

We currently report a wrong result for this test ``` C C-atomic-cmpxchg-failure-02 { atomic_t x = ATOMIC_INIT(0); atomic_t z = ATOMIC_INIT(0); } P0(atomic_t *x, atomic_t *z) { int r0; int...

New LFDS benchmarks

1

The benchmarks are already written in C so we probably only need to write some client code. Stack: https://github.com/skeeto/lstack Queue: https://github.com/skeeto/scratch/blob/master/misc/queue.c

The following benchmark shows there is a problem with constant propagation ``` ❯ java -jar dartagnan/target/dartagnan-3.0.0.jar cat/svcomp.cat ../sv-benchmarks/c/pthread-divine/ring_1w1r-2.c --method=assume --bound=2 FAIL ❯ java -jar dartagnan/target/dartagnan-3.0.0.jar cat/svcomp.cat ../sv-benchmarks/c/pthread-divine/ring_1w1r-2.c --method=assume --bound=2 --program.processing.constantPropagation=false...

Assume event causes problems

21

When `assume_abort_if_not` is parsed as an `Assume` event, the family of benchmarks `pthread_wmm/rfi005_X` return PASS instead of FAIL.