Undefined behaviour for module_get_put-drivers-char-ipmi-ipmi_watchdog.ko_true-unreach-call.cil.out.i.pp.i

[lucasccordeiro]

@marek-trtik and I have analyzed this benchmark. Our conclusions are: each execution trace (starting in the main function) reaches the line 6847, where is called a function ldv_initialize. Two things apply here:

1. The function ldv_initialize is only declared external in the benchmark, it is not defined.
2. There is no assumption about calling undefined function in rules of SV-COMP (https://sv-comp.sosy-lab.org/2018/rules.php).

So, the function pointer ldv_initialize is udefined and the call ldv_initialize() at line 6847 leads to an undefined behaviour.

Another way how to prove the presence of the undefined behaviour in the benchmark (assuming ldv_initialize is defined as identity) is as follows:

1. In the main function at line 6848 is called the function ipmi_wdog_init.
2. In function ipmi_wdog_init at line 6711 we call the function action_op. Important is that the first argument is the pointer to the global array action. This array was initialsed (before entering main) to the string reset. The second argument is NULL pointer.
3. When entering the function action_op the fist parameter inval points to the global array action and the second parameter outval is NULL.
4. The execution takes the else branch at line 6503.
5. The execution takes the else branch at line 6510.
6. The result from the call to strcmp at line 6516 returns 0, because it compares the string pointed to be inval (i.e. the string reset in action global variable) with the string constant reset.
7. The execution takes the true branch at line 6518.
8. At line 6545 there is called function strcpy with address of action global array with inval pointer, which contains address of the same array action. Therefore, we reach an undefined behaviour.