sv-benchmarks Missing initialisation in LDV benchmarks results in undefined behavior

Missing initialisation in LDV benchmarks results in undefined behavior

Open tautschnig opened this issue 4 years ago • 2 comments

Various device driver benchmarks either completely lack initialisation of pointers passed around or do not suitably initialise members of allocated storage. See #1049 for a (likely incomplete) list of benchmarks, with the individual commits calling out which variables are lacking initialisation.

I should be able to provide fixes once #1037 and #1038 are merged.

Dec 16 '19 17:12 tautschnig

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 in #1049.)

Dec 22 '19 14:12 tautschnig

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 to be done.

Dec 23 '19 13:12 tautschnig

sv-benchmarks sv-benchmarks copied to clipboard

Missing initialisation in LDV benchmarks results in undefined behavior

sv-benchmarks
sv-benchmarks copied to clipboard