Michael Tautschnig 75212d89ea process_array_expr: abort upon reaching a void-typed object ... We previously attempted to compute the size of the expression, which is undefined if we arrive at a void-typed object, which typically will be a failed_symbol resulting from the (failed) attempt to dereference a void* pointer. There is nothing else to be done once we hit a failed_symbol, and thus we just return. Encountered in several of SV-COMP's device driver benchmarks (yes, they might not be memory safe, but this is not an excuse to fail an invariant). For example (with --unwind 2): ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--ethernet--atheros--atlx--atl1.ko-entry_point.cil.out.i		2019-05-30 08:07:26 +00:00
..
main.c	process_array_expr: abort upon reaching a void-typed object	2019-05-30 08:07:26 +00:00
test.desc	process_array_expr: abort upon reaching a void-typed object	2019-05-30 08:07:26 +00:00