./locksmith /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c


--------------------------------------------------------------------------------


gcc -D_GNUCC -E -DCIL=1 /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c -o /tmp/cil-POuvTLj4.i
./cil/obj/x86_LINUX/cilly.asm.exe --out /tmp/cil-8gyhgKdH.cil.c /tmp/cil-POuvTLj4.i
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3910: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3910: Warning: Variable-sized local variable rbuf
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3972: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3972: Warning: Variable-sized local variable buf
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4064: Warning: MEMBEROFPTR in constant
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4064: Warning: Variable-sized local variable fds
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4344: Warning: Variable-sized local variable buf

************************* STARTING *************************

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:920: Warning: function pointer conflated
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:920: Warning: function pointer in downcasting.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:920: Warning: function pointer conflated
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:920: Warning: function pointer in downcasting.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1324: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1324: Probably using char* where void* is best used:
 int*^{*skb.head:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1319} flows to struct iphdr {
                                                                                                }*^{ip_hdr.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1319}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1324: Warning: subtyping incompatible types:
int
struct iphdr {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1324: Warning: subtyping incompatible types:
struct iphdr {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1527: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1527: Probably using char* where void* is best used:
 int*^{*iphdr.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1520} flows to struct icmp_v4 {
                                                                                                  }*^{icmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1522}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1527: Warning: subtyping incompatible types:
int
struct icmp_v4 {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1527: Warning: subtyping incompatible types:
struct icmp_v4 {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1560: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1560: Probably using char* where void* is best used:
 int*^{*skb.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1516} flows to struct icmp_v4 {
                                                                                                }*^{icmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1549}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1560: Warning: subtyping incompatible types:
int
struct icmp_v4 {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1560: Warning: subtyping incompatible types:
struct icmp_v4 {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1948: Warning: number of args non-equal. first extra arg: int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1948: Warning: number of args non-equal. first extra arg: int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1996: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1996: Probably using char* where void* is best used:
 int*^{*iph.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1991} flows to struct tcphdr {
                                                                                                }*^{th:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1992}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1996: Warning: subtyping incompatible types:
int
struct tcphdr {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:1996: Warning: subtyping incompatible types:
struct tcphdr {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2635: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2635: Probably using char* where void* is best used:
 int*^{*skb.head:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2630} flows to struct tcphdr {
                                                                                                }*^{tcp_hdr.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2630}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2635: Warning: subtyping incompatible types:
int
struct tcphdr {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2635: Warning: subtyping incompatible types:
struct tcphdr {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2674: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2674: Probably using char* where void* is best used:
 int*^{*th.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2664} flows to struct tcp_opt_mss {
                                                                                               }*^{opt_mss:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2666}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2674: Warning: subtyping incompatible types:
int
struct tcp_opt_mss {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2674: Warning: subtyping incompatible types:
struct tcp_opt_mss {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2748: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2748: Probably using char* where void* is best used:
 int*^{ptr:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2720} flows to struct tcp_sack_block {
                                                                                          }*^{sb:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2725}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2748: Warning: subtyping incompatible types:
int
struct tcp_sack_block {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:2748: Warning: subtyping incompatible types:
struct tcp_sack_block {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3192: Warning: subtyping incompatible types:
(void)
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3266: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3266: Probably using char* where void* is best used:
 int*^{*skb.head:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3261} flows to struct arp_hdr {
                                                                                                }*^{arp_hdr.return:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3261}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3266: Warning: subtyping incompatible types:
int
struct arp_hdr {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3266: Warning: subtyping incompatible types:
struct arp_hdr {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3371: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3371: Probably using char* where void* is best used:
 int*^{*arphdr.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3351} flows to struct arp_ipv4 {
                                                                                                   }*^{arpdata:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3352}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3371: Warning: subtyping incompatible types:
int
struct arp_ipv4 {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3371: Warning: subtyping incompatible types:
struct arp_ipv4 {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3417: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3417: Probably using char* where void* is best used:
 int*^{tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3406} flows to struct arp_ipv4 {
                                                                                          }*^{payload:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3404}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3417: Warning: subtyping incompatible types:
int
struct arp_ipv4 {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3417: Warning: subtyping incompatible types:
struct arp_ipv4 {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3425: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3425: Probably using char* where void* is best used:
 int*^{tmp___0:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3407} flows to struct arp_hdr {
                                                                                              }*^{arp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3403}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3425: Warning: subtyping incompatible types:
int
struct arp_hdr {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3425: Warning: subtyping incompatible types:
struct arp_hdr {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3447: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3447: Probably using char* where void* is best used:
 int*^{*arphdr.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3440} flows to struct arp_ipv4 {
                                                                                                   }*^{arpdata:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3441}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3447: Warning: subtyping incompatible types:
int
struct arp_ipv4 {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3447: Warning: subtyping incompatible types:
struct arp_ipv4 {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3521: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3521: Probably using char* where void* is best used:
 int*^{tmp:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3517} flows to struct eth_hdr {
                                                                                          }*^{hdr:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3516}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3521: Warning: subtyping incompatible types:
int
struct eth_hdr {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3521: Warning: subtyping incompatible types:
struct eth_hdr {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3586: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3586: Probably using char* where void* is best used:
 int*^{*skb.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3253} flows to struct eth_hdr {
                                                                                                }*^{hdr:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3579}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3586: Warning: subtyping incompatible types:
int
struct eth_hdr {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3586: Warning: subtyping incompatible types:
struct eth_hdr {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3883: Warning: subtyping incompatible types:
struct ipc_err {
  <err.err:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3863> err: int
  <err.rc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3863> rc: int
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3907: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3907: Probably using char* where void* is best used:
 int*^{*msg.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3892} flows to struct ipc_read {
                                                                                                }*^{requested:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3894}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3907: Warning: subtyping incompatible types:
int
struct ipc_read {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3907: Warning: subtyping incompatible types:
struct ipc_read {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3921: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3921: Probably using char* where void* is best used:
 int*^{*response.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3899} flows to struct ipc_err {
                                                                                                     }*^{error:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3901}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3921: Warning: subtyping incompatible types:
int
struct ipc_err {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3921: Warning: subtyping incompatible types:
struct ipc_err {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3922: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3922: Probably using char* where void* is best used:
 int*^{*error.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3901} flows to struct ipc_read {
                                                                                                  }*^{actual:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3902}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3922: Warning: subtyping incompatible types:
int
struct ipc_read {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3922: Warning: subtyping incompatible types:
struct ipc_read {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3968: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3968: Probably using char* where void* is best used:
 int*^{*msg.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3955} flows to struct ipc_write {
                                                                                                }*^{payload:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3957}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3968: Warning: subtyping incompatible types:
int
struct ipc_write {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3968: Warning: subtyping incompatible types:
struct ipc_write {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4006: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4006: Probably using char* where void* is best used:
 int*^{*msg.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:3998} flows to struct ipc_connect {
                                                                                                }*^{payload:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4000}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4006: Warning: subtyping incompatible types:
int
struct ipc_connect {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4006: Warning: subtyping incompatible types:
struct ipc_connect {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4023: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4023: Probably using char* where void* is best used:
 int*^{*msg.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4015} flows to struct ipc_socket {
                                                                                                }*^{sock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4017}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4023: Warning: subtyping incompatible types:
int
struct ipc_socket {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4023: Warning: subtyping incompatible types:
struct ipc_socket {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4038: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4038: Probably using char* where void* is best used:
 int*^{*msg.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4031} flows to struct ipc_close {
                                                                                                }*^{payload:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4033}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4038: Warning: subtyping incompatible types:
int
struct ipc_close {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4038: Warning: subtyping incompatible types:
struct ipc_close {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4061: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4061: Probably using char* where void* is best used:
 int*^{*msg.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4046} flows to struct ipc_poll {
                                                                                                }*^{data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4048}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4061: Warning: subtyping incompatible types:
int
struct ipc_poll {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4061: Warning: subtyping incompatible types:
struct ipc_poll {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4089: Warning: subtyping incompatible types:
struct ipc_err {
  <err.err:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4055> err: int
  <err.rc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4055> rc: int
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4091: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4091: Probably using char* where void* is best used:
 int*^{*response.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4053} flows to struct ipc_err {
                                                                                                     }*^{cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4091}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4091: Warning: subtyping incompatible types:
int
struct ipc_err {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4091: Warning: subtyping incompatible types:
struct ipc_err {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4091: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4091: Probably using char* where void* is best used:
 int*^{*((struct ipc_err *)(response->data)).data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4091} flows to struct ipc_pollfd {
                                                                                                                                 }*^{polled:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4056}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4091: Warning: subtyping incompatible types:
int
struct ipc_pollfd {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4091: Warning: subtyping incompatible types:
struct ipc_pollfd {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4114: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4114: Probably using char* where void* is best used:
 int*^{*msg.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4106} flows to struct ipc_fcntl {
                                                                                                }*^{fc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4108}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4114: Warning: subtyping incompatible types:
int
struct ipc_fcntl {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4114: Warning: subtyping incompatible types:
struct ipc_fcntl {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4146: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4146: Probably using char* where void* is best used:
 int*^{*msg.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4133} flows to struct ipc_sockopt {
                                                                                                }*^{opts:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4135}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4146: Warning: subtyping incompatible types:
int
struct ipc_sockopt {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4146: Warning: subtyping incompatible types:
struct ipc_sockopt {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4167: Warning: subtyping incompatible types:
struct ipc_err {
  <err.err:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4141> err: int
  <err.rc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4141> rc: int
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4169: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4169: Probably using char* where void* is best used:
 int*^{*response.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4139} flows to struct ipc_err {
                                                                                                     }*^{cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4169}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4169: Warning: subtyping incompatible types:
int
struct ipc_err {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4169: Warning: subtyping incompatible types:
struct ipc_err {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4169: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4169: Probably using char* where void* is best used:
 int*^{*((struct ipc_err *)(response->data)).data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4169} flows to struct ipc_sockopt {
                                                                                                                                 }*^{optres:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4142}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4169: Warning: subtyping incompatible types:
int
struct ipc_sockopt {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4169: Warning: subtyping incompatible types:
struct ipc_sockopt {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4174: Warning: assigning number to pointer
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4196: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4196: Probably using char* where void* is best used:
 int*^{*msg.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4183} flows to struct ipc_sockname {
                                                                                                }*^{name:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4185}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4196: Warning: subtyping incompatible types:
int
struct ipc_sockname {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4196: Warning: subtyping incompatible types:
struct ipc_sockname {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4208: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4208: Probably using char* where void* is best used:
 int*^{*response.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4189} flows to struct ipc_err {
                                                                                                     }*^{cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4208}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4208: Warning: subtyping incompatible types:
int
struct ipc_err {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4208: Warning: subtyping incompatible types:
struct ipc_err {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4208: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4208: Probably using char* where void* is best used:
 int*^{*((struct ipc_err *)(response->data)).data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4208} flows to struct ipc_sockname {
                                                                                                                                 }*^{nameres:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4191}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4208: Warning: subtyping incompatible types:
int
struct ipc_sockname {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4208: Warning: subtyping incompatible types:
struct ipc_sockname {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4209: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4209: Probably using char* where void* is best used:
 int*^{*nameres.sa_data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4191} flows to struct sockaddr {
                                                                                                       }*^{_getpeername.address:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4209}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4209: Warning: subtyping incompatible types:
int
struct sockaddr {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4209: Warning: subtyping incompatible types:
struct sockaddr {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4218: Warning: subtyping incompatible types:
struct ipc_err {
  <err.err:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4192> err: int
  <err.rc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4192> rc: int
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4241: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4241: Probably using char* where void* is best used:
 int*^{*msg.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4228} flows to struct ipc_sockname {
                                                                                                }*^{name:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4230}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4241: Warning: subtyping incompatible types:
int
struct ipc_sockname {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4241: Warning: subtyping incompatible types:
struct ipc_sockname {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4253: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4253: Probably using char* where void* is best used:
 int*^{*response.data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4234} flows to struct ipc_err {
                                                                                                     }*^{cast:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4253}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4253: Warning: subtyping incompatible types:
int
struct ipc_err {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4253: Warning: subtyping incompatible types:
struct ipc_err {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4253: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4253: Probably using char* where void* is best used:
 int*^{*((struct ipc_err *)(response->data)).data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4253} flows to struct ipc_sockname {
                                                                                                                                 }*^{nameres:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4236}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4253: Warning: subtyping incompatible types:
int
struct ipc_sockname {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4253: Warning: subtyping incompatible types:
struct ipc_sockname {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4254: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4254: Probably using char* where void* is best used:
 int*^{*nameres.sa_data:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4236} flows to struct sockaddr {
                                                                                                       }*^{_getsockname.address:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4254}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4254: Warning: subtyping incompatible types:
int
struct sockaddr {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4254: Warning: subtyping incompatible types:
struct sockaddr {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4263: Warning: subtyping incompatible types:
struct ipc_err {
  <err.err:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4237> err: int
  <err.rc:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4237> rc: int
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4288: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4288: Probably using char* where void* is best used:
 int*^{cmdbuf:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4273} flows to struct ipc_msg {
                                                                                             }*^{msg:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4275}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4288: Warning: subtyping incompatible types:
int
struct ipc_msg {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4288: Warning: subtyping incompatible types:
struct ipc_msg {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4577: Warning: assigning pointer to non-pointer: (void)*^{create_thread.func->arg1:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4577}
 ->
 void
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4577: Warning: assigning non-pointer to pointer: void
 ->
 (void)*^{create_thread.func->arg1:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4577}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4578: Warning: number of args non-equal. first extra arg: (void)*^{create_thread.func->arg1:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4578}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4578: Warning: number of args non-equal. first extra arg: (void)*^{create_thread.func->arg1:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4578}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4579: Warning: assigning pointer to non-pointer: (void)*^{create_thread.func->arg1:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4579}
 ->
 void
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4579: Warning: assigning non-pointer to pointer: void
 ->
 (void)*^{create_thread.func->arg1:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4579}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4714: Warning: /mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4714: Probably using char* where void* is best used:
 int*^{ptr:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4690} flows to struct tcp_opt_mss {
                                                                                          }*^{opt_mss:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4692}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4714: Warning: subtyping incompatible types:
int
struct tcp_opt_mss {
}
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4714: Warning: subtyping incompatible types:
struct tcp_opt_mss {
}
int
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4950: Warning: function pointer conflated
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4950: Warning: function pointer in downcasting.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4950: Warning: function pointer conflated
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:4950: Warning: function pointer in downcasting.

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:5267: Warning: lock is conflated! (*t.lock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:5267)
/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:5267: Warning: lock emerges at downcasting: *t.lock:/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:5267

/mnt/goblint-svcomp/goblint-bench/bench/concrat/level-ip/main.c:5298: Error: overwritting trylock-result
Fatal error: exception Locktype.TypingBug
