forked from cil-project/cil
-
Notifications
You must be signed in to change notification settings - Fork 24
Open
Labels
Description
In concrat/zmap, which has been merged with Goblint CIL 1.8.2, merging has produced some non-compilable code.
In particular, this happens with a function argument which is a transparent union, some GCC trickery. CIL does some transformations with it, but when merging, some copies of the function are in a non-compilable intermediate state.
I didn't try to reproduce it with a newer Goblint CIL, but we haven't fixed anything related to transparent unions (I wasn't even aware of them), so it's unlikely to have changed.
Correct version
__inline extern ssize_t ( __attribute__((__gnu_inline__, __always_inline__)) recvfrom)(int __fd ,
void * __restrict __buf ,
size_t __n ,
int __flags ,
struct sockaddr * __restrict __cil_tmp14 ,
socklen_t * __restrict __addr_len )
{
__SOCKADDR_ARG __addr ;
unsigned long tmp ;
ssize_t tmp___0 ;
unsigned long tmp___1 ;
ssize_t tmp___2 ;
unsigned long tmp___3 ;
unsigned long tmp___4 ;
ssize_t tmp___5 ;
{
__addr.__sockaddr__ = __cil_tmp14;
tmp___4 = __builtin_object_size((void *)__buf, 0);
if (tmp___4 != 0xffffffffffffffffUL) {
tmp = __builtin_object_size((void *)__buf, 0);
tmp___0 = __recvfrom_chk(__fd, __buf, __n, tmp, __flags, __addr.__sockaddr__,
__addr_len);
return (tmp___0);
tmp___3 = __builtin_object_size((void *)__buf, 0);
if (__n > tmp___3) {
tmp___1 = __builtin_object_size((void *)__buf, 0);
tmp___2 = __recvfrom_chk_warn(__fd, __buf, __n, tmp___1, __flags, __addr.__sockaddr__,
__addr_len);
return (tmp___2);
}
}
tmp___5 = __recvfrom_alias(__fd, __buf, __n, __flags, __addr.__sockaddr__, __addr_len);
return (tmp___5);
}
}Incorrect version
Body uses __addr but argument has already been replaced with __cil_tmp14, yet no local nor assignment has been added to body:
__inline extern ssize_t ( __attribute__((__gnu_inline__, __always_inline__)) recvfrom)(int __fd ,
void * __restrict __buf ,
size_t __n ,
int __flags ,
struct sockaddr * __restrict __cil_tmp14 ,
socklen_t * __restrict __addr_len )
{
unsigned long tmp ;
ssize_t tmp___0 ;
unsigned long tmp___1 ;
ssize_t tmp___2 ;
unsigned long tmp___3 ;
unsigned long tmp___4 ;
ssize_t tmp___5 ;
{
tmp___4 = __builtin_object_size((void *)__buf, 0);
if (tmp___4 != 0xffffffffffffffffUL) {
tmp = __builtin_object_size((void *)__buf, 0);
tmp___0 = __recvfrom_chk(__fd, __buf, __n, tmp, __flags, __addr, __addr_len);
return (tmp___0);
tmp___3 = __builtin_object_size((void *)__buf, 0);
if (__n > tmp___3) {
tmp___1 = __builtin_object_size((void *)__buf, 0);
tmp___2 = __recvfrom_chk_warn(__fd, __buf, __n, tmp___1, __flags, __addr, __addr_len);
return (tmp___2);
}
}
tmp___5 = __recvfrom_alias(__fd, __buf, __n, __flags, __addr, __addr_len);
return (tmp___5);
}
}Reactions are currently unavailable