Martina Vitovská

Undefined behavior in termination-memory-linkedlists

1

I believe there can be signed integer underflow in [termination-memory-linkedlists/cll_by_lseg-alloca_false-termination.c.i](https://sv-comp.sosy-lab.org/2019/results/sv-benchmarks/c/termination-memory-linkedlists/cll_by_lseg-alloca_false-termination.c.i). In `main` 0 is passed as `n` to `new_cll`, hence -1 is passed to `new_lseg` as `n` which is recursively...

Invalid dereference in loops termination benchmark

1

There can be an invalid dereference in benchmark [loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i](https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i) on line [61](https://github.com/sosy-lab/sv-benchmarks/blob/15b5d973979ad445f45dde28dd9c46deb14542ef/c/loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i#L61) which leads to undefined behavior. The benchmark is labeled as false-unreach-call, which means that the assertion `__VERIFIER_assert(j -...

refactoring

1

refactor instr.cpp

http://llvm.org/docs/CodingStandards.html

Points-to analysis bug - accessing array elements

1

When accessing array elements, points-to analysis doesn't work correctly if the elements are accessed by index that changes, e.g. in a cycle: ``` for (i = 0; i < 10;...