mutilin

@lucasccordeiro do you have a witness confirmed by some of the witness checkers? According to which specification strings passes to `strncpy` should not overlap?

@lucasccordeiro Which version of the C standard you are referring to? @lucasccordeiro Which witness checker accepts the witness? > Violated property: > file line 18 function strncpy > strncpy src/dst...

> Yes, and "true-unreach-call" has nothing to do with undefined behaviour. Hence the `__VERIFIER_error()` is not reachable > That's what C11, page 363 says. C11 it is for C++, isn't...

@lucasccordeiro, @tautschnig, @danieldietsch thanks for the references `strncpy` in not defined by SV-COMP rules and Linux drivers do not use `string.h` functions from the standard library. Instead they use hardware-dependent...

> Brilliant, the correctness of that benchmark depends on a pointer-manipulating undefined function apparently not covered by any standard or rules. The correctness of all Linux driver benchmarks depend on...

All functions with names equal to C standard library functions should be renamed as they are not conforming to the C standard. Then recursively allocated memory will help here as...

@sim642 Simmo, the intention of the benchmark was to demonstrate a violation of [Module get/put](http://linuxtesting.org/ldv/online?action=show_rule&rule_id=0008) rule. In this example there is a mismatch between `try_module_get` expanded from `fops_get` and `module_put`...

I think it is better to move it to some TODO directory or remove, because now I do not have time to fix it.

All benchmarks in ldv-consumption directory are using parameters var_groupN which are not initialized. Why only these 3 benchmarks are causing problems?

See #227, #228, #229 for examples N1, N2, N3