marek-trtik / cbmc

C Bounded Model Checker
http://www.cprover.org/cbmc
Other
0 stars 0 forks source link

19+3 guard failures of memcpy and strcpy #17

Closed marek-trtik closed 7 years ago

marek-trtik commented 7 years ago

Fix 19 issues in this page:

https://sv-comp.sosy-lab.org/2018/results/results-verified/cbmc.2017-11-19_1229.results.sv-comp18.Systems_DeviceDriversLinux64_ReachSafety.xml.bz2.merged.xml.bz2.table.html

And 3 issues in this page:

https://sv-comp.sosy-lab.org/2018/results/results-verified/cbmc.2017-11-19_1229.results.sv-comp18.ReachSafety-ControlFlow.xml.bz2.merged.xml.bz2.table.html

marek-trtik commented 7 years ago

Solved all 3 issues from https://sv-comp.sosy-lab.org/2018/results/results-verified/cbmc.2017-11-19_1229.results.sv-comp18.ReachSafety-ControlFlow.xml.bz2.merged.xml.bz2.table.html

Namely, these benchmarks were fixed (see first 3 commits (from master) in the branch https://github.com/marek-trtik/sv-benchmarks/commits/add_memcpy_guard):

ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c
ntdrivers/parport_true-unreach-call.i.cil.c
marek-trtik commented 7 years ago

I've fixed all the remaining benchmarks.

Here is the commit with fixes in CBMC: https://github.com/marek-trtik/cbmc/commit/1d8ce287df654e33ca50082b839eec1b55343de8

And here are PRs with fixes into benchmarks: https://github.com/sosy-lab/sv-benchmarks/pull/533 https://github.com/sosy-lab/sv-benchmarks/pull/532