r12436, unnecessary warning for side-effects (csmith)
ID0000771: This issue was created automatically from Mantis Issue 771. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000771 | Frama-C | Kernel | public | 2011-03-30 | 2014-02-12 |
| Reporter | pascal | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
The command below leads the value analysis to check whether *g_19 can be in alias with g_20. They can be, so the value analysis emits an alarm, but I fail to see why this should be checked. The functions called have no side-effects. In fact, there are no side-effects in the whole assignment, except the side-effect of the assignment.
This is likely to be related to 676: the display below is very strange, with some statements displayed as empty lines (and still having inputs !!). __
bin/toplevel.opt -unspecified-access se.i
assert.30103607.7.c:632:[kernel] warning: Unspecified sequence with side effect: /* <- / tmp = safe_add_func_uint16_t_u_u(p_69.f2,(unsigned short )l_80); / <- / tmp_0 = safe_lshift_func_uint8_t_u_u((unsigned char )p_70.f0, (unsigned int )l_85); / <- p_70.f3 */
/* <-
*/
tmp_1 = safe_sub_func_uint32_t_u_u((unsigned int )l_90[0][0][1],
(unsigned int )*g_19);
/* <- */
tmp_2 = safe_sub_func_uint32_t_u_u(tmp_1,(unsigned int )p_70.f3);
/* <- l_80 g_14 */
/* <- */
tmp_3 = safe_rshift_func_int8_t_s_s((signed char )p_70.f3,g_20);
/* <- g_20 */
/* <-
*/
tmp_4 = safe_add_func_int8_t_s_s((signed char )((int )tmp_3 >= g_20),
(signed char )((long )(l_80 < (int32_t )g_14) <= 0xC7L));
/* <-
*/
tmp_5 = safe_add_func_int8_t_s_s(tmp_4,
(signed char )((uint32_t )((int )tmp != (int )tmp_0) <= tmp_2));
/* <- g_14 */
/* *g_19 <-
*/
*g_19 = (int32_t )safe_mul_func_int8_t_s_s((signed char )g_14,
(signed char )(1U != (unsigned int )tmp_5));