./locksmith /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c


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


gcc -D_GNUCC -E -DCIL=1 /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c -o /tmp/cil-vmWeCaca.i
./cil/obj/x86_LINUX/cilly.asm.exe --out /tmp/cil-QoDpaiPb.cil.c /tmp/cil-vmWeCaca.i

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

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1144: Warning: subtyping incompatible types:
void
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1394: Warning: assigning pointer to non-pointer: (void)*^{tmp___2:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1340}
 ->
 int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1399: Warning: assigning pointer to non-pointer: (void)*^{tmp___3:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1341}
 ->
 int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987: Probably using char* where void* is best used:
 struct ObjectLink_s {
 }*^{*allocator.first_free:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1968} flows to int*^{*AtomicCompareAndSwapPointer.ptr:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987: Warning: subtyping incompatible types:
struct ObjectLink_s {
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987: Warning: subtyping incompatible types:
int
struct ObjectLink_s {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987: Probably using char* where void* is best used:
 int*^{*AtomicCompareAndSwapPointer.ptr:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987} flows to struct ObjectLink_s {
                                                                                                                                        }*^{*allocator.first_free:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1968}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987: Probably using char* where void* is best used:
 struct ObjectLink_s {
 }*^{old_link:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1971} flows to int*^{AtomicCompareAndSwapPointer.old_ptr:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987: Warning: subtyping incompatible types:
struct ObjectLink_s {
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987: Warning: subtyping incompatible types:
int
struct ObjectLink_s {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987: Probably using char* where void* is best used:
 struct ObjectLink_s {
 }*^{start:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1968} flows to int*^{AtomicCompareAndSwapPointer.new_ptr:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987: Warning: subtyping incompatible types:
struct ObjectLink_s {
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1987: Warning: subtyping incompatible types:
int
struct ObjectLink_s {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013: Probably using char* where void* is best used:
 struct ObjectLink_s {
   <*old_link.next:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1999> next: struct ObjectLink_s {
                                                                                                                }*^{*old_link.next:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1999}
 }*^{*allocator.first_free:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1996} flows to int*^{*AtomicCompareAndSwapPointer.ptr:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013: Warning: subtyping incompatible types:
struct ObjectLink_s {
  <*old_link.next:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1999> next: struct ObjectLink_s {
                                                                                                               }*^{*old_link.next:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1999}
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013: Warning: subtyping incompatible types:
int
struct ObjectLink_s {
  <*old_link.next:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1999> next: struct ObjectLink_s {
                                                                                                               }*^{*old_link.next:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1999}
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013: Probably using char* where void* is best used:
 int*^{*AtomicCompareAndSwapPointer.ptr:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013} flows to struct ObjectLink_s {
                                                                                                                                          <*old_link.next:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1999> next: struct ObjectLink_s {
                                                                                                                                                                                                                                                       }*^{*old_link.next:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1999}
                                                                                                                                        }*^{*allocator.first_free:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1996}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013: Probably using char* where void* is best used:
 struct ObjectLink_s {
   <*old_link.next:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1999> next: struct ObjectLink_s {
                                                                                                                }*^{*old_link.next:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1999}
 }*^{old_link:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1999} flows to int*^{AtomicCompareAndSwapPointer.old_ptr:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013: Warning: subtyping incompatible types:
struct ObjectLink_s {
  <*old_link.next:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1999> next: struct ObjectLink_s {
                                                                                                               }*^{*old_link.next:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1999}
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013: Warning: subtyping incompatible types:
int
struct ObjectLink_s {
  <*old_link.next:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1999> next: struct ObjectLink_s {
                                                                                                               }*^{*old_link.next:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:1999}
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013: Probably using char* where void* is best used:
 struct ObjectLink_s {
 }*^{next_link:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2000} flows to int*^{AtomicCompareAndSwapPointer.new_ptr:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013: Warning: subtyping incompatible types:
struct ObjectLink_s {
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2013: Warning: subtyping incompatible types:
int
struct ObjectLink_s {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2038: Warning: assigning pointer to non-pointer: (void)*^{*object:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2024}
 ->
 int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2186: Warning: subtyping incompatible types:
(void)
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2717: Warning: conflating flow at asm block
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2717: Warning: conflating flow at asm block
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2717: Warning: conflating flow at asm block
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2723: Warning: conflating flow at asm block
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2723: Warning: conflating flow at asm block
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2723: Warning: conflating flow at asm block
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2729: Warning: conflating flow at asm block
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2729: Warning: conflating flow at asm block
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:2729: Warning: conflating flow at asm block
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:3758: Warning: assigning pointer to non-pointer: (void)*^{data:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:3745}
 ->
 int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4011: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4011: Probably using char* where void* is best used:
 int*^{*(queue->data).ptr:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:3983} flows to struct Message {
                                                                                                                          }*^{msg:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:3986}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4011: Warning: subtyping incompatible types:
int
struct Message {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4011: Warning: subtyping incompatible types:
struct Message {
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4057: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4057: Probably using char* where void* is best used:
 int*^{*(queue->data).ptr:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4039} flows to struct Message {
                                                                                                                          }*^{ptr:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4041}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4057: Warning: subtyping incompatible types:
int
struct Message {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4057: Warning: subtyping incompatible types:
struct Message {
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4922: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4922: Probably using char* where void* is best used:
 int*^{*message.payload:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4912} flows to struct Msg_SampleTree {
                                                                                                                        }*^{payload:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4911}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4922: Warning: subtyping incompatible types:
int
struct Msg_SampleTree {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4922: Warning: subtyping incompatible types:
struct Msg_SampleTree {
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4948: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4948: Probably using char* where void* is best used:
 int*^{*message.payload:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4937} flows to struct Msg_AddToStringTable {
                                                                                                                        }*^{payload:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4935}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4948: Warning: subtyping incompatible types:
int
struct Msg_AddToStringTable {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:4948: Warning: subtyping incompatible types:
struct Msg_AddToStringTable {
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5336: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5336: Probably using char* where void* is best used:
 int*^{*message.payload:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5325} flows to struct Msg_ProcessorThreads {
                                                                                                                        }*^{payload:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5323}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5336: Warning: subtyping incompatible types:
int
struct Msg_ProcessorThreads {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5336: Warning: subtyping incompatible types:
struct Msg_ProcessorThreads {
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5818: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5818: Probably using char* where void* is best used:
 int*^{*message.payload:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5807} flows to struct Msg_AddToStringTable {
                                                                                                                        }*^{payload:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5809}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5818: Warning: subtyping incompatible types:
int
struct Msg_AddToStringTable {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5818: Warning: subtyping incompatible types:
struct Msg_AddToStringTable {
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5819: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5819: Probably using char* where void* is best used:
 struct Msg_AddToStringTable {
 }*^{payload:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5809} flows to int*^{name:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5810}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5975: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5975: Probably using char* where void* is best used:
 int*^{*message.payload:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5957} flows to struct Msg_SampleTree {
                                                                                                                        }*^{sample_tree:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5962}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5975: Warning: subtyping incompatible types:
int
struct Msg_SampleTree {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5975: Warning: subtyping incompatible types:
struct Msg_SampleTree {
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6028: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6028: Probably using char* where void* is best used:
 int*^{*message.payload:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:5996} flows to struct Msg_ProcessorThreads {
                                                                                                                        }*^{processor_threads:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6000}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6028: Warning: subtyping incompatible types:
int
struct Msg_ProcessorThreads {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6028: Warning: subtyping incompatible types:
struct Msg_ProcessorThreads {
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6334: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6334: Probably using char* where void* is best used:
 int*^{*message.payload:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6327} flows to struct Msg_PropertySnapshot {
                                                                                                                        }*^{msg_snapshot:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6329}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6334: Warning: subtyping incompatible types:
int
struct Msg_PropertySnapshot {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6334: Warning: subtyping incompatible types:
struct Msg_PropertySnapshot {
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6427: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6427: Probably using char* where void* is best used:
 int*^{*message.payload:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6406} flows to struct Msg_SampleTree {
                                                                                                                        }*^{sample_tree:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6408}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6427: Warning: subtyping incompatible types:
int
struct Msg_SampleTree {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6427: Warning: subtyping incompatible types:
struct Msg_SampleTree {
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6431: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6431: Probably using char* where void* is best used:
 int*^{*message.payload:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6406} flows to struct Msg_PropertySnapshot {
                                                                                                                        }*^{msg_snapshot:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6409}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6431: Warning: subtyping incompatible types:
int
struct Msg_PropertySnapshot {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6431: Warning: subtyping incompatible types:
struct Msg_PropertySnapshot {
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6469: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6469: Probably using char* where void* is best used:
 int*^{*(queue->data).ptr:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6446} flows to struct Message {
                                                                                                                          }*^{message:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6449}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6469: Warning: subtyping incompatible types:
int
struct Message {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6469: Warning: subtyping incompatible types:
struct Message {
}
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6503: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6503: Probably using char* where void* is best used:
 (rmt: struct Remotery {
       }*^{*rmt.map_message_queue_fn->rmt:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485},
  arg2: struct Message {
        }*^{*rmt.map_message_queue_fn->arg2:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485},
  in at /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485)
 ->^{(Er_inputeffect#12559\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
      Ew_inputeffect#12558\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
      Es_dummy#4\n:-1,
     ),
     (Er_outputeffect#12557\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
      Ew_outputeffect#12556\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
      Es_dummy#4\n:-1,
     ),
     X-Xr_X#12555\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485}
 (void,
  out at /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485)*^{*rmt.map_message_queue_fn:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485} flows to int*^{*LoadAcquirePointer.ptr:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6503}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6503: Warning: subtyping incompatible types:
(rmt: struct Remotery {
      }*^{*rmt.map_message_queue_fn->rmt:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485},
 arg2: struct Message {
       }*^{*rmt.map_message_queue_fn->arg2:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485},
 in at /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485)
->^{(Er_inputeffect#12559\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
     Ew_inputeffect#12558\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
     Es_dummy#4\n:-1,
    ),
    (Er_outputeffect#12557\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
     Ew_outputeffect#12556\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
     Es_dummy#4\n:-1,
    ),
    X-Xr_X#12555\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485}
(void,
 out at /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485)
int
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6503: Warning: subtyping incompatible types:
int
(rmt: struct Remotery {
      }*^{*rmt.map_message_queue_fn->rmt:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485},
 arg2: struct Message {
       }*^{*rmt.map_message_queue_fn->arg2:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485},
 in at /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485)
->^{(Er_inputeffect#12559\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
     Ew_inputeffect#12558\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
     Es_dummy#4\n:-1,
    ),
    (Er_outputeffect#12557\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
     Ew_outputeffect#12556\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
     Es_dummy#4\n:-1,
    ),
    X-Xr_X#12555\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485}
(void,
 out at /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485)
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6503: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6503: Probably using char* where void* is best used:
 int*^{*LoadAcquirePointer.ptr:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6503} flows to (rmt: struct Remotery {
                                                                                                                                     }*^{*rmt.map_message_queue_fn->rmt:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485},
                                                                                                                                arg2: struct Message {
                                                                                                                                      }*^{*rmt.map_message_queue_fn->arg2:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485},
                                                                                                                                in at /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485)
                                                                                                                               ->^{(Er_inputeffect#12559\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
                                                                                                                                    Ew_inputeffect#12558\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
                                                                                                                                    Es_dummy#4\n:-1,
                                                                                                                                   ),
                                                                                                                                   (Er_outputeffect#12557\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
                                                                                                                                    Ew_outputeffect#12556\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
                                                                                                                                    Es_dummy#4\n:-1,
                                                                                                                                   ),
                                                                                                                                   X-Xr_X#12555\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485}
                                                                                                                               (void,
                                                                                                                                out at /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485)*^{*rmt.map_message_queue_fn:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6506: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6506: Probably using char* where void* is best used:
 (rmt: struct Remotery {
       }*^{*rmt.map_message_queue_fn->rmt:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485},
  arg2: struct Message {
        }*^{*rmt.map_message_queue_fn->arg2:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485},
  in at /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485)
 ->^{(Er_inputeffect#12559\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
      Ew_inputeffect#12558\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
      Es_dummy#4\n:-1,
     ),
     (Er_outputeffect#12557\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
      Ew_outputeffect#12556\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
      Es_dummy#4\n:-1,
     ),
     X-Xr_X#12555\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485}
 (void,
  out at /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485)*^{*rmt.map_message_queue_fn:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485} flows to int*^{*StoreReleasePointer.ptr:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6506}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6506: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6506: Probably using char* where void* is best used:
 int*^{*StoreReleasePointer.ptr:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6506} flows to (rmt: struct Remotery {
                                                                                                                                      }*^{*rmt.map_message_queue_fn->rmt:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485},
                                                                                                                                 arg2: struct Message {
                                                                                                                                       }*^{*rmt.map_message_queue_fn->arg2:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485},
                                                                                                                                 in at /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485)
                                                                                                                                ->^{(Er_inputeffect#12559\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
                                                                                                                                     Ew_inputeffect#12558\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
                                                                                                                                     Es_dummy#4\n:-1,
                                                                                                                                    ),
                                                                                                                                    (Er_outputeffect#12557\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
                                                                                                                                     Ew_outputeffect#12556\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485,
                                                                                                                                     Es_dummy#4\n:-1,
                                                                                                                                    ),
                                                                                                                                    X-Xr_X#12555\n/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485}
                                                                                                                                (void,
                                                                                                                                 out at /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485)*^{*rmt.map_message_queue_fn:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:6485}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:7500: Warning: /mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:7500: Probably using char* where void* is best used:
 int*^{*message.payload:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:7470} flows to struct Msg_PropertySnapshot {
                                                                                                                        }*^{payload:/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:7469}.  Losing precision.

/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:7500: Warning: subtyping incompatible types:
int
struct Msg_PropertySnapshot {
}
/mnt/goblint-svcomp/goblint-bench/the-continuous-race/benchmarks/Remotery/main.c:7500: Warning: subtyping incompatible types:
struct Msg_PropertySnapshot {
}
int
functions declared and used but not defined:
  __assert_fail
  __errno_location
  __sync_bool_compare_and_swap
  __sync_fetch_and_add
  abs
  accept
  bind
  clock
  clock_gettime
  close
  fabs
  fclose
  fcntl
  fmod
  fopen
  ftruncate
  fwrite
  gmtime
  htonl
  htons
  listen
  mbstowcs
  memcmp
  mkstemp
  mmap
  munmap
  prctl
  printf
  pthread_equal
  pthread_getspecific
  pthread_join
  pthread_key_create
  pthread_key_delete
  pthread_self
  pthread_setspecific
  rand
  recv
  select
  send
  setsockopt
  shutdown
  signal
  sin
  socket
  strlen
  time
  unlink
  usleep
