Michael Tautschnig

So #121 is all about this, and there are discussions on the mailing list. I think we have a vast collection of technical solutions proposed. @PhilippWendler @dbeyer It's now a...

I will try to work on this now that #1037 and #1038 are merged. (#1055 should also be helpful, but does in itself not fix any of the issues reported...

The PRs #1059 through to #1069 address most of the issues of #1049. Once all of them are merged I will re-run CBMC on the benchmarks and see what's left...

@zvonimir Unfortunately, CBMC still times out on this benchmark. But perhaps the problem for SMACK is the absence of a non-deterministic initialiser in https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-validator-v0.8/linux-stable-5934df9-1-111_1a-drivers--scsi--gdth.ko-entry_point_ldv-val-v0.8.cil.out.i#L10888? This matters, because https://github.com/sosy-lab/sv-benchmarks/blob/master/c/ldv-validator-v0.8/linux-stable-5934df9-1-111_1a-drivers--scsi--gdth.ko-entry_point_ldv-val-v0.8.cil.out.i#L10904 does not...

I do not think that undefined behaviour is at play here. The assumption of strict aliasing enables additional (unsound) assumptions in the alias analysis used by GCC to build SSA...

In my opinion we first need to get rid of all the Cil-processed benchmarks. These are all affected by the kind of behaviour you are pointing out, as the pointers...

I have not claimed they are incorrectly processed - they have just been processed by Cil with settings such as to rewrite various access paths into arithmetic over a mix...

See also my rambling on the SV-COMP mailing list just moments ago: unless #56 and #59, plus #106 are closed, it would likely remain a good idea to actually ping...

I've tried to do at least the administrative changes in #239. I believe that all the remaining ones of `check.py` are already being tracked as issues, except for termination benchmarks...

The single PR #239 has now been replaced by individual ones in #243..#260.