| Anonymous | Login | Signup for a new account | 2019-10-18 12:08 CEST |  |
| Main | My View | View Issues | Change Log | Roadmap | Repositories |
| View Issue Details [ Jump to Notes ] [ Related Changesets ] | [ Issue History ] [ Print ] | ||||||||
| ID | Project | Category | View Status | Date Submitted | Last Update | ||||
| 0000963 | Frama-C | Plug-in > slicing | public | 2011-09-14 14:13 | 2014-02-12 16:59 | ||||
| Reporter | pascal | ||||||||
| Assigned To | Anne | ||||||||
| Priority | normal | Severity | minor | Reproducibility | always | ||||
| Status | closed | Resolution | fixed | ||||||
| Platform | OS | OS Version | |||||||
| Product Version | Frama-C GIT, precise the release id | ||||||||
| Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
| Summary | 0000963: Sliced program computes differently from original (csmith) | ||||||||
| Description | Bon, j'ai peut-être un peu perdu la main, alors il faudra m'excuser si je rapporte un non-problème, ou si j'oublie des détails au début. L'architecture cible est maintenant -machdep x86_64 (on a maintenant confiance dans l'analyse de valeurs sur cette architecture). La commande de slicing utilisée est dans le script slice_src_dest.sh Pour compiler l'original ou le programme slicé: gcc -Iruntime s.14134425.9.c show_each.c -o orig gcc -Iruntime s.14134425.9.s.c show_each.c -o slice (c'est un gcc 64-bit) J'obtiens les fichiers .exec et .execs, qui sont différents. | ||||||||
| Tags | No tags attached. | ||||||||
| Attached Files |  s.tgz [^] (107,419 bytes) 2011-09-14 14:13 s.c [^] (66,433 bytes) 2011-09-14 14:35 [Show Content] [Hide Content]/*
* This is a RANDOMLY GENERATED PROGRAM.
*
* Generator: csmith 2.1.0
* Git version: ea4762b
* Options: --max-array-dim 2 --max-array-len-per-dim 3 --bitfields --max-funcs 5 --no-unions --max-struct-fields 4 --no-volatiles --no-argc
* Seed: 143284654
*/
#include "csmith.h"
static long __undefined;
/* --- Struct/Union Declarations --- */
/* --- GLOBAL VARIABLES --- */
static int32_t g_3 = 0xD8C45CDBL;
static int32_t g_5 = 0x15DE05DAL;
static int32_t g_30 = 0x4A0426A7L;
static int32_t g_59 = (-1L);
static uint16_t g_70 = 0xC444L;
static int32_t g_94 = 0x3F992CE4L;
static uint8_t g_112 = 0x0FL;
static uint16_t g_121[2] = {0x2392L, 0x2392L};
static const int32_t g_139 = 0xB1200BAFL;
static uint32_t g_141 = 1UL;
static int8_t g_143 = (-2L);
static int8_t g_160 = 0x6CL;
static uint32_t g_161[1] = {4294967295UL};
static int8_t g_164 = 0x27L;
static int16_t g_182 = 5L;
static int32_t *g_190 = (void*)0;
static int16_t g_230[1] = {(-3L)};
static uint32_t g_231[3][3] = {{0x833108A3L, 0x0747FD14L, 0x833108A3L}, {0x833108A3L, 0x0747FD14L, 0x833108A3L}, {0x833108A3L, 0x0747FD14L, 0x833108A3L}};
static uint64_t g_262[3][3] = {{0UL, 0UL, 0UL}, {0UL, 0UL, 0UL}, {0UL, 0UL, 0UL}};
static uint64_t g_271[2][1] = {{18446744073709551615UL}, {18446744073709551615UL}};
static int32_t g_286 = 0x686086E3L;
static uint32_t g_287 = 0x28BB7CF6L;
static int32_t *g_294 = &g_94;
static int32_t **g_293[2] = {&g_294, &g_294};
static int32_t *** const g_292 = &g_293[1];
static uint32_t g_337 = 4294967289UL;
static uint16_t g_341 = 6UL;
static uint32_t g_346[3] = {3UL, 3UL, 3UL};
static int8_t *g_364 = &g_143;
static int8_t **g_363 = &g_364;
static uint8_t g_391 = 0x11L;
static int32_t g_400[2] = {0L, 0L};
static uint32_t **g_413 = (void*)0;
static uint32_t g_441[1] = {0xC3F769CEL};
static int16_t *g_486 = &g_230[0];
static int16_t **g_485 = &g_486;
static int16_t *** const g_484[3][3] = {{&g_485, &g_485, &g_485}, {&g_485, &g_485, &g_485}, {&g_485, &g_485, &g_485}};
static int64_t g_556 = 0x912B29C7893BD8DBLL;
static int64_t g_590 = 0x74D60928ED1CF75DLL;
static const int16_t **g_612 = (void*)0;
static const int16_t ***g_611 = &g_612;
static const int64_t *g_688 = &g_590;
static const int64_t **g_687[3] = {&g_688, &g_688, &g_688};
static int8_t ***g_694[2] = {&g_363, &g_363};
static uint16_t g_711 = 0xA51BL;
static int16_t g_731 = (-2L);
static int64_t *g_776 = (void*)0;
static int64_t **g_775 = &g_776;
static int32_t g_839 = 1L;
static int32_t *g_845 = &g_30;
static uint64_t *g_888[1] = {&g_271[0][0]};
static uint64_t **g_887 = &g_888[0];
static uint16_t *g_892 = &g_121[1];
static uint16_t *g_893 = &g_711;
static int64_t g_1043 = 8L;
static int8_t g_1045 = 0x6DL;
static int8_t ****g_1069[3][3] = {{(void*)0, &g_694[0], (void*)0}, {(void*)0, &g_694[0], (void*)0}, {(void*)0, &g_694[0], (void*)0}};
static const int32_t *g_1185 = &g_3;
static uint32_t g_1214 = 0x2276EB68L;
static uint8_t g_1238 = 0xF9L;
static int8_t * const ****g_1317 = (void*)0;
static uint64_t g_1330 = 0xBC8A7F71F50E09C5LL;
/* --- FORWARD DECLARATIONS --- */
static uint64_t func_1(void);
static int16_t func_10(int32_t * p_11, int32_t * p_12, int32_t p_13);
static int32_t func_14(int32_t * p_15, int32_t p_16, uint8_t p_17, int32_t p_18, const int32_t * p_19);
static int32_t * func_20(int32_t * p_21, int32_t * const p_22, int32_t * p_23, int16_t p_24);
static int32_t * func_25(int32_t * p_26);
/* --- FUNCTIONS --- */
/* ------------------------------------------ */
/*
* reads : g_485 g_486 g_230 g_59 g_1238 g_845 g_30 g_3 g_887 g_888 g_711 g_1185 g_400 g_164 g_892 g_121 g_364 g_271 g_839 g_294 g_94 g_292 g_293 g_5 g_231 g_190 g_112 g_1043 g_893 g_182
* writes: g_3 g_271 g_1185 g_230 g_143 g_400 g_839 g_845 g_5 g_94 g_30 g_164 g_59 g_190 g_112 g_1043 g_711 g_182
*/
static uint64_t func_1(void)
{ Frama_C_show_each_trace(0);
uint8_t l_2[1];
int32_t *l_1021[2];
int32_t *l_1024 = &g_3;
int32_t l_1039 = 0L;
uint64_t ***l_1042 = &g_887;
uint64_t l_1046 = 0x6D3EA35DDC2899C5LL;
int8_t ****l_1070 = (void*)0;
int32_t l_1096[2][3] = {{1L, 1L, 1L}, {1L, 1L, 1L}};
int8_t l_1143[2];
int16_t l_1154[2][2];
uint32_t l_1180[3][3] = {{0x99F78955L, 4294967288UL, 0x99F78955L}, {0x99F78955L, 4294967288UL, 0x99F78955L}, {0x99F78955L, 4294967288UL, 0x99F78955L}};
int32_t * const l_1212 = &g_3;
int8_t l_1248 = 0x30L;
int32_t ** const *l_1251[3];
int32_t *l_1258 = &g_30;
int8_t ***l_1274[2];
const int8_t *l_1277 = &l_1143[0];
const int8_t **l_1276 = &l_1277;
const int8_t ***l_1275 = &l_1276;
uint8_t l_1397[2];
int32_t l_1405 = (-1L);
int i, j;
for (i = 0; i < 1; i++)
l_2[i] = 9UL;
for (i = 0; i < 2; i++)
l_1021[i] = (void*)0;
for (i = 0; i < 2; i++)
l_1143[i] = 1L;
for (i = 0; i < 2; i++)
{
for (j = 0; j < 2; j++)
l_1154[i][j] = 1L;
}
for (i = 0; i < 3; i++)
l_1251[i] = &g_293[0];
for (i = 0; i < 2; i++)
l_1274[i] = (void*)0;
for (i = 0; i < 2; i++)
l_1397[i] = 0xA2L;
lbl_1259:
for (g_3 = 0; (g_3 >= 0); g_3 -= 1)
{ Frama_C_show_each_trace(3);
const int32_t *l_896 = &g_3;
int32_t l_1027 = (-1L);
const uint64_t **l_1092 = (void*)0;
const uint64_t *** const l_1091 = &l_1092;
int16_t l_1114 = 0x9572L;
int32_t l_1117[1][2];
uint64_t l_1127[3];
int32_t l_1142[3];
uint64_t l_1150 = 0x4AF05E10AC6BCFCCLL;
int16_t l_1153 = 0xD9DDL;
int16_t l_1186 = 0x3691L;
int32_t l_1187[2];
uint8_t l_1189 = 0x4CL;
int i, j;
for (i = 0; i < 1; i++)
{
for (j = 0; j < 2; j++)
l_1117[i][j] = 0L;
}
for (i = 0; i < 3; i++)
l_1127[i] = 0xB99F77A192DF21DBLL;
for (i = 0; i < 3; i++)
l_1142[i] = 0L;
for (i = 0; i < 2; i++)
l_1187[i] = 0x2CD28C41L;
}
for (l_1046 = (-29); (l_1046 > 40); ++l_1046)
{ Frama_C_show_each_trace(818);
int64_t l_1241[2];
int8_t l_1242 = 0L;
uint8_t *l_1245 = &l_2[0];
int32_t ** const **l_1252 = &l_1251[0];
int32_t ** const l_1254 = (void*)0;
int32_t ** const *l_1253 = &l_1254;
int32_t ***l_1255 = (void*)0;
int32_t ****l_1256 = &l_1255;
int32_t *l_1257 = &g_400[1];
const uint64_t *l_1265 = &g_271[0][0];
const uint64_t **l_1264 = &l_1265;
const uint64_t ***l_1263 = &l_1264;
int32_t *l_1281 = &g_30;
int32_t **l_1282 = &g_845;
int i;
for (i = 0; i < 2; i++)
l_1241[i] = (-1L);
(*l_1212) = (safe_div_func_int8_t_s_s((((**g_485) | (&g_121[1] != ((safe_div_func_int32_t_s_s((g_59 || (0xD47214DDD5B027CFLL > (g_1238 , (safe_mul_func_uint8_t_u_u(((l_1241[1] & l_1242) < l_1242), (safe_sub_func_uint32_t_u_u(l_1242, 0xF8EBDAB4L))))))), (*g_845))) , (void*)0))) || l_1242), 1L));
if ((((*l_1245)++) != (((*l_1212) |= l_1248) , (((*l_1024) > ((safe_lshift_func_int8_t_s_s(((*l_1024) < ((l_1253 = ((*l_1252) = l_1251[0])) == ((((-2L) > ((**g_887) = (*l_1024))) , (*g_845)) , ((*l_1256) = l_1255)))), func_10(l_1257, l_1258, (*l_1258)))) | 0x1F4046F145586EA7LL)) <= (*l_1024)))))
{ Frama_C_show_each_trace(826);
if (g_30)
goto lbl_1259;
}
else
{ Frama_C_show_each_trace(828);
uint64_t l_1262[2];
int32_t *l_1266[1][1];
int i, j;
for (i = 0; i < 2; i++)
l_1262[i] = 18446744073709551611UL;
for (i = 0; i < 1; i++)
{
for (j = 0; j < 1; j++)
l_1266[i][j] = &g_3;
}
for (l_1242 = 1; (l_1242 >= 0); l_1242 -= 1)
{ Frama_C_show_each_trace(831);
uint64_t ***l_1267 = &g_887;
int32_t l_1280 = 1L;
g_1185 = l_1257;
if ((g_711 | (~(safe_div_func_int8_t_s_s(0L, ((0UL || (*g_1185)) , l_1262[1]))))))
{ Frama_C_show_each_trace(833);
const int8_t ****l_1278 = &l_1275;
int32_t l_1279[3];
int i;
for (i = 0; i < 3; i++)
l_1279[i] = 9L;
(*l_1257) = (((((l_1263 != (func_10(&l_1096[0][1], l_1266[0][0], (*g_845)) , l_1267)) & ((*g_364) = (safe_add_func_int8_t_s_s(4L, (safe_rshift_func_int16_t_s_u(((*g_486) = (safe_mod_func_uint8_t_u_u((l_1274[0] != ((*l_1278) = l_1275)), g_164))), (*g_892))))))) , 0L) != (*l_1212)) || l_1279[0]);
return (**g_887);
}
else
{ Frama_C_show_each_trace(839);
for (g_839 = 0; (g_839 <= 1); g_839 += 1)
{ Frama_C_show_each_trace(842);
return l_1280;
}
}
}
}
(*l_1282) = l_1281;
}
if (((*l_1258) = (safe_lshift_func_uint8_t_u_u(func_14(&g_3, (*l_1212), g_839, (*g_294), &l_1039), 0))))
{ Frama_C_show_each_trace(851);
int32_t *l_1304[3][3] = {{&g_30, &g_3, &g_30}, {&g_30, &g_3, &g_30}, {&g_30, &g_3, &g_30}};
int8_t *** const * const l_1402 = &l_1274[0];
uint32_t *l_1409 = &g_231[1][2];
uint32_t **l_1408 = &l_1409;
int i, j;
(*l_1024) = (*l_1024);
for (g_112 = 0; (g_112 > 43); g_112 = safe_add_func_int16_t_s_s(g_112, 2))
{ Frama_C_show_each_trace(855);
int8_t * const *l_1306 = &g_364;
int32_t l_1309 = 0xF23FDABDL;
int8_t *****l_1312 = &g_1069[2][0];
uint8_t l_1344 = 0xF5L;
int32_t l_1373 = 3L;
int32_t l_1374 = (-1L);
int32_t l_1378[1];
uint64_t l_1384 = 0x8DCBB57EA0C95542LL;
int i;
for (i = 0; i < 1; i++)
l_1378[i] = 0L;
for (g_1043 = 16; (g_1043 != 10); g_1043--)
{ Frama_C_show_each_trace(858);
uint32_t l_1291 = 1UL;
uint64_t l_1316 = 0x6BEB2F8F3B3DBF6FLL;
uint32_t ***l_1345 = (void*)0;
uint8_t *l_1354 = (void*)0;
uint16_t l_1359 = 65526UL;
int64_t *l_1360 = &g_590;
uint64_t *l_1361 = &l_1046;
int32_t l_1362 = 0L;
int32_t l_1371 = 0x83D2D412L;
int32_t l_1372 = (-1L);
int32_t l_1377[1];
int64_t l_1382 = 0x448A3ED760145373LL;
int16_t l_1383 = (-3L);
int i;
for (i = 0; i < 1; i++)
l_1377[i] = (-3L);
}
}
l_1397[0]--;
(*l_1024) = (((*l_1024) >= (l_1402 != (void*)0)) | (safe_mul_func_uint16_t_u_u((*g_892), ((((*g_893) = l_1405) < (**g_485)) == (safe_rshift_func_int16_t_s_s(((*l_1024) && (l_1021[1] != ((*l_1408) = &g_346[0]))), 5))))));
}
else
{ Frama_C_show_each_trace(927);
for (g_182 = 0; (g_182 <= 1); g_182 += 1)
{ Frama_C_show_each_trace(930);
return (**g_887);
}
}
(*g_845) = ((*l_1024) = (*l_1258));
return (*l_1212);
}
/* ------------------------------------------ */
/*
* reads :
* writes:
*/
static int16_t func_10(int32_t * p_11, int32_t * p_12, int32_t p_13)
{ Frama_C_show_each_trace(678);
return p_13;
}
/* ------------------------------------------ */
/*
* reads : g_3 g_400 g_30 g_5 g_292 g_293 g_294 g_271 g_94 g_164 g_231 g_59 g_845 g_190
* writes: g_5 g_94 g_30 g_164 g_59 g_845 g_190 g_400
*/
static int32_t func_14(int32_t * p_15, int32_t p_16, uint8_t p_17, int32_t p_18, const int32_t * p_19)
{ Frama_C_show_each_trace(569);
uint64_t l_900 = 18446744073709551608UL;
int32_t l_903[3];
int8_t l_946[3];
uint16_t l_960 = 0xB212L;
int i;
for (i = 0; i < 3; i++)
l_903[i] = 0x2A3A850DL;
for (i = 0; i < 3; i++)
l_946[i] = 0x23L;
if ((*p_15))
{ Frama_C_show_each_trace(570);
uint16_t l_899 = 0xF4C5L;
int8_t l_904 = 0xC3L;
int32_t *l_905 = &g_5;
int32_t l_938 = 0xF24F9D6EL;
int32_t l_939 = (-1L);
int32_t l_942 = 0x71D17369L;
int8_t l_944 = 0xDEL;
int32_t l_947[2][2] = {{0xF31E3325L, 1L}, {0xF31E3325L, 1L}};
int32_t **l_963 = (void*)0;
int32_t **l_964 = &l_905;
int i, j;
(*l_905) |= ((((((void*)0 != (**g_292)) & p_17) , (((safe_mod_func_int64_t_s_s((l_900 = (p_16 && l_899)), ((safe_mod_func_uint32_t_u_u(l_903[0], l_899)) , l_899))) == (l_899 , 0UL)) >= 1UL)) , l_904) | g_271[0][0]);
for (g_94 = 0; (g_94 == 4); ++g_94)
{ Frama_C_show_each_trace(575);
int16_t l_918 = 1L;
int32_t l_949[2];
int32_t *l_959[3];
int i;
for (i = 0; i < 2; i++)
l_949[i] = 4L;
for (i = 0; i < 3; i++)
l_959[i] = &l_903[0];
if ((*p_15))
break;
for (g_30 = 18; (g_30 <= 14); g_30--)
{ Frama_C_show_each_trace(579);
uint16_t l_919 = 65535UL;
uint32_t l_928 = 4294967286UL;
int32_t l_941 = 2L;
int32_t l_943 = 0xA4A7804BL;
int32_t l_945 = 0x5B30C376L;
int8_t l_950[2];
int32_t l_952[3][2];
uint64_t l_953 = 18446744073709551612UL;
int i, j;
for (i = 0; i < 2; i++)
l_950[i] = (-1L);
for (i = 0; i < 3; i++)
{
for (j = 0; j < 2; j++)
l_952[i][j] = 0xA62C22E3L;
}
for (g_164 = 2; (g_164 >= 0); g_164 -= 1)
{ Frama_C_show_each_trace(582);
int8_t l_927 = 0x38L;
for (p_17 = 0; (p_17 <= 2); p_17 += 1)
{ Frama_C_show_each_trace(585);
int32_t **l_913 = &l_905;
int i, j;
(*l_905) = (g_231[p_17][g_164] < (safe_mul_func_int8_t_s_s(((safe_unary_minus_func_int16_t_s(p_17)) || p_18), (*l_905))));
(*l_913) = &p_16;
(*l_905) = (((**l_913) >= 9UL) , (*p_19));
}
for (g_59 = 7; (g_59 > (-13)); g_59--)
{ Frama_C_show_each_trace(592);
int32_t **l_916 = &g_845;
int32_t *l_917 = &l_903[0];
int32_t *l_920 = (void*)0;
int32_t l_921 = (-1L);
int32_t *l_922 = &g_400[0];
int32_t *l_923 = &g_5;
int32_t *l_924 = &l_903[0];
int32_t *l_925 = &l_921;
int32_t *l_926[2][3] = {{&g_400[1], &l_903[2], &g_400[1]}, {&g_400[1], &l_903[2], &g_400[1]}};
int i, j;
(*l_916) = &g_30;
(*l_917) ^= ((*l_905) |= (*g_845));
l_919 |= l_918;
++l_928;
}
}
for (l_918 = 0; (l_918 >= 23); l_918 = safe_add_func_int64_t_s_s(l_918, 5))
{ Frama_C_show_each_trace(602);
int32_t **l_933 = &g_190;
int32_t l_940[1];
int8_t l_951 = 0xDEL;
int i;
for (i = 0; i < 1; i++)
l_940[i] = (-1L);
(*l_933) = &g_5;
for (l_899 = 0; (l_899 == 57); l_899 = safe_add_func_int16_t_s_s(l_899, 6))
{ Frama_C_show_each_trace(606);
int32_t *l_936 = (void*)0;
int32_t *l_937[2][2];
int8_t l_948 = 0xD2L;
int i, j;
for (i = 0; i < 2; i++)
{
for (j = 0; j < 2; j++)
l_937[i][j] = &g_5;
}
--l_953;
if ((*g_190))
break;
if ((*p_15))
break;
}
for (g_5 = (-22); (g_5 > (-29)); g_5 = safe_sub_func_int8_t_s_s(g_5, 2))
{ Frama_C_show_each_trace(613);
int32_t *l_958[1];
int i;
for (i = 0; i < 1; i++)
l_958[i] = &l_952[0][1];
g_400[0] = (**l_933);
}
}
}
l_960++;
}
(*l_964) = (void*)0;
p_16 &= (*p_15);
}
else
{ Frama_C_show_each_trace(622);
uint64_t l_976 = 0x181872C8A30EEC2ELL;
const int32_t l_994 = 0xA991B84DL;
uint32_t l_999 = 18446744073709551608UL;
uint8_t *l_1000 = &g_112;
uint16_t *l_1004 = &l_960;
int32_t **l_1015 = &g_845;
for (p_17 = 0; (p_17 <= 2); p_17 += 1)
{ Frama_C_show_each_trace(625);
uint16_t l_972 = 2UL;
int32_t *l_1006[2];
int i;
for (i = 0; i < 2; i++)
l_1006[i] = &g_59;
}
(*l_1015) = &g_400[0];
(**l_1015) = 0x42E4E3B5L;
}
return (*p_15);
}
/* ------------------------------------------ */
/*
* reads : g_391 g_112 g_341 g_121 g_161 g_3 g_484 g_262 g_485 g_486 g_364 g_143 g_139 g_5 g_292 g_190 g_400 g_363 g_293 g_294 g_94 g_230 g_287 g_688 g_590 g_775 g_30 g_70 g_59 g_164 g_160 g_141 g_231 g_271 g_182 g_337 g_346 g_413 g_441
* writes: g_391 g_5 g_112 g_341 g_121 g_230 g_190 g_271 g_262 g_143 g_293 g_775 g_400 g_94 g_30 g_59 g_70 g_161 g_164 g_182 g_231 g_287 g_337 g_346 g_363 g_160 g_413 g_286 g_845 g_711 g_887 g_892 g_893
*/
static int32_t * func_20(int32_t * p_21, int32_t * const p_22, int32_t * p_23, int16_t p_24)
{ Frama_C_show_each_trace(297);
uint32_t l_474 = 0x16AE204AL;
int32_t l_493 = (-1L);
const int32_t **l_507 = (void*)0;
const int32_t ***l_506[2];
uint32_t l_514 = 0x6798A1E5L;
int32_t l_527 = 0x047D0D4DL;
uint16_t *l_529[3];
int32_t l_530 = (-1L);
int32_t l_572 = (-7L);
int32_t l_577[3];
int16_t ** const l_625 = &g_486;
int8_t *l_646 = &g_164;
int32_t l_651 = (-1L);
uint16_t l_698 = 0x3353L;
int64_t l_798 = 0x82744448365323B5LL;
int32_t *l_827 = &g_30;
int16_t l_850[1][3];
uint16_t **l_891[1][3];
int32_t l_894 = 0xA64B3498L;
int32_t *l_895 = &g_5;
int i, j;
for (i = 0; i < 2; i++)
l_506[i] = &l_507;
for (i = 0; i < 3; i++)
l_529[i] = &g_121[1];
for (i = 0; i < 3; i++)
l_577[i] = 0x58CF3274L;
for (i = 0; i < 1; i++)
{
for (j = 0; j < 3; j++)
l_850[i][j] = 0xB2C6L;
}
for (i = 0; i < 1; i++)
{
for (j = 0; j < 3; j++)
l_891[i][j] = &l_529[2];
}
lbl_504:
for (g_391 = (-6); (g_391 > 1); g_391 = safe_add_func_int32_t_s_s(g_391, 5))
{ Frama_C_show_each_trace(300);
(*p_21) = g_391;
}
for (g_112 = (-11); (g_112 == 35); g_112 = safe_add_func_int16_t_s_s(g_112, 3))
{ Frama_C_show_each_trace(305);
uint32_t l_467 = 0xA923E03BL;
uint64_t *l_477 = &g_271[1][0];
int32_t l_487 = 1L;
uint64_t *l_490 = &g_262[2][1];
uint16_t *l_491 = &g_121[1];
int32_t l_492 = 0xF4DD614EL;
for (g_341 = 28; (g_341 >= 60); g_341++)
{ Frama_C_show_each_trace(308);
uint16_t *l_461 = &g_121[1];
int16_t *l_464 = &g_230[0];
int32_t **l_465 = (void*)0;
int32_t **l_466[1];
int i;
for (i = 0; i < 1; i++)
l_466[i] = &g_190;
(*p_21) = ((++(*l_461)) | (~((*l_464) = p_24)));
g_190 = &g_59;
--l_467;
}
l_492 = (safe_mod_func_int8_t_s_s((safe_sub_func_int16_t_s_s(l_474, (safe_lshift_func_uint16_t_u_s((((g_161[0] ^ ((*p_23) , l_467)) ^ ((*l_477) = p_24)) != (((g_161[0] <= ((**g_485) = ((safe_mod_func_int32_t_s_s((safe_sub_func_uint16_t_u_u(((*l_491) = (((*l_490) = (((safe_add_func_uint32_t_u_u((l_487 = ((void*)0 != g_484[1][2])), (safe_sub_func_int64_t_s_s(g_262[2][1], 0x5366F19421CC5B27LL)))) , l_474) >= 0x3613L)) != p_24)), l_467)), p_24)) <= 0x642235E8L))) >= p_24) & 7UL)), 14)))), p_24));
}
if (l_493)
{ Frama_C_show_each_trace(322);
uint64_t *l_502 = (void*)0;
int32_t l_503 = 0xBDCAAD3AL;
int32_t ***l_505 = &g_293[1];
int32_t *l_508 = &g_30;
int32_t l_509[2];
int32_t *l_510 = &g_59;
int32_t *l_511 = &g_59;
int32_t *l_512 = &g_5;
int32_t *l_513[1][1];
uint32_t l_635 = 1UL;
int8_t l_640[2][2] = {{0xADL, 0x6CL}, {0xADL, 0x6CL}};
int16_t l_690[2];
int64_t l_730 = 1L;
int i, j;
for (i = 0; i < 2; i++)
l_509[i] = 0x1D7B26AEL;
for (i = 0; i < 1; i++)
{
for (j = 0; j < 1; j++)
l_513[i][j] = &g_30;
}
for (i = 0; i < 2; i++)
l_690[i] = 0xBBB0L;
if ((safe_mul_func_int32_t_s_s((safe_mod_func_int16_t_s_s(p_24, (safe_mul_func_int8_t_s_s(((*g_364) &= 0xDCL), 255UL)))), ((g_121[0] < (g_271[0][0] = (safe_lshift_func_int8_t_s_s(p_24, 7)))) < ((**g_485) = l_503)))))
{ Frama_C_show_each_trace(326);
(*p_21) ^= g_139;
}
else
{ Frama_C_show_each_trace(328);
if (g_3)
goto lbl_504;
(*p_21) = (((((g_3 >= p_24) , (-1L)) || 0L) , l_505) != l_506[1]);
}
++l_514;
for (g_112 = 17; (g_112 < 18); g_112 = safe_add_func_uint16_t_u_u(g_112, 6))
{ Frama_C_show_each_trace(335);
int32_t l_528 = 1L;
const int32_t l_550 = (-1L);
int32_t l_563 = (-2L);
int32_t l_564 = 0xA65F8173L;
int32_t l_566 = 0L;
int32_t l_574[3][3];
uint8_t l_578[1][3];
const int16_t *l_610[2];
const int16_t **l_609 = &l_610[0];
const int16_t ***l_608[2];
int64_t l_618[1][3];
int16_t l_632 = 0x6027L;
int16_t l_662 = 0xB103L;
uint32_t ***l_747 = &g_413;
uint32_t *l_760[1];
int64_t *l_761 = (void*)0;
int64_t *l_762[3][2];
uint32_t ***l_764 = &g_413;
uint32_t ****l_763 = &l_764;
int i, j;
for (i = 0; i < 3; i++)
{
for (j = 0; j < 3; j++)
l_574[i][j] = 1L;
}
for (i = 0; i < 1; i++)
{
for (j = 0; j < 3; j++)
l_578[i][j] = 0xBBL;
}
for (i = 0; i < 2; i++)
l_610[i] = &g_230[0];
for (i = 0; i < 2; i++)
l_608[i] = &l_609;
for (i = 0; i < 1; i++)
{
for (j = 0; j < 3; j++)
l_618[i][j] = 0x0BE2BBF9F6374DB5LL;
}
for (i = 0; i < 1; i++)
l_760[i] = &g_287;
for (i = 0; i < 3; i++)
{
for (j = 0; j < 2; j++)
l_762[i][j] = &g_590;
}
}
l_510 = &g_400[0];
}
else
{ Frama_C_show_each_trace(478);
int32_t **l_767 = &g_294;
int64_t *l_768 = (void*)0;
int32_t l_771 = (-10L);
int32_t l_788 = 0xF674CDFEL;
int32_t l_813 = 0x34793382L;
int32_t l_814[1][2];
const uint32_t l_844 = 1UL;
int32_t **l_880[3][1];
uint64_t *l_885 = &g_262[2][1];
uint64_t **l_884 = &l_885;
uint64_t ***l_886[1][3];
int i, j;
for (i = 0; i < 1; i++)
{
for (j = 0; j < 2; j++)
l_814[i][j] = 0xC38BC804L;
}
for (i = 0; i < 3; i++)
{
for (j = 0; j < 1; j++)
l_880[i][j] = &l_827;
}
for (i = 0; i < 1; i++)
{
for (j = 0; j < 3; j++)
l_886[i][j] = (void*)0;
}
if (((safe_div_func_int64_t_s_s(((-1L) || (((l_530 = ((l_577[0] , ((*g_292) = l_767)) == &g_294)) | ((safe_lshift_func_int16_t_s_u(l_771, 14)) ^ (-8L))) ^ l_572)), 1UL)) , ((*p_21) = (*p_21))))
{ Frama_C_show_each_trace(482);
int32_t l_772 = 0L;
l_772 = (~(*p_21));
}
else
{ Frama_C_show_each_trace(484);
int32_t **l_773[3];
int64_t **l_774 = &l_768;
uint32_t *l_799 = &g_141;
int32_t l_828 = 0L;
int i;
for (i = 0; i < 3; i++)
l_773[i] = &g_190;
g_190 = &g_400[0];
g_775 = l_774;
if ((*g_190))
{ Frama_C_show_each_trace(487);
int16_t l_779 = 0x142BL;
int32_t l_802[3];
int32_t l_838 = 9L;
int i;
for (i = 0; i < 3; i++)
l_802[i] = (-10L);
(*g_190) = (0UL && ((*g_364) = (p_24 , (*g_364))));
if (((safe_div_func_int16_t_s_s((l_779 <= 0x3798CDC8FE646501LL), (l_577[0] , (safe_mod_func_uint64_t_u_u(((l_771 = l_779) > (safe_add_func_int8_t_s_s(p_24, (~(**g_363))))), (safe_rshift_func_int8_t_s_u(p_24, 7))))))) ^ (((***g_292) |= (safe_mul_func_int16_t_s_s(l_698, (l_651 | p_24)))) , l_788)))
{ Frama_C_show_each_trace(492);
uint32_t l_789 = 4294967295UL;
(*p_21) = l_789;
return &g_30;
}
else
{ Frama_C_show_each_trace(495);
int32_t l_800 = 0xB7B00C8FL;
int32_t l_801 = 1L;
int32_t l_811 = (-5L);
int32_t l_812[2][2];
uint32_t l_815 = 0x3498FE5BL;
int32_t l_840 = 0x37168384L;
int i, j;
for (i = 0; i < 2; i++)
{
for (j = 0; j < 2; j++)
l_812[i][j] = 0x4A74A583L;
}
l_802[0] &= ((safe_sub_func_uint64_t_u_u((safe_div_func_int32_t_s_s(((safe_mod_func_uint16_t_u_u(((*g_364) , ((safe_sub_func_uint8_t_u_u(l_698, ((l_798 , l_799) != ((((l_800 = 0UL) == l_801) > (*g_486)) , p_22)))) && l_514)), g_287)) > p_24), l_771)), p_24)) , (*g_190));
if ((*g_190))
{ Frama_C_show_each_trace(498);
(*p_21) = (safe_lshift_func_uint8_t_u_s((safe_mul_func_uint16_t_u_u(65529UL, ((safe_unary_minus_func_int16_t_s(p_24)) | (safe_mul_func_uint16_t_u_u((l_788 = ((*g_688) != ((*g_775) == (void*)0))), 0UL))))), 4));
}
else
{ Frama_C_show_each_trace(501);
int32_t l_810 = (-9L);
int32_t l_829 = 0x09F318F1L;
int32_t l_830 = (-1L);
int32_t l_831 = 0x24D53C66L;
int32_t l_832 = 0x6E812EF7L;
int64_t l_833 = (-1L);
int32_t l_834 = 0x0A6F1039L;
int32_t l_835 = 0x9B563BF4L;
int32_t l_836 = 0x8E59058FL;
int32_t l_837[2];
uint8_t l_841 = 1UL;
int i;
for (i = 0; i < 2; i++)
l_837[i] = (-10L);
l_815--;
if (p_24)
goto lbl_826;
lbl_826:
(*g_190) = (safe_add_func_int32_t_s_s(0xA863986EL, (safe_sub_func_uint16_t_u_u((safe_mul_func_int8_t_s_s((safe_mul_func_uint8_t_u_u(p_24, 0x08L)), p_24)), l_802[0]))));
l_827 = (g_190 = p_21);
++l_841;
}
(*g_190) = (*g_190);
}
if ((l_844 || 0x0E2BF874L))
{ Frama_C_show_each_trace(511);
int64_t l_846 = 5L;
p_21 = func_25(&g_400[0]);
g_845 = (g_190 = p_23);
l_846 = (*p_23);
(*l_827) = 0L;
}
else
{ Frama_C_show_each_trace(517);
return p_21;
}
p_23 = ((safe_unary_minus_func_uint32_t_u(p_24)) , (void*)0);
}
else
{ Frama_C_show_each_trace(521);
uint32_t l_862 = 6UL;
int32_t l_869[3][3];
uint64_t l_873 = 0x1B171DA6ED2ABC60LL;
int32_t *l_877 = &g_59;
int i, j;
for (i = 0; i < 3; i++)
{
for (j = 0; j < 3; j++)
l_869[i][j] = 7L;
}
for (g_5 = 0; (g_5 < 2); g_5++)
{ Frama_C_show_each_trace(524);
uint32_t l_851 = 1UL;
--l_851;
}
if ((+l_771))
{ Frama_C_show_each_trace(527);
int8_t l_858 = 0xFAL;
(*p_21) ^= ((p_24 >= (safe_sub_func_int8_t_s_s((safe_mul_func_int16_t_s_s(p_24, (g_711 = 0xE467L))), (((p_24 < ((0xA029B0CAL <= ((p_24 , l_788) != l_844)) , g_287)) , 0x0EF6D901L) & (*l_827))))) && l_858);
for (g_341 = (-13); (g_341 >= 49); g_341 = safe_add_func_uint8_t_u_u(g_341, 9))
{ Frama_C_show_each_trace(532);
return p_21;
}
if ((p_24 == p_24))
{ Frama_C_show_each_trace(535);
return &g_30;
}
else
{ Frama_C_show_each_trace(537);
int64_t l_861 = (-1L);
++l_862;
g_190 = &l_527;
g_845 = (p_24 , (void*)0);
}
}
else
{ Frama_C_show_each_trace(542);
int64_t l_866 = 0xD26A196467FAD3A9LL;
int32_t l_870[1];
int16_t l_872 = 0L;
int i;
for (i = 0; i < 1; i++)
l_870[i] = (-1L);
if (l_788)
{ Frama_C_show_each_trace(543);
int32_t *l_865 = &g_30;
int32_t l_867 = 0x6250BCF7L;
int32_t l_868 = 0x3E02EA48L;
int32_t l_871 = 9L;
p_23 = func_25(l_865);
l_873++;
(*l_865) |= (l_862 < l_862);
}
else
{ Frama_C_show_each_trace(547);
int32_t *l_876[2];
int i;
for (i = 0; i < 2; i++)
l_876[i] = (void*)0;
l_876[0] = p_21;
return &g_400[0];
}
return &g_3;
}
l_877 = p_21;
(*l_877) |= (safe_div_func_int16_t_s_s((*l_827), p_24));
}
}
p_21 = func_25(&g_400[0]);
for (g_164 = 7; (g_164 < 6); g_164 = safe_sub_func_int8_t_s_s(g_164, 3))
{ Frama_C_show_each_trace(560);
int32_t *l_883 = &l_771;
return &g_5;
}
g_887 = l_884;
}
l_894 |= ((((safe_div_func_uint64_t_u_u((*l_827), (*l_827))) , (g_892 = &l_698)) != (g_893 = &g_70)) ^ 0xBD1DL);
return l_895;
}
/* ------------------------------------------ */
/*
* reads : g_3 g_30 g_5 g_70 g_59 g_112 g_94 g_121 g_143 g_161 g_164 g_139 g_160 g_141 g_190 g_231 g_271 g_287 g_292 g_262 g_182 g_337 g_341 g_346 g_293 g_294 g_363 g_391 g_364 g_400 g_230 g_413 g_441
* writes: g_5 g_30 g_59 g_70 g_94 g_112 g_121 g_143 g_161 g_164 g_182 g_190 g_231 g_271 g_287 g_337 g_341 g_346 g_363 g_160 g_391 g_400 g_413 g_286 g_230
*/
static int32_t * func_25(int32_t * p_26)
{ Frama_C_show_each_trace(6);
uint32_t l_36 = 8UL;
int32_t l_96 = (-7L);
int32_t *l_183 = (void*)0;
uint8_t l_219 = 255UL;
int8_t l_238 = 1L;
uint8_t l_270 = 253UL;
int32_t l_281 = 0x6584DEB0L;
int32_t l_282 = 0x724B863AL;
int16_t *l_301 = &g_230[0];
int16_t **l_300 = &l_301;
int16_t ***l_299[3];
int32_t *l_316 = (void*)0;
int16_t l_340[1][2];
uint16_t l_351 = 0xF301L;
uint32_t *l_452 = &g_161[0];
int i, j;
for (i = 0; i < 3; i++)
l_299[i] = &l_300;
for (i = 0; i < 1; i++)
{
for (j = 0; j < 2; j++)
l_340[i][j] = 0x4518L;
}
lbl_75:
for (g_5 = (-19); (g_5 < (-3)); g_5++)
{ Frama_C_show_each_trace(9);
int32_t *l_29 = &g_30;
int32_t *l_31 = &g_30;
int32_t *l_32 = &g_30;
int32_t l_33 = 0x494ABC24L;
int32_t *l_34 = &l_33;
int32_t *l_35[2][1];
uint8_t l_39 = 4UL;
int i, j;
for (i = 0; i < 2; i++)
{
for (j = 0; j < 1; j++)
l_35[i][j] = &l_33;
}
if (g_3)
break;
++l_36;
--l_39;
}
for (g_30 = 0; (g_30 != (-7)); --g_30)
{ Frama_C_show_each_trace(16);
int32_t *l_58 = &g_59;
uint16_t *l_68 = (void*)0;
uint16_t *l_69 = &g_70;
int32_t l_71[1][2];
int32_t *l_72 = &l_71[0][1];
uint32_t l_180 = 0xA1647F7CL;
int32_t *l_192[2];
int32_t **l_191 = &l_192[1];
int8_t *l_253 = (void*)0;
int8_t *l_255 = &g_164;
uint64_t *l_261 = &g_262[2][1];
uint32_t l_302 = 0x2C5786C6L;
int8_t l_315 = 0xEFL;
int32_t *l_318 = (void*)0;
int32_t *l_319[1][2];
int32_t l_320[2][1];
int16_t l_336 = 6L;
int32_t **l_408 = &l_72;
int32_t **l_409 = &l_58;
int32_t *l_422 = &l_71[0][1];
int i, j;
for (i = 0; i < 1; i++)
{
for (j = 0; j < 2; j++)
l_71[i][j] = 0xDEF05DE0L;
}
for (i = 0; i < 2; i++)
l_192[i] = &g_94;
for (i = 0; i < 1; i++)
{
for (j = 0; j < 2; j++)
l_319[i][j] = &l_71[0][0];
}
for (i = 0; i < 2; i++)
{
for (j = 0; j < 1; j++)
l_320[i][j] = 0x47A76EE4L;
}
if ((safe_add_func_uint64_t_u_u((safe_mul_func_uint16_t_u_u(l_36, g_30)), (safe_div_func_int64_t_s_s((g_5 != ((-1L) <= g_5)), (safe_rshift_func_int8_t_s_u((safe_mod_func_int32_t_s_s((safe_sub_func_int32_t_s_s(((*l_58) = l_36), (!l_36))), (safe_lshift_func_uint16_t_u_s((((*l_72) = (((safe_mod_func_int64_t_s_s(g_3, ((((safe_mod_func_uint16_t_u_u(((*l_69) = (!0x3883L)), 0xDCDAL)) != l_36) <= l_36) && l_36))) ^ l_71[0][0]) > 0UL)) != 0xCFB861A7L), l_36)))), l_36)))))))
{ Frama_C_show_each_trace(20);
int8_t l_80 = 4L;
int32_t *l_93 = &g_94;
int32_t **l_95 = &l_72;
int8_t *l_109 = &l_80;
uint8_t *l_110 = (void*)0;
uint8_t *l_111 = &g_112;
uint16_t *l_119 = (void*)0;
uint16_t *l_120 = &g_121[1];
int32_t l_142 = 0x13A23B15L;
for (g_70 = 0; (g_70 < 54); g_70 = safe_add_func_int8_t_s_s(g_70, 7))
{ Frama_C_show_each_trace(23);
int64_t l_83[2][2] = {{(-10L), (-1L)}, {(-10L), (-1L)}};
int32_t *l_90[3][1];
int i, j;
for (i = 0; i < 3; i++)
{
for (j = 0; j < 1; j++)
l_90[i][j] = &l_71[0][0];
}
if (l_36)
goto lbl_75;
if (g_70)
goto lbl_75;
(*l_72) = (safe_mul_func_uint16_t_u_u((safe_div_func_uint16_t_u_u(l_80, ((safe_div_func_uint64_t_u_u(l_83[0][0], g_59)) , (((safe_add_func_uint64_t_u_u(((safe_rshift_func_int8_t_s_s(((l_36 >= (g_3 && l_80)) & (*p_26)), 4)) , g_30), (safe_div_func_uint16_t_u_u(((void*)0 != l_90[0][0]), l_36)))) , g_5) , g_70)))), (-1L)));
if (l_36)
break;
}
l_96 &= (g_30 , ((((0x00F1D91AL && (safe_sub_func_uint32_t_u_u((((*l_93) = g_30) , 0x00AF4084L), (((((void*)0 != p_26) , &g_30) == ((*l_95) = p_26)) != (*l_58))))) == (*l_58)) < g_5) < 1L));
g_5 &= ((safe_lshift_func_uint8_t_u_s(g_30, 7)) , (safe_mod_func_int64_t_s_s((~(safe_lshift_func_uint8_t_u_u((safe_sub_func_uint8_t_u_u((safe_add_func_int8_t_s_s(0x0BL, ((safe_rshift_func_int8_t_s_s(((*l_58) & ((*l_109) = g_70)), 0)) == 1L))), (++(*l_111)))), 6))), ((safe_div_func_uint8_t_u_u(((*l_58) || (safe_lshift_func_int16_t_s_u((**l_95), ((*l_120) = (**l_95))))), (safe_mul_func_uint8_t_u_u(g_30, (**l_95))))) , (**l_95)))));
for (l_36 = (-9); (l_36 < 14); l_36++)
{ Frama_C_show_each_trace(38);
int32_t l_130 = 0x261C1CA3L;
for (g_5 = 0; (g_5 == 25); g_5++)
{ Frama_C_show_each_trace(41);
int16_t l_132 = 0x12D9L;
if (g_94)
break;
for (g_94 = 0; (g_94 >= (-15)); --g_94)
{ Frama_C_show_each_trace(45);
const int32_t *l_138 = &g_139;
const int32_t **l_137 = &l_138;
uint32_t *l_140[1][1];
int i, j;
for (i = 0; i < 1; i++)
{
for (j = 0; j < 1; j++)
l_140[i][j] = &g_141;
}
g_143 ^= (g_94 <= (g_121[1] & (l_130 < (g_59 , ((((safe_unary_minus_func_int32_t_s((*p_26))) , g_121[1]) , l_132) , (l_142 = (safe_lshift_func_uint8_t_u_s(((*l_111) |= (safe_add_func_int32_t_s_s((((*l_137) = ((*p_26) , &g_94)) != &g_94), 0xE2A06A03L))), g_70))))))));
}
for (l_130 = 24; (l_130 == (-25)); l_130 = safe_sub_func_int32_t_s_s(l_130, 6))
{ Frama_C_show_each_trace(53);
int32_t l_146[1][1];
int i, j;
for (i = 0; i < 1; i++)
{
for (j = 0; j < 1; j++)
l_146[i][j] = 0x7D9658AAL;
}
l_146[0][0] = 4L;
if ((*p_26))
continue;
if (g_3)
break;
}
if (((safe_rshift_func_int16_t_s_s(l_132, (safe_rshift_func_int16_t_s_s((safe_rshift_func_uint16_t_u_u(((*l_120) = 0x34EFL), (0xADB2L < ((safe_sub_func_int8_t_s_s((**l_95), (safe_sub_func_int16_t_s_s(2L, (*l_72))))) || 9L)))), 6)))) <= (**l_95)))
{ Frama_C_show_each_trace(59);
int32_t *l_157 = (void*)0;
int32_t *l_158 = &l_130;
int32_t *l_159[2];
int i;
for (i = 0; i < 2; i++)
l_159[i] = (void*)0;
++g_161[0];
}
else
{ Frama_C_show_each_trace(61);
g_164 &= ((*l_58) = l_130);
}
}
(*l_58) = (((*l_58) < g_139) & (((-4L) | (g_143 < (((*l_69) = (*l_58)) < (g_121[1]++)))) <= g_143));
}
}
else
{ Frama_C_show_each_trace(70);
uint32_t l_168[3][1];
const int32_t l_169 = (-7L);
int32_t *l_184 = &g_5;
int32_t l_215 = 0x11A4FFB4L;
uint8_t l_216 = 255UL;
int32_t l_277 = 1L;
int32_t l_279 = 0x6541942EL;
int32_t l_280 = 1L;
int32_t l_285 = 0xC8567E17L;
int32_t * const *l_291 = &l_192[1];
int32_t * const **l_290 = &l_291;
int i, j;
for (i = 0; i < 3; i++)
{
for (j = 0; j < 1; j++)
l_168[i][j] = 0UL;
}
if (l_96)
{ Frama_C_show_each_trace(71);
int8_t *l_167 = &g_164;
l_96 &= (((g_160 , ((g_160 , g_141) , ((*p_26) | g_94))) != (0UL || (((l_168[2][0] = ((*l_167) = (g_143 = g_5))) != ((l_169 == l_36) , g_161[0])) > l_169))) , g_3);
if (l_168[1][0])
continue;
if (g_3)
goto lbl_75;
}
else
{ Frama_C_show_each_trace(78);
int32_t *l_171 = (void*)0;
int32_t **l_170 = &l_171;
int32_t l_172[2];
int32_t *l_186[2][3] = {{&g_5, &g_5, &g_59}, {&g_5, &g_5, &g_59}};
int i, j;
for (i = 0; i < 2; i++)
l_172[i] = (-8L);
if ((g_161[0] , (((*l_58) , (void*)0) == ((*l_170) = p_26))))
{ Frama_C_show_each_trace(80);
int32_t l_173 = 0x47421FA5L;
int16_t *l_181 = &g_182;
(*l_72) |= (g_5 & l_172[0]);
g_5 ^= (((l_173 , l_36) , (g_121[1] & (safe_mul_func_uint16_t_u_u(((&l_36 != ((safe_mod_func_int8_t_s_s(((((*l_58) = (l_96 , (1UL & (g_164 = g_121[1])))) > ((*l_181) = ((safe_sub_func_uint8_t_u_u(g_3, (((l_180 , l_96) < l_96) == g_141))) ^ g_112))) , g_30), l_36)) , p_26)) >= g_30), l_173)))) | l_168[1][0]);
if ((g_5 || g_30))
{ Frama_C_show_each_trace(86);
return l_183;
}
else
{ Frama_C_show_each_trace(88);
int32_t **l_185 = (void*)0;
int32_t **l_187[1];
int i;
for (i = 0; i < 1; i++)
l_187[i] = &l_72;
p_26 = (l_186[0][0] = l_184);
}
return p_26;
}
else
{ Frama_C_show_each_trace(93);
int32_t **l_188 = &l_183;
int32_t **l_189[2][1];
int i, j;
for (i = 0; i < 2; i++)
{
for (j = 0; j < 1; j++)
l_189[i][j] = (void*)0;
}
g_190 = ((*l_188) = &g_5);
}
}
if ((((g_121[1] || (g_161[0] , (~(*l_184)))) & ((void*)0 == l_191)) & ((*l_58) = (~(safe_lshift_func_int16_t_s_u(0x8E98L, ((*l_69) = g_121[1])))))))
{ Frama_C_show_each_trace(100);
int64_t l_202 = 1L;
int32_t l_204 = 4L;
int32_t *l_207[3];
int i;
for (i = 0; i < 3; i++)
l_207[i] = &g_59;
for (g_112 = 0; (g_112 < 10); g_112 = safe_add_func_uint32_t_u_u(g_112, 1))
{ Frama_C_show_each_trace(103);
uint64_t l_199 = 0x3B27F04C0B57B2B2LL;
uint64_t *l_203[2];
uint32_t *l_217 = &l_168[2][0];
int16_t **l_223 = (void*)0;
int i;
for (i = 0; i < 2; i++)
l_203[i] = &l_199;
if ((safe_sub_func_int8_t_s_s((l_199 && ((*l_69) = (safe_add_func_int8_t_s_s((l_202 != (((*l_184) , (l_204 = (*l_184))) , 0x1D7CL)), (safe_lshift_func_int16_t_s_s((*l_184), 6)))))), 1L)))
{ Frama_C_show_each_trace(106);
(*l_58) ^= (*p_26);
}
else
{ Frama_C_show_each_trace(108);
int64_t l_212 = 0x962BC75856559E35LL;
l_207[0] = (g_190 = &g_59);
(*l_184) &= ((safe_sub_func_int32_t_s_s((safe_lshift_func_uint8_t_u_s(l_199, 2)), (*g_190))) > (*l_72));
if (l_199)
goto lbl_75;
(*l_184) = l_212;
}
l_215 |= (0x2C3DD90FL | (+((*l_184) >= (safe_mod_func_int16_t_s_s(g_161[0], l_199)))));
if ((((*l_217) = l_216) , g_141))
{ Frama_C_show_each_trace(117);
uint64_t l_218 = 0x8CFFC910CF37CF8FLL;
if (l_218)
break;
if ((*p_26))
continue;
if (l_199)
break;
if (l_219)
break;
}
else
{ Frama_C_show_each_trace(122);
int16_t *l_222 = &g_182;
int16_t **l_221 = &l_222;
int16_t ***l_220[2][2] = {{&l_221, &l_221}, {&l_221, &l_221}};
int32_t **l_224 = (void*)0;
int32_t **l_225 = &l_207[0];
int i, j;
l_223 = (l_199 , (void*)0);
(*l_225) = &g_5;
}
for (l_204 = 0; (l_204 <= 15); l_204++)
{ Frama_C_show_each_trace(128);
int32_t **l_228 = &l_192[1];
int32_t ***l_229 = &l_228;
(*l_229) = l_228;
}
}
--g_231[1][2];
}
else
{ Frama_C_show_each_trace(133);
uint32_t *l_241 = &l_180;
int8_t *l_252 = (void*)0;
uint32_t l_256 = 0UL;
int32_t l_283 = 7L;
int32_t l_284 = (-8L);
int32_t **l_317[1];
int i;
for (i = 0; i < 1; i++)
l_317[i] = &l_184;
if (((safe_sub_func_uint8_t_u_u(g_161[0], ((safe_sub_func_int8_t_s_s(0x11L, g_5)) || (l_238 , (safe_mod_func_int32_t_s_s(0xB097E5DDL, ((*l_241) |= g_161[0]))))))) > (*l_58)))
{ Frama_C_show_each_trace(135);
uint8_t l_247 = 0xEAL;
int8_t **l_254[3][2];
int32_t l_278 = (-1L);
int16_t *l_295[2];
int i, j;
for (i = 0; i < 3; i++)
{
for (j = 0; j < 2; j++)
l_254[i][j] = &l_253;
}
for (i = 0; i < 2; i++)
l_295[i] = &g_230[0];
for (l_215 = 5; (l_215 < 0); l_215 = safe_sub_func_uint32_t_u_u(l_215, 9))
{ Frama_C_show_each_trace(138);
int32_t **l_244[3];
int i;
for (i = 0; i < 3; i++)
l_244[i] = &l_183;
(*l_58) |= (*p_26);
l_184 = &g_5;
if ((*p_26))
break;
}
if (((g_231[2][0] | (0x6E0FL != (safe_mod_func_int8_t_s_s(((l_247 >= ((safe_add_func_uint16_t_u_u(((*l_69) &= (((safe_lshift_func_int8_t_s_s(0x07L, (*l_184))) , ((*l_184) , l_252)) == (l_255 = l_253))), l_247)) , g_112)) ^ g_112), l_256)))) , 1L))
{ Frama_C_show_each_trace(145);
uint16_t l_265 = 0xCE40L;
(*l_58) = (safe_rshift_func_int8_t_s_u(((safe_mod_func_uint8_t_u_u((l_261 == ((l_247 , 3L) , l_261)), l_247)) == (safe_sub_func_uint32_t_u_u(l_265, (((((l_270 = ((((safe_add_func_uint8_t_u_u((safe_rshift_func_uint8_t_u_u(((l_256 , (*l_72)) , 255UL), 7)), 8UL)) | 0x4DABL) || g_141) , (*l_72))) || (-4L)) || l_256) < g_59) && g_3)))), (*l_72)));
l_58 = &g_3;
}
else
{ Frama_C_show_each_trace(149);
int32_t **l_274 = &l_72;
int32_t *l_275 = &g_59;
int32_t *l_276[3][3] = {{&l_96, (void*)0, &l_96}, {&l_96, (void*)0, &l_96}, {&l_96, (void*)0, &l_96}};
int i, j;
--g_271[0][0];
if (l_247)
continue;
(*l_274) = p_26;
++g_287;
}
(*l_184) ^= ((g_231[1][1] || 5UL) >= (l_278 |= (l_290 == g_292)));
}
else
{ Frama_C_show_each_trace(157);
int16_t *l_298 = &g_182;
int16_t **l_297[2];
int16_t ***l_296 = &l_297[1];
uint32_t l_303[1];
int i;
for (i = 0; i < 2; i++)
l_297[i] = &l_298;
for (i = 0; i < 1; i++)
l_303[i] = 0x71BF1117L;
(*l_184) = (((l_296 == l_299[2]) != g_231[2][1]) <= ((((g_143 = l_302) && (((((*l_58) < 0x0110L) , ((void*)0 != p_26)) != (-9L)) < 4294967286UL)) || 0x1989L) != (*l_184)));
if (l_283)
{ Frama_C_show_each_trace(160);
(*l_184) = (((*l_241) = (g_143 ^ 1L)) ^ ((l_303[0] , l_303[0]) , (0x371AC1D6L & (*p_26))));
}
else
{ Frama_C_show_each_trace(163);
(*l_58) |= (*p_26);
}
if (g_160)
goto lbl_75;
for (l_282 = 0; (l_282 < 6); l_282 = safe_add_func_uint64_t_u_u(l_282, 9))
{ Frama_C_show_each_trace(169);
int32_t l_308 = (-1L);
uint8_t *l_311 = (void*)0;
uint8_t *l_312 = (void*)0;
uint8_t *l_313 = (void*)0;
uint8_t *l_314[3][2] = {{(void*)0, &l_270}, {(void*)0, &l_270}, {(void*)0, &l_270}};
int i, j;
(*l_58) = l_303[0];
(*l_58) = l_303[0];
if (g_161[0])
break;
l_283 |= ((((*l_72) || ((safe_rshift_func_int16_t_s_u(g_70, ((*l_72) || (l_315 = (((l_308 == ((*p_26) , ((safe_lshift_func_int16_t_s_u((((*l_184) , ((void*)0 == &l_308)) < g_262[2][2]), g_262[2][1])) == 0x5CE1L))) >= (*l_72)) && 255UL))))) , 0xDDL)) ^ g_59) | g_161[0]);
}
}
g_190 = l_316;
if (g_5)
goto lbl_75;
}
(*l_184) = (*p_26);
}
if ((l_320[0][0] = (l_282 = (*p_26))))
{ Frama_C_show_each_trace(184);
const uint64_t l_327 = 0x6EDBF72F53F702E6LL;
int32_t l_344 = 0x44FA07D2L;
int32_t l_345 = 0L;
if ((safe_mod_func_int8_t_s_s((((safe_lshift_func_int8_t_s_s((((g_59 = ((safe_add_func_int8_t_s_s((l_327 ^ ((safe_add_func_uint32_t_u_u(g_143, ((safe_div_func_uint32_t_u_u(g_182, l_327)) , (*l_72)))) & (safe_unary_minus_func_int16_t_s((l_327 <= (((safe_add_func_int8_t_s_s((0x63L ^ l_327), (g_164 = (g_287 | (*l_72))))) < l_327) , g_287)))))), 0UL)) || g_121[1])) , &l_319[0][0]) == (void*)0), l_327)) != g_262[0][0]) > l_327), 0x46L)))
{ Frama_C_show_each_trace(187);
int16_t l_335 = 0xE1FFL;
g_337++;
g_341++;
g_346[2]--;
return &g_30;
}
else
{ Frama_C_show_each_trace(192);
uint16_t l_360[2][1];
int32_t l_366 = 7L;
int32_t l_367 = 3L;
int i, j;
for (i = 0; i < 2; i++)
{
for (j = 0; j < 1; j++)
l_360[i][j] = 0x02F3L;
}
for (l_315 = 12; (l_315 >= 1); l_315 = safe_sub_func_int8_t_s_s(l_315, 1))
{ Frama_C_show_each_trace(195);
int16_t l_355[3];
uint8_t *l_356 = &l_219;
int32_t *l_359[3][1];
int8_t **l_361 = &l_253;
int8_t ***l_362 = &l_361;
int8_t ***l_365 = &g_363;
int i, j;
for (i = 0; i < 3; i++)
l_355[i] = (-5L);
for (i = 0; i < 3; i++)
{
for (j = 0; j < 1; j++)
l_359[i][j] = (void*)0;
}
l_351 &= g_164;
l_367 = ((safe_unary_minus_func_uint64_t_u(((l_355[1] > (l_327 >= (((l_360[0][0] = ((***g_292) = ((g_160 <= ((*l_356)--)) || (l_359[1][0] != (void*)0)))) , 6UL) && (l_366 &= ((((((*l_362) = l_361) != ((*l_365) = g_363)) && (*l_58)) , (void*)0) != (void*)0))))) < (-3L)))) == g_70);
if ((*p_26))
break;
}
}
for (g_182 = 0; (g_182 <= (-6)); g_182 = safe_sub_func_int32_t_s_s(g_182, 8))
{ Frama_C_show_each_trace(209);
uint16_t l_374 = 65533UL;
int32_t l_389 = 0x985A4F54L;
int32_t l_390[2][1];
int32_t ** const l_401 = &l_316;
int i, j;
for (i = 0; i < 2; i++)
{
for (j = 0; j < 1; j++)
l_390[i][j] = 5L;
}
for (g_160 = 0; (g_160 >= 0); g_160 -= 1)
{ Frama_C_show_each_trace(212);
int i, j;
g_59 ^= (safe_add_func_int64_t_s_s(g_271[(g_160 + 1)][g_160], g_160));
return p_26;
}
if (((safe_add_func_uint64_t_u_u(l_374, (safe_sub_func_uint32_t_u_u(0xE944D6ADL, (safe_rshift_func_int16_t_s_u(0L, l_327)))))) != l_374))
{ Frama_C_show_each_trace(216);
int16_t **l_385[2];
int32_t l_388 = 0L;
int i;
for (i = 0; i < 2; i++)
l_385[i] = (void*)0;
for (g_287 = 0; (g_287 <= 0); g_287 += 1)
{ Frama_C_show_each_trace(219);
return &g_3;
}
g_5 |= (safe_rshift_func_uint16_t_u_s(l_374, (((safe_rshift_func_int16_t_s_u((safe_div_func_uint64_t_u_u(l_374, (g_341 | (*p_26)))), (l_385[1] != (void*)0))) , (safe_lshift_func_int16_t_s_u(0x0D9CL, g_160))) < l_388)));
--g_391;
}
else
{ Frama_C_show_each_trace(224);
int32_t * const l_399[2] = {&g_400[0], &g_400[0]};
int32_t * const *l_398 = &l_399[1];
int32_t * const **l_397 = &l_398;
int i;
for (g_287 = (-12); (g_287 >= 18); g_287++)
{ Frama_C_show_each_trace(227);
int32_t **l_396 = &l_58;
(*l_396) = p_26;
}
l_389 &= (((l_344 ^ ((**g_363) = 0x31L)) , ((*l_397) = &g_190)) != l_401);
for (l_270 = 0; (l_270 < 32); ++l_270)
{ Frama_C_show_each_trace(235);
g_400[0] = (g_59 = 2L);
return p_26;
}
}
}
for (g_391 = 0; (g_391 < 56); g_391 = safe_add_func_int32_t_s_s(g_391, 9))
{ Frama_C_show_each_trace(244);
if ((*l_58))
break;
}
}
else
{ Frama_C_show_each_trace(247);
if ((*p_26))
break;
}
g_400[0] |= 0x7003CCA9L;
if ((safe_lshift_func_int8_t_s_s((((((((*l_408) = &l_96) != (g_230[0] , ((*l_409) = p_26))) , g_400[0]) , (**g_363)) & 1UL) == 0x9FCA559DDD172D46LL), 7)))
{ Frama_C_show_each_trace(253);
uint32_t l_419 = 0x70481B8DL;
int32_t l_440 = 0xF4E4425EL;
int32_t l_442 = 0L;
for (l_315 = 0; (l_315 <= 2); l_315 += 1)
{ Frama_C_show_each_trace(256);
int32_t l_416[2][2];
int i, j;
for (i = 0; i < 2; i++)
{
for (j = 0; j < 2; j++)
l_416[i][j] = (-1L);
}
if (g_346[l_315])
break;
for (g_337 = 0; (g_337 <= 0); g_337 += 1)
{ Frama_C_show_each_trace(260);
int32_t l_412 = 1L;
int32_t l_417 = 0x5838F8EFL;
int i;
l_412 |= (safe_lshift_func_int16_t_s_s(g_346[(g_337 + 1)], 2));
for (g_112 = 0; (g_112 <= 2); g_112 += 1)
{ Frama_C_show_each_trace(264);
uint32_t ***l_414 = (void*)0;
uint32_t ***l_415 = &g_413;
int32_t l_418 = 9L;
int i, j;
(*l_415) = g_413;
--l_419;
g_400[0] = l_340[g_337][(g_337 + 1)];
}
}
for (g_286 = 0; (g_286 >= 0); g_286 -= 1)
{ Frama_C_show_each_trace(272);
int i;
if (g_346[l_315])
break;
}
g_190 = l_422;
}
for (l_419 = 0; (l_419 > 46); ++l_419)
{ Frama_C_show_each_trace(279);
uint32_t l_439 = 0x0EDAA46BL;
l_442 = (safe_sub_func_int16_t_s_s(((**l_300) = (g_59 <= (safe_rshift_func_uint16_t_u_s(0x138AL, l_419)))), (l_419 , (safe_sub_func_uint32_t_u_u((safe_sub_func_uint8_t_u_u(((void*)0 != (*l_300)), (safe_mod_func_uint16_t_u_u(l_419, ((safe_mod_func_int64_t_s_s((l_440 = (l_439 & (0L <= 0xC97FL))), g_441[0])) && l_439))))), 0xF0E65E22L)))));
}
for (g_341 = (-30); (g_341 == 4); g_341 = safe_add_func_int64_t_s_s(g_341, 6))
{ Frama_C_show_each_trace(286);
(**l_408) ^= (safe_rshift_func_int16_t_s_u((safe_div_func_int16_t_s_s(l_351, l_419)), 10));
(*l_409) = p_26;
}
}
else
{ Frama_C_show_each_trace(290);
int32_t *l_449[3][1];
int i, j;
for (i = 0; i < 3; i++)
{
for (j = 0; j < 1; j++)
l_449[i][j] = &l_282;
}
return &g_3;
}
}
l_281 |= (g_94 , (safe_mod_func_int8_t_s_s(((((*g_364) != (l_270 & (1L || (l_96 , l_96)))) , (((*l_452) = (&l_96 != (((g_161[0] != g_262[0][0]) && (*g_364)) , p_26))) > g_441[0])) ^ 254UL), 0xBBL)));
return &g_30;
}
/* ---------------------------------------- */
int main (void)
{
int i, j;
int print_hash_value = 0;
platform_main_begin();
crc32_gentab();
func_1();
transparent_crc(g_3, "g_3", print_hash_value);
transparent_crc(g_5, "g_5", print_hash_value);
transparent_crc(g_30, "g_30", print_hash_value);
transparent_crc(g_59, "g_59", print_hash_value);
transparent_crc(g_70, "g_70", print_hash_value);
transparent_crc(g_94, "g_94", print_hash_value);
transparent_crc(g_112, "g_112", print_hash_value);
for (i = 0; i < 2; i++)
{
transparent_crc(g_121[i], "g_121[i]", print_hash_value);
if (print_hash_value) printf("index = [%d]\n", i);
}
transparent_crc(g_139, "g_139", print_hash_value);
transparent_crc(g_141, "g_141", print_hash_value);
transparent_crc(g_143, "g_143", print_hash_value);
transparent_crc(g_160, "g_160", print_hash_value);
for (i = 0; i < 1; i++)
{
transparent_crc(g_161[i], "g_161[i]", print_hash_value);
if (print_hash_value) printf("index = [%d]\n", i);
}
transparent_crc(g_164, "g_164", print_hash_value);
transparent_crc(g_182, "g_182", print_hash_value);
for (i = 0; i < 1; i++)
{
transparent_crc(g_230[i], "g_230[i]", print_hash_value);
if (print_hash_value) printf("index = [%d]\n", i);
}
for (i = 0; i < 3; i++)
{
for (j = 0; j < 3; j++)
{
transparent_crc(g_231[i][j], "g_231[i][j]", print_hash_value);
if (print_hash_value) printf("index = [%d][%d]\n", i, j);
}
}
for (i = 0; i < 3; i++)
{
for (j = 0; j < 3; j++)
{
transparent_crc(g_262[i][j], "g_262[i][j]", print_hash_value);
if (print_hash_value) printf("index = [%d][%d]\n", i, j);
}
}
for (i = 0; i < 2; i++)
{
for (j = 0; j < 1; j++)
{
transparent_crc(g_271[i][j], "g_271[i][j]", print_hash_value);
if (print_hash_value) printf("index = [%d][%d]\n", i, j);
}
}
transparent_crc(g_286, "g_286", print_hash_value);
transparent_crc(g_287, "g_287", print_hash_value);
transparent_crc(g_337, "g_337", print_hash_value);
transparent_crc(g_341, "g_341", print_hash_value);
for (i = 0; i < 3; i++)
{
transparent_crc(g_346[i], "g_346[i]", print_hash_value);
if (print_hash_value) printf("index = [%d]\n", i);
}
transparent_crc(g_391, "g_391", print_hash_value);
for (i = 0; i < 2; i++)
{
transparent_crc(g_400[i], "g_400[i]", print_hash_value);
if (print_hash_value) printf("index = [%d]\n", i);
}
for (i = 0; i < 1; i++)
{
transparent_crc(g_441[i], "g_441[i]", print_hash_value);
if (print_hash_value) printf("index = [%d]\n", i);
}
transparent_crc(g_556, "g_556", print_hash_value);
transparent_crc(g_590, "g_590", print_hash_value);
transparent_crc(g_711, "g_711", print_hash_value);
transparent_crc(g_731, "g_731", print_hash_value);
transparent_crc(g_839, "g_839", print_hash_value);
transparent_crc(g_1043, "g_1043", print_hash_value);
transparent_crc(g_1045, "g_1045", print_hash_value);
transparent_crc(g_1214, "g_1214", print_hash_value);
transparent_crc(g_1238, "g_1238", print_hash_value);
transparent_crc(g_1330, "g_1330", print_hash_value);
platform_main_end(crc32_context ^ 0xFFFFFFFFUL, print_hash_value);
return 0;
}
/************************ statistics *************************
XXX max struct depth: 0
breakdown:
depth: 0, occurrence: 437
XXX total union variables: 0
XXX non-zero bitfields defined in structs: 0
XXX zero bitfields defined in structs: 0
XXX const bitfields defined in structs: 0
XXX volatile bitfields defined in structs: 0
XXX structs with bitfields in the program: 0
breakdown:
XXX full-bitfields structs in the program: 0
breakdown:
XXX times a bitfields struct's address is taken: 0
XXX times a bitfields struct on LHS: 0
XXX times a bitfields struct on RHS: 0
XXX times a single bitfield on LHS: 0
XXX times a single bitfield on RHS: 0
XXX max expression depth: 25
breakdown:
depth: 1, occurrence: 255
depth: 2, occurrence: 70
depth: 3, occurrence: 4
depth: 4, occurrence: 5
depth: 5, occurrence: 5
depth: 6, occurrence: 2
depth: 7, occurrence: 2
depth: 8, occurrence: 3
depth: 9, occurrence: 3
depth: 10, occurrence: 4
depth: 12, occurrence: 1
depth: 13, occurrence: 3
depth: 14, occurrence: 4
depth: 15, occurrence: 7
depth: 17, occurrence: 2
depth: 18, occurrence: 1
depth: 20, occurrence: 2
depth: 21, occurrence: 2
depth: 22, occurrence: 2
depth: 25, occurrence: 1
XXX total number of pointers: 318
XXX times a variable address is taken: 169
XXX times a pointer is dereferenced on RHS: 251
breakdown:
depth: 1, occurrence: 220
depth: 2, occurrence: 31
XXX times a pointer is dereferenced on LHS: 220
breakdown:
depth: 1, occurrence: 205
depth: 2, occurrence: 11
depth: 3, occurrence: 4
XXX times a pointer is compared with null: 26
XXX times a pointer is compared with address of another variable: 1
XXX times a pointer is compared with another pointer: 6
XXX times a pointer is qualified to be dereferenced: 5296
XXX max dereference level: 3
breakdown:
level: 0, occurrence: 0
level: 1, occurrence: 6594
level: 2, occurrence: 647
level: 3, occurrence: 67
XXX number of pointers point to pointers: 142
XXX number of pointers point to scalars: 176
XXX number of pointers point to structs: 0
XXX percent of pointers has null in alias set: 25.8
XXX average alias set size: 1.47
XXX times a non-volatile is read: 1264
XXX times a non-volatile is write: 714
XXX times a volatile is read: 0
XXX times read thru a pointer: 0
XXX times a volatile is write: 0
XXX times written thru a pointer: 0
XXX times a volatile is available for access: 0
XXX percentage of non-volatile access: 100
XXX forward jumps: 1
XXX backward jumps: 12
XXX stmts: 253
XXX max block depth: 5
breakdown:
depth: 0, occurrence: 17
depth: 1, occurrence: 33
depth: 2, occurrence: 33
depth: 3, occurrence: 42
depth: 4, occurrence: 58
depth: 5, occurrence: 70
XXX percentage a fresh-made variable is used: 18.4
XXX percentage an existing variable is used: 81.6
********************* end of statistics **********************/
| ||||||||
 Relationships |
|
 Relationships |
|
Notes |
|
|
(0002264) pascal (reporter) 2011-09-14 14:36 |
Je savais bien que j'allais oublier quelque chose. J'ai attaché une version avec substitution, non testée. |
|
(0002265) pascal (reporter) 2011-09-14 14:41 |
> J'en étais sure que tu en trouverais d'autres ! On est sur des périodes de 18h avec 12 processeurs, comparable au temps passé à trouver les précédents bugs. Je varie aussi certains paramètres de temps en temps pour essayer de dénicher tous les bugs qui peuvent être trouvés de cette façon. Celui-ci s'est montré rapidement après que j'aie réglé l'analyse de valeurs sur "moins précis", mais ça ne veut pas forcément dire grand-chose, ça peut être une coïncidence. |
|
(0002268) Anne (reporter) 2011-09-14 16:14 |
Le problème est le suivant : - seule l'instruction [i = 0;] dépend du [goto]; - la boucle n'est pas considérée comme une vrai boucle car on emprunte jamais l'arc de bouclage ; - le [i] n'est donc pas utile. En bref, on ôte le [goto] parce qu'on a une boucle et on ôte la boucle puisqu'on a un goto : pas cool :-/ |
|
(0002269) Anne (reporter) 2011-09-14 17:55 |
Je pense qu'il y a un défaut dans le calcul des dépendances de contrôle pour les boucles... J'avais essayé de réparer les cas qui conduisaient à introduire des boucles infinies, mais je n'avais pas vu que le problème était plus grave. J'essaye de remettre tout ça à plat demain. |
|
(0002275) Anne (reporter) 2011-09-16 14:52 |
Oouuinn ! j'y arrive pas... :-( Je vais déjà essayer de résumer le problème (surtout pour moi dans un premier temps, et pour mémoire quand je serai partie). Quand on a [while(1) S; LS: ], on aimerait pouvoir générer les dépendances de contrôle pour le corps de boucle exactement comme si on avait [L: S; goto L; LS: ]. Dans le second cas, tout se passe bien parce que le [goto] est à la FIN du corps de boucle, si bien qu'il récupère les bonnes dépendances vis à vis des instructions de S. Dans le cas du while, comme il est au DEBUT du corps de boucle, on y passe déjà une première fois quand on entre dans la boucle, et non pas seulement en cas de bouclage réel. Il est difficile de faire "semblant" d'avoir le [goto] car on utilise par exemple le calcul de post-dominateurs, qui utilise Dataflow, c'est-a-dire les successeurs calculés par Cil. Par ailleurs, ce ne sont pas directement les dépendances sur le [while] qui posent un problème, mais plutôt celles sur les [goto] situés dans la boucle. Dans le cas présent, c'est le [goto L] qui devrait contrôler les instructions du début de boucle, et comme on garde [Frama_C_show_each], on garderait alors aussi le [goto]. Mais ce n'est pas le cas car le successeur lexical (*) du [goto] est le [while] et on a donc l'impression que le début de boucle ne dépend pas du [goto] (car on croit qu'on y va avec ou sans le goto). Dans ce cas très précis, on pourrait bricoler le successeur lexical quand on s'aperçoit que c'est une boucle, mais on aurait encore le problème dès qu'on ajouterait d'autres instructions en fin de boucle. (*) successeur lexical = instruction sur laquelle on se retrouverait si on remplaçait le [goto] par un [nop]. Sur ce, je retourne agiter mes trois neurones pour essayer de trouver une solution. |
|
(0002280) Anne (reporter) 2011-09-19 11:26 |
Finalement, je suis en train de faire une analyse des post-dominateurs spécifiquement adaptée aux besoins du PDG. De toute façon, il y en avait déjà une pour gérer le cas des boucles infinies, et du coup, autant tout faire là. L'objectif est de simuler la transformation [while] -> [goto]. |
|
(0002281) Anne (reporter) 2011-09-19 11:50 |
Il faut que je vérifie plus en détail, car je n'en crois pas mes yeux 8-/ mais il semblerait qu'en calculant simplement les post-dominateurs "correctement", ça corrige le problème ci-dessus, plus divers bugs dans les oracles ! :-) La différence proviendrait du fait que [!Db.Postdominators.stmt_postdominators kf stmt] contient [stmt] alors que normalement, une instruction ne se post-domine elle-même qu'en cas de boucle infinie. J'avais bricolé quelque chose pour néanmoins utiliser ce résultat, mais on dirait que c'était faux !!! A confirmer, donc... |
|
(0004736) Anne (reporter) 2014-02-12 16:59 |
Fix committed to stable/neon branch. |
|
Notes |
|
Issue History |
|||
| Date Modified | Username | Field | Change |
| 2011-09-14 14:13 | pascal | New Issue | |
| 2011-09-14 14:13 | pascal | Status | new => assigned |
| 2011-09-14 14:13 | pascal | Assigned To | => Anne |
| 2011-09-14 14:13 | pascal | File Added: s.tgz | |
| 2011-09-14 14:35 | pascal | File Added: s.c | |
| 2011-09-14 14:36 | pascal | Note Added: 0002264 | |
| 2011-09-14 14:41 | pascal | Note Added: 0002265 | |
| 2011-09-14 16:14 | Anne | Note Added: 0002268 | |
| 2011-09-14 17:55 | Anne | Note Added: 0002269 | |
| 2011-09-16 14:52 | Anne | Note Added: 0002275 | |
| 2011-09-19 11:26 | Anne | Note Added: 0002280 | |
| 2011-09-19 11:50 | Anne | Note Added: 0002281 | |
| 2011-09-19 15:50 | svn | Checkin | |
| 2011-09-19 15:50 | svn | Status | assigned => resolved |
| 2011-09-19 15:50 | svn | Resolution | open => fixed |
| 2011-10-10 14:13 | signoles | Fixed in Version | => Frama-C Nitrogen-20111001 |
| 2011-10-10 14:14 | signoles | Status | resolved => closed |
| 2011-12-18 20:09 | pascal | Status | closed => feedback |
| 2011-12-18 20:09 | pascal | Resolution | fixed => reopened |
| 2011-12-18 20:09 | pascal | View Status | private => public |
| 2011-12-19 09:51 | pascal | Status | feedback => closed |
| 2011-12-19 09:51 | pascal | Resolution | reopened => fixed |
| 2014-02-12 16:59 | Anne | Note Added: 0004736 | |
| 2014-02-12 16:59 | Anne | Status | closed => resolved |
|
Issue History |
| Copyright © 2000 - 2019 MantisBT Team |
|