Shaobo

After reading the sea-dsa paper, I think I have a better understanding of this. The consequence of memcpy on this example is not that bad because unifying the nodes does...

> Sorry, but what should be the expected outcome of verifying this program? Thx! It should be verified.

I would like to revive this issue and propose something different than Monty's. I propose that we reuse the `__assert_fail` function to which libc expands the `assert` macro. We could...

SMACK can still report this bug. If anyone is interested in debugging it, we are happy to provide the imperfect witness file.

Hi @mutilin, Based on my observation, it is because dereferencing some uninitialized function pointers that are reachable from these parameters results in calling functions that lead to assertion failure (let's...

Hi @mutilin @AndrianovPavel , Sorry for the late reply. SMACK still reports bugs for these benchmarks. For example, in N1, `var_group_4` is calloced, so `__cil_tmp23` at line 8285 is equal...

@AndrianovPavel With respect to the fourth benchmark, `rtl8150_driver_group1` got the return value of `ldv_zalloc`, which can return a NULL pointer.

@AndrianovPavel I'm afraid your changes does not fix the issue. Please take a look at the error witness attached. [witness.txt](https://github.com/sosy-lab/sv-benchmarks/files/634931/witness.txt)

@AndrianovPavel @mutilin May I ask what is your assumption on uninitialized function pointer dispatch?

@mutilin Yes, it seems so for some benchmarks. For other benchmarks that SMACK reported a false bug, commenting out function pointers does not help. We will look into them.