diffblue-cbmc/regression/cbmc/Function5
Michael Tautschnig 867f748b13 Limit dereferencing checks to actual access size
For member accesses, access to other components need not be valid as
shown in the included regression test Malloc23.

Also do not require --bounds-check for full dereferencing checks.

Fixes #219.
2017-02-01 10:36:32 +00:00
..
main.c more regressions from CVS 2012-11-03 17:21:06 +00:00
test.desc Limit dereferencing checks to actual access size 2017-02-01 10:36:32 +00:00