Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- input: hello.bc
- <...> property { safety }: [assert + memory + arithmetic + leak + user + guard + mutex]
- ---------------- Reachability ----------------
- meta: model=hello.bc; algorithm=reachability; visitor=shared; compression=tree; threads=8; mpinodes=1;
- searching... 10 states, 10 edges, GOAL
- ===== Trace from initial =====
- globals:
- key = @(48904:0| null)
- once = @(48906:0| { { 0, 0, 3, 0 } })
- stdin = @(48919:0| @(48920:0| { 48926:0 <...>, { null }, { [ 0, 0, 0, 0 ] }, 48930:0 <...>, 256, 0, 0, 0, 48935:0 <...>, 32778, { 0, { { [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ], [ 0, 0, 0, 0, 0, 0, 0, 0 ] }, 0, 0, 0 } }, null, 48941:0 <...> }))
- stdout = @(48967:0| 48941:0 <...>)
- stderr = @(48969:0| 48950:0 <...>)
- __cxa_terminate_handler = @(50652:0| 299:0)
- __cxa_unexpected_handler = @(50654:0| 300:0)
- __cxa_new_handler = @(51128:0| null)
- __dso_handle = @(54063:0| null)
- _mpi_num_processes = @(54069:0| 0)
- _mpi_exit_barrier = @(54071:0| 0)
- MPI_CHAR = @(54114:0| null)
- MPI_SHORT = @(54116:0| null)
- MPI_INT = @(54118:0| null)
- MPI_LONG = @(54120:0| null)
- MPI_LONG_LONG_INT = @(54122:0| null)
- MPI_LONG_LONG = @(54124:0| null)
- MPI_SIGNED_CHAR = @(54126:0| null)
- MPI_UNSIGNED_CHAR = @(54128:0| null)
- MPI_UNSIGNED_SHORT = @(54130:0| null)
- MPI_UNSIGNED = @(54132:0| null)
- MPI_UNSIGNED_LONG = @(54134:0| null)
- MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
- MPI_FLOAT = @(54138:0| null)
- MPI_DOUBLE = @(54140:0| null)
- MPI_LONG_DOUBLE = @(54142:0| null)
- MPI_WCHAR = @(54144:0| null)
- MPI_C_BOOL = @(54146:0| null)
- MPI_INT8_T = @(54148:0| null)
- MPI_INT16_T = @(54150:0| null)
- MPI_INT32_T = @(54152:0| null)
- MPI_INT64_T = @(54154:0| null)
- MPI_UINT8_T = @(54156:0| null)
- MPI_UINT16_T = @(54158:0| null)
- MPI_UINT32_T = @(54160:0| null)
- MPI_UINT64_T = @(54162:0| null)
- MPI_AINT = @(54164:0| null)
- MPI_COUNT = @(54166:0| null)
- MPI_OFFSET = @(54168:0| null)
- MPI_C_COMPLEX = @(54170:0| null)
- MPI_C_FLOAT_COMPLEX = @(54172:0| null)
- MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
- MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
- MPI_BYTE = @(54178:0| null)
- MPI_PACKED = @(54180:0| null)
- MPI_FLOAT_INT = @(54182:0| null)
- MPI_DOUBLE_INT = @(54184:0| null)
- MPI_LONG_INT = @(54186:0| null)
- MPI_2INT = @(54188:0| null)
- MPI_SHORT_INT = @(54190:0| null)
- MPI_LONG_DOUBLE_INT = @(54192:0| null)
- MPI_MAX = @(54198:0| null)
- MPI_MIN = @(54200:0| null)
- MPI_SUM = @(54202:0| null)
- MPI_PROD = @(54204:0| null)
- MPI_MAXLOC = @(54206:0| null)
- MPI_MINLOC = @(54208:0| null)
- MPI_BAND = @(54210:0| null)
- MPI_BOR = @(54212:0| null)
- MPI_BXOR = @(54214:0| null)
- MPI_LAND = @(54216:0| null)
- MPI_LOR = @(54218:0| null)
- MPI_LXOR = @(54220:0| null)
- MPI_GROUP_EMPTY = @(54222:0| null)
- MPI_COMM_WORLD_ = @(54226:0| null)
- MPI_COMM_SELF_ = @(54228:0| null)
- thread 0:
- #1: <_divine_start> << %1 = alloca i32, align 4 >> [ ctorcount = 5, ctors = 899219456, mainproto = 2, c = 0?, i = 0?, r = 0?, i1 = 0? ]
- globals:
- key = @(48904:0| null)
- once = @(48906:0| { { 0, 0, 3, 0 } })
- stdin = @(48919:0| @(48920:0| { 48926:0 <...>, { null }, { [ 0, 0, 5, 0 ] }, 48930:0 <...>, 256, 0, 0, 0, 48935:0 <...>, 32778, { 0, { { [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ], [ 0, 0, 0, 0, 0, 0, 0, 0 ] }, 0, 0, 0 } }, null, 48941:0 <...> }))
- stdout = @(48967:0| 48941:0 <...>)
- stderr = @(48969:0| 48950:0 <...>)
- __cxa_terminate_handler = @(50652:0| 299:0)
- __cxa_unexpected_handler = @(50654:0| 300:0)
- __cxa_new_handler = @(51128:0| null)
- __dso_handle = @(54063:0| null)
- _mpi_num_processes = @(54069:0| 0)
- _mpi_exit_barrier = @(54071:0| 0)
- MPI_CHAR = @(54114:0| null)
- MPI_SHORT = @(54116:0| null)
- MPI_INT = @(54118:0| null)
- MPI_LONG = @(54120:0| null)
- MPI_LONG_LONG_INT = @(54122:0| null)
- MPI_LONG_LONG = @(54124:0| null)
- MPI_SIGNED_CHAR = @(54126:0| null)
- MPI_UNSIGNED_CHAR = @(54128:0| null)
- MPI_UNSIGNED_SHORT = @(54130:0| null)
- MPI_UNSIGNED = @(54132:0| null)
- MPI_UNSIGNED_LONG = @(54134:0| null)
- MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
- MPI_FLOAT = @(54138:0| null)
- MPI_DOUBLE = @(54140:0| null)
- MPI_LONG_DOUBLE = @(54142:0| null)
- MPI_WCHAR = @(54144:0| null)
- MPI_C_BOOL = @(54146:0| null)
- MPI_INT8_T = @(54148:0| null)
- MPI_INT16_T = @(54150:0| null)
- MPI_INT32_T = @(54152:0| null)
- MPI_INT64_T = @(54154:0| null)
- MPI_UINT8_T = @(54156:0| null)
- MPI_UINT16_T = @(54158:0| null)
- MPI_UINT32_T = @(54160:0| null)
- MPI_UINT64_T = @(54162:0| null)
- MPI_AINT = @(54164:0| null)
- MPI_COUNT = @(54166:0| null)
- MPI_OFFSET = @(54168:0| null)
- MPI_C_COMPLEX = @(54170:0| null)
- MPI_C_FLOAT_COMPLEX = @(54172:0| null)
- MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
- MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
- MPI_BYTE = @(54178:0| null)
- MPI_PACKED = @(54180:0| null)
- MPI_FLOAT_INT = @(54182:0| null)
- MPI_DOUBLE_INT = @(54184:0| null)
- MPI_LONG_INT = @(54186:0| null)
- MPI_2INT = @(54188:0| null)
- MPI_SHORT_INT = @(54190:0| null)
- MPI_LONG_DOUBLE_INT = @(54192:0| null)
- MPI_MAX = @(54198:0| null)
- MPI_MIN = @(54200:0| null)
- MPI_SUM = @(54202:0| null)
- MPI_PROD = @(54204:0| null)
- MPI_MAXLOC = @(54206:0| null)
- MPI_MINLOC = @(54208:0| null)
- MPI_BAND = @(54210:0| null)
- MPI_BOR = @(54212:0| null)
- MPI_BXOR = @(54214:0| null)
- MPI_LAND = @(54216:0| null)
- MPI_LOR = @(54218:0| null)
- MPI_LXOR = @(54220:0| null)
- MPI_GROUP_EMPTY = @(54222:0| null)
- MPI_COMM_WORLD_ = @(54226:0| null)
- MPI_COMM_SELF_ = @(54228:0| null)
- thread 0:
- #1: <_divine_start> [ entry.cpp:53 ] [ ctorcount = 5, ctors = 899219456, mainproto = 2, c = @(7:0| @(54884:0| { 65535, 151:0 })), i = @(8:0| 0), r = @(9:0| 0?), i1 = @(10:0| 0?) ]
- #2: <init_stdio> [ posix/_PDCLIB_stdinit.c:792 ] []
- #3: <mtx_init> << %1 = alloca i32, align 4 >> [ mtx = 801849360, type = 1, rc = 0?, attr = 0? ]
- globals:
- key = @(48904:0| null)
- once = @(48906:0| { { 0, 0, 3, 0 } })
- stdin = @(48919:0| @(48920:0| { 48926:0 <...>, { null }, { [ 0, 0, 5, 0 ] }, 48930:0 <...>, 256, 0, 0, 0, 48935:0 <...>, 32778, { 0, { { [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ], [ 0, 0, 0, 0, 0, 0, 0, 0 ] }, 0, 0, 0 } }, null, 48941:0 <...> }))
- stdout = @(48967:0| 48941:0 <...>)
- stderr = @(48969:0| 48950:0 <...>)
- __cxa_terminate_handler = @(50652:0| 299:0)
- __cxa_unexpected_handler = @(50654:0| 300:0)
- __cxa_new_handler = @(51128:0| null)
- __dso_handle = @(54063:0| null)
- _mpi_num_processes = @(54069:0| 0)
- _mpi_exit_barrier = @(54071:0| 0)
- MPI_CHAR = @(54114:0| null)
- MPI_SHORT = @(54116:0| null)
- MPI_INT = @(54118:0| null)
- MPI_LONG = @(54120:0| null)
- MPI_LONG_LONG_INT = @(54122:0| null)
- MPI_LONG_LONG = @(54124:0| null)
- MPI_SIGNED_CHAR = @(54126:0| null)
- MPI_UNSIGNED_CHAR = @(54128:0| null)
- MPI_UNSIGNED_SHORT = @(54130:0| null)
- MPI_UNSIGNED = @(54132:0| null)
- MPI_UNSIGNED_LONG = @(54134:0| null)
- MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
- MPI_FLOAT = @(54138:0| null)
- MPI_DOUBLE = @(54140:0| null)
- MPI_LONG_DOUBLE = @(54142:0| null)
- MPI_WCHAR = @(54144:0| null)
- MPI_C_BOOL = @(54146:0| null)
- MPI_INT8_T = @(54148:0| null)
- MPI_INT16_T = @(54150:0| null)
- MPI_INT32_T = @(54152:0| null)
- MPI_INT64_T = @(54154:0| null)
- MPI_UINT8_T = @(54156:0| null)
- MPI_UINT16_T = @(54158:0| null)
- MPI_UINT32_T = @(54160:0| null)
- MPI_UINT64_T = @(54162:0| null)
- MPI_AINT = @(54164:0| null)
- MPI_COUNT = @(54166:0| null)
- MPI_OFFSET = @(54168:0| null)
- MPI_C_COMPLEX = @(54170:0| null)
- MPI_C_FLOAT_COMPLEX = @(54172:0| null)
- MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
- MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
- MPI_BYTE = @(54178:0| null)
- MPI_PACKED = @(54180:0| null)
- MPI_FLOAT_INT = @(54182:0| null)
- MPI_DOUBLE_INT = @(54184:0| null)
- MPI_LONG_INT = @(54186:0| null)
- MPI_2INT = @(54188:0| null)
- MPI_SHORT_INT = @(54190:0| null)
- MPI_LONG_DOUBLE_INT = @(54192:0| null)
- MPI_MAX = @(54198:0| null)
- MPI_MIN = @(54200:0| null)
- MPI_SUM = @(54202:0| null)
- MPI_PROD = @(54204:0| null)
- MPI_MAXLOC = @(54206:0| null)
- MPI_MINLOC = @(54208:0| null)
- MPI_BAND = @(54210:0| null)
- MPI_BOR = @(54212:0| null)
- MPI_BXOR = @(54214:0| null)
- MPI_LAND = @(54216:0| null)
- MPI_LOR = @(54218:0| null)
- MPI_LXOR = @(54220:0| null)
- MPI_GROUP_EMPTY = @(54222:0| null)
- MPI_COMM_WORLD_ = @(54226:0| null)
- MPI_COMM_SELF_ = @(54228:0| null)
- thread 0:
- #1: <_divine_start> [ entry.cpp:53 ] [ ctorcount = 5, ctors = 899219456, mainproto = 2, c = @(7:0| @(54884:0| { 65535, 151:0 })), i = @(8:0| 0), r = @(9:0| 0?), i1 = @(10:0| 0?) ]
- #2: <init_stdio> [ posix/_PDCLIB_stdinit.c:794 ] []
- #3: <mtx_init> << %1 = alloca i32, align 4 >> [ mtx = 801996816, type = 1, rc = 0?, attr = 0? ]
- globals:
- key = @(48904:0| null)
- once = @(48906:0| { { 0, 0, 3, 0 } })
- stdin = @(48919:0| @(48920:0| { 48926:0 <...>, { null }, { [ 0, 0, 5, 0 ] }, 48930:0 <...>, 256, 0, 0, 0, 48935:0 <...>, 32778, { 0, { { [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ], [ 0, 0, 0, 0, 0, 0, 0, 0 ] }, 0, 0, 0 } }, null, 48941:0 <...> }))
- stdout = @(48967:0| 48941:0 <...>)
- stderr = @(48969:0| 48950:0 <...>)
- __cxa_terminate_handler = @(50652:0| 299:0)
- __cxa_unexpected_handler = @(50654:0| 300:0)
- __cxa_new_handler = @(51128:0| null)
- __dso_handle = @(54063:0| null)
- _mpi_num_processes = @(54069:0| 0)
- _mpi_exit_barrier = @(54071:0| 0)
- MPI_CHAR = @(54114:0| null)
- MPI_SHORT = @(54116:0| null)
- MPI_INT = @(54118:0| null)
- MPI_LONG = @(54120:0| null)
- MPI_LONG_LONG_INT = @(54122:0| null)
- MPI_LONG_LONG = @(54124:0| null)
- MPI_SIGNED_CHAR = @(54126:0| null)
- MPI_UNSIGNED_CHAR = @(54128:0| null)
- MPI_UNSIGNED_SHORT = @(54130:0| null)
- MPI_UNSIGNED = @(54132:0| null)
- MPI_UNSIGNED_LONG = @(54134:0| null)
- MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
- MPI_FLOAT = @(54138:0| null)
- MPI_DOUBLE = @(54140:0| null)
- MPI_LONG_DOUBLE = @(54142:0| null)
- MPI_WCHAR = @(54144:0| null)
- MPI_C_BOOL = @(54146:0| null)
- MPI_INT8_T = @(54148:0| null)
- MPI_INT16_T = @(54150:0| null)
- MPI_INT32_T = @(54152:0| null)
- MPI_INT64_T = @(54154:0| null)
- MPI_UINT8_T = @(54156:0| null)
- MPI_UINT16_T = @(54158:0| null)
- MPI_UINT32_T = @(54160:0| null)
- MPI_UINT64_T = @(54162:0| null)
- MPI_AINT = @(54164:0| null)
- MPI_COUNT = @(54166:0| null)
- MPI_OFFSET = @(54168:0| null)
- MPI_C_COMPLEX = @(54170:0| null)
- MPI_C_FLOAT_COMPLEX = @(54172:0| null)
- MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
- MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
- MPI_BYTE = @(54178:0| null)
- MPI_PACKED = @(54180:0| null)
- MPI_FLOAT_INT = @(54182:0| null)
- MPI_DOUBLE_INT = @(54184:0| null)
- MPI_LONG_INT = @(54186:0| null)
- MPI_2INT = @(54188:0| null)
- MPI_SHORT_INT = @(54190:0| null)
- MPI_LONG_DOUBLE_INT = @(54192:0| null)
- MPI_MAX = @(54198:0| null)
- MPI_MIN = @(54200:0| null)
- MPI_SUM = @(54202:0| null)
- MPI_PROD = @(54204:0| null)
- MPI_MAXLOC = @(54206:0| null)
- MPI_MINLOC = @(54208:0| null)
- MPI_BAND = @(54210:0| null)
- MPI_BOR = @(54212:0| null)
- MPI_BXOR = @(54214:0| null)
- MPI_LAND = @(54216:0| null)
- MPI_LOR = @(54218:0| null)
- MPI_LXOR = @(54220:0| null)
- MPI_GROUP_EMPTY = @(54222:0| null)
- MPI_COMM_WORLD_ = @(54226:0| null)
- MPI_COMM_SELF_ = @(54228:0| null)
- thread 0:
- #1: <_divine_start> [ entry.cpp:54 ] [ ctorcount = 5, ctors = 899219456, mainproto = 2, c = @(7:0| @(54884:16| { 65535, 895:0 })), i = @(8:0| 1), r = @(9:0| 0?), i1 = @(10:0| 0?) ]
- globals:
- key = @(48904:0| null)
- once = @(48906:0| { { 0, 0, 3, 0 } })
- stdin = @(48919:0| @(48920:0| { 48926:0 <...>, { null }, { [ 0, 0, 5, 0 ] }, 48930:0 <...>, 256, 0, 0, 0, 48935:0 <...>, 32778, { 0, { { [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ], [ 0, 0, 0, 0, 0, 0, 0, 0 ] }, 0, 0, 0 } }, null, 48941:0 <...> }))
- stdout = @(48967:0| 48941:0 <...>)
- stderr = @(48969:0| 48950:0 <...>)
- __cxa_terminate_handler = @(50652:0| 299:0)
- __cxa_unexpected_handler = @(50654:0| 300:0)
- __cxa_new_handler = @(51128:0| null)
- __dso_handle = @(54063:0| null)
- _mpi_num_processes = @(54069:0| 0)
- _mpi_exit_barrier = @(54071:0| 0)
- MPI_CHAR = @(54114:0| null)
- MPI_SHORT = @(54116:0| null)
- MPI_INT = @(54118:0| null)
- MPI_LONG = @(54120:0| null)
- MPI_LONG_LONG_INT = @(54122:0| null)
- MPI_LONG_LONG = @(54124:0| null)
- MPI_SIGNED_CHAR = @(54126:0| null)
- MPI_UNSIGNED_CHAR = @(54128:0| null)
- MPI_UNSIGNED_SHORT = @(54130:0| null)
- MPI_UNSIGNED = @(54132:0| null)
- MPI_UNSIGNED_LONG = @(54134:0| null)
- MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
- MPI_FLOAT = @(54138:0| null)
- MPI_DOUBLE = @(54140:0| null)
- MPI_LONG_DOUBLE = @(54142:0| null)
- MPI_WCHAR = @(54144:0| null)
- MPI_C_BOOL = @(54146:0| null)
- MPI_INT8_T = @(54148:0| null)
- MPI_INT16_T = @(54150:0| null)
- MPI_INT32_T = @(54152:0| null)
- MPI_INT64_T = @(54154:0| null)
- MPI_UINT8_T = @(54156:0| null)
- MPI_UINT16_T = @(54158:0| null)
- MPI_UINT32_T = @(54160:0| null)
- MPI_UINT64_T = @(54162:0| null)
- MPI_AINT = @(54164:0| null)
- MPI_COUNT = @(54166:0| null)
- MPI_OFFSET = @(54168:0| null)
- MPI_C_COMPLEX = @(54170:0| null)
- MPI_C_FLOAT_COMPLEX = @(54172:0| null)
- MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
- MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
- MPI_BYTE = @(54178:0| null)
- MPI_PACKED = @(54180:0| null)
- MPI_FLOAT_INT = @(54182:0| null)
- MPI_DOUBLE_INT = @(54184:0| null)
- MPI_LONG_INT = @(54186:0| null)
- MPI_2INT = @(54188:0| null)
- MPI_SHORT_INT = @(54190:0| null)
- MPI_LONG_DOUBLE_INT = @(54192:0| null)
- MPI_MAX = @(54198:0| null)
- MPI_MIN = @(54200:0| null)
- MPI_SUM = @(54202:0| null)
- MPI_PROD = @(54204:0| null)
- MPI_MAXLOC = @(54206:0| null)
- MPI_MINLOC = @(54208:0| null)
- MPI_BAND = @(54210:0| null)
- MPI_BOR = @(54212:0| null)
- MPI_BXOR = @(54214:0| null)
- MPI_LAND = @(54216:0| null)
- MPI_LOR = @(54218:0| null)
- MPI_LXOR = @(54220:0| null)
- MPI_GROUP_EMPTY = @(54222:0| null)
- MPI_COMM_WORLD_ = @(54226:0| null)
- MPI_COMM_SELF_ = @(54228:0| null)
- thread 0:
- #1: <_divine_start> [ entry.cpp:54 ] [ ctorcount = 5, ctors = 899219456, mainproto = 2, c = @(8:0| @(54884:32| { 65535, 4186:0 })), i = @(9:0| 2), r = @(10:0| 0?), i1 = @(11:0| 0?) ]
- globals:
- key = @(48904:0| null)
- once = @(48906:0| { { 0, 0, 3, 0 } })
- stdin = @(48919:0| @(48920:0| { 48926:0 <...>, { null }, { [ 0, 0, 5, 0 ] }, 48930:0 <...>, 256, 0, 0, 0, 48935:0 <...>, 32778, { 0, { { [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ], [ 0, 0, 0, 0, 0, 0, 0, 0 ] }, 0, 0, 0 } }, null, 48941:0 <...> }))
- stdout = @(48967:0| 48941:0 <...>)
- stderr = @(48969:0| 48950:0 <...>)
- __cxa_terminate_handler = @(50652:0| 299:0)
- __cxa_unexpected_handler = @(50654:0| 300:0)
- __cxa_new_handler = @(51128:0| null)
- __dso_handle = @(54063:0| null)
- _mpi_num_processes = @(54069:0| 0)
- _mpi_exit_barrier = @(54071:0| 0)
- MPI_CHAR = @(54114:0| null)
- MPI_SHORT = @(54116:0| null)
- MPI_INT = @(54118:0| null)
- MPI_LONG = @(54120:0| null)
- MPI_LONG_LONG_INT = @(54122:0| null)
- MPI_LONG_LONG = @(54124:0| null)
- MPI_SIGNED_CHAR = @(54126:0| null)
- MPI_UNSIGNED_CHAR = @(54128:0| null)
- MPI_UNSIGNED_SHORT = @(54130:0| null)
- MPI_UNSIGNED = @(54132:0| null)
- MPI_UNSIGNED_LONG = @(54134:0| null)
- MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
- MPI_FLOAT = @(54138:0| null)
- MPI_DOUBLE = @(54140:0| null)
- MPI_LONG_DOUBLE = @(54142:0| null)
- MPI_WCHAR = @(54144:0| null)
- MPI_C_BOOL = @(54146:0| null)
- MPI_INT8_T = @(54148:0| null)
- MPI_INT16_T = @(54150:0| null)
- MPI_INT32_T = @(54152:0| null)
- MPI_INT64_T = @(54154:0| null)
- MPI_UINT8_T = @(54156:0| null)
- MPI_UINT16_T = @(54158:0| null)
- MPI_UINT32_T = @(54160:0| null)
- MPI_UINT64_T = @(54162:0| null)
- MPI_AINT = @(54164:0| null)
- MPI_COUNT = @(54166:0| null)
- MPI_OFFSET = @(54168:0| null)
- MPI_C_COMPLEX = @(54170:0| null)
- MPI_C_FLOAT_COMPLEX = @(54172:0| null)
- MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
- MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
- MPI_BYTE = @(54178:0| null)
- MPI_PACKED = @(54180:0| null)
- MPI_FLOAT_INT = @(54182:0| null)
- MPI_DOUBLE_INT = @(54184:0| null)
- MPI_LONG_INT = @(54186:0| null)
- MPI_2INT = @(54188:0| null)
- MPI_SHORT_INT = @(54190:0| null)
- MPI_LONG_DOUBLE_INT = @(54192:0| null)
- MPI_MAX = @(54198:0| null)
- MPI_MIN = @(54200:0| null)
- MPI_SUM = @(54202:0| null)
- MPI_PROD = @(54204:0| null)
- MPI_MAXLOC = @(54206:0| null)
- MPI_MINLOC = @(54208:0| null)
- MPI_BAND = @(54210:0| null)
- MPI_BOR = @(54212:0| null)
- MPI_BXOR = @(54214:0| null)
- MPI_LAND = @(54216:0| null)
- MPI_LOR = @(54218:0| null)
- MPI_LXOR = @(54220:0| null)
- MPI_GROUP_EMPTY = @(54222:0| null)
- MPI_COMM_WORLD_ = @(54226:0| null)
- MPI_COMM_SELF_ = @(54228:0| null)
- thread 0:
- #1: <_divine_start> [ entry.cpp:54 ] [ ctorcount = 5, ctors = 899219456, mainproto = 2, c = @(8:0| @(54884:48| { 65535, 4973:0 })), i = @(9:0| 3), r = @(10:0| 0?), i1 = @(11:0| 0?) ]
- globals:
- key = @(48904:0| null)
- once = @(48906:0| { { 0, 0, 3, 0 } })
- stdin = @(48919:0| @(48920:0| { 48926:0 <...>, { null }, { [ 0, 0, 5, 0 ] }, 48930:0 <...>, 256, 0, 0, 0, 48935:0 <...>, 32778, { 0, { { [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ], [ 0, 0, 0, 0, 0, 0, 0, 0 ] }, 0, 0, 0 } }, null, 48941:0 <...> }))
- stdout = @(48967:0| 48941:0 <...>)
- stderr = @(48969:0| 48950:0 <...>)
- __cxa_terminate_handler = @(50652:0| 299:0)
- __cxa_unexpected_handler = @(50654:0| 300:0)
- __cxa_new_handler = @(51128:0| null)
- __dso_handle = @(54063:0| null)
- _mpi_num_processes = @(54069:0| 2)
- _mpi_exit_barrier = @(54071:0| 0)
- MPI_CHAR = @(54114:0| null)
- MPI_SHORT = @(54116:0| null)
- MPI_INT = @(54118:0| null)
- MPI_LONG = @(54120:0| null)
- MPI_LONG_LONG_INT = @(54122:0| null)
- MPI_LONG_LONG = @(54124:0| null)
- MPI_SIGNED_CHAR = @(54126:0| null)
- MPI_UNSIGNED_CHAR = @(54128:0| null)
- MPI_UNSIGNED_SHORT = @(54130:0| null)
- MPI_UNSIGNED = @(54132:0| null)
- MPI_UNSIGNED_LONG = @(54134:0| null)
- MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
- MPI_FLOAT = @(54138:0| null)
- MPI_DOUBLE = @(54140:0| null)
- MPI_LONG_DOUBLE = @(54142:0| null)
- MPI_WCHAR = @(54144:0| null)
- MPI_C_BOOL = @(54146:0| null)
- MPI_INT8_T = @(54148:0| null)
- MPI_INT16_T = @(54150:0| null)
- MPI_INT32_T = @(54152:0| null)
- MPI_INT64_T = @(54154:0| null)
- MPI_UINT8_T = @(54156:0| null)
- MPI_UINT16_T = @(54158:0| null)
- MPI_UINT32_T = @(54160:0| null)
- MPI_UINT64_T = @(54162:0| null)
- MPI_AINT = @(54164:0| null)
- MPI_COUNT = @(54166:0| null)
- MPI_OFFSET = @(54168:0| null)
- MPI_C_COMPLEX = @(54170:0| null)
- MPI_C_FLOAT_COMPLEX = @(54172:0| null)
- MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
- MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
- MPI_BYTE = @(54178:0| null)
- MPI_PACKED = @(54180:0| null)
- MPI_FLOAT_INT = @(54182:0| null)
- MPI_DOUBLE_INT = @(54184:0| null)
- MPI_LONG_INT = @(54186:0| null)
- MPI_2INT = @(54188:0| null)
- MPI_SHORT_INT = @(54190:0| null)
- MPI_LONG_DOUBLE_INT = @(54192:0| null)
- MPI_MAX = @(54198:0| null)
- MPI_MIN = @(54200:0| null)
- MPI_SUM = @(54202:0| null)
- MPI_PROD = @(54204:0| null)
- MPI_MAXLOC = @(54206:0| null)
- MPI_MINLOC = @(54208:0| null)
- MPI_BAND = @(54210:0| null)
- MPI_BOR = @(54212:0| null)
- MPI_BXOR = @(54214:0| null)
- MPI_LAND = @(54216:0| null)
- MPI_LOR = @(54218:0| null)
- MPI_LXOR = @(54220:0| null)
- MPI_GROUP_EMPTY = @(54222:0| null)
- MPI_COMM_WORLD_ = @(54226:0| null)
- MPI_COMM_SELF_ = @(54228:0| null)
- thread 0:
- #1: <_divine_start> [ entry.cpp:54 ] [ ctorcount = 5, ctors = 899219456, mainproto = 2, c = @(8:0| @(54884:64| { 65535, 5060:0 })), i = @(9:0| 4), r = @(10:0| 0?), i1 = @(11:0| 0?) ]
- globals:
- key = @(48904:0| null)
- once = @(48906:0| { { 0, 0, 3, 0 } })
- stdin = @(48919:0| @(48920:0| { 48926:0 <...>, { null }, { [ 0, 0, 5, 0 ] }, 48930:0 <...>, 256, 0, 0, 0, 48935:0 <...>, 32778, { 0, { { [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ], [ 0, 0, 0, 0, 0, 0, 0, 0 ] }, 0, 0, 0 } }, null, 48941:0 <...> }))
- stdout = @(48967:0| 48941:0 <...>)
- stderr = @(48969:0| 48950:0 <...>)
- __cxa_terminate_handler = @(50652:0| 299:0)
- __cxa_unexpected_handler = @(50654:0| 300:0)
- __cxa_new_handler = @(51128:0| null)
- __dso_handle = @(54063:0| null)
- _mpi_num_processes = @(54069:0| 2)
- _mpi_exit_barrier = @(54071:0| 0)
- MPI_CHAR = @(54114:0| null)
- MPI_SHORT = @(54116:0| null)
- MPI_INT = @(54118:0| null)
- MPI_LONG = @(54120:0| null)
- MPI_LONG_LONG_INT = @(54122:0| null)
- MPI_LONG_LONG = @(54124:0| null)
- MPI_SIGNED_CHAR = @(54126:0| null)
- MPI_UNSIGNED_CHAR = @(54128:0| null)
- MPI_UNSIGNED_SHORT = @(54130:0| null)
- MPI_UNSIGNED = @(54132:0| null)
- MPI_UNSIGNED_LONG = @(54134:0| null)
- MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
- MPI_FLOAT = @(54138:0| null)
- MPI_DOUBLE = @(54140:0| null)
- MPI_LONG_DOUBLE = @(54142:0| null)
- MPI_WCHAR = @(54144:0| null)
- MPI_C_BOOL = @(54146:0| null)
- MPI_INT8_T = @(54148:0| null)
- MPI_INT16_T = @(54150:0| null)
- MPI_INT32_T = @(54152:0| null)
- MPI_INT64_T = @(54154:0| null)
- MPI_UINT8_T = @(54156:0| null)
- MPI_UINT16_T = @(54158:0| null)
- MPI_UINT32_T = @(54160:0| null)
- MPI_UINT64_T = @(54162:0| null)
- MPI_AINT = @(54164:0| null)
- MPI_COUNT = @(54166:0| null)
- MPI_OFFSET = @(54168:0| null)
- MPI_C_COMPLEX = @(54170:0| null)
- MPI_C_FLOAT_COMPLEX = @(54172:0| null)
- MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
- MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
- MPI_BYTE = @(54178:0| null)
- MPI_PACKED = @(54180:0| null)
- MPI_FLOAT_INT = @(54182:0| null)
- MPI_DOUBLE_INT = @(54184:0| null)
- MPI_LONG_INT = @(54186:0| null)
- MPI_2INT = @(54188:0| null)
- MPI_SHORT_INT = @(54190:0| null)
- MPI_LONG_DOUBLE_INT = @(54192:0| null)
- MPI_MAX = @(54198:0| null)
- MPI_MIN = @(54200:0| null)
- MPI_SUM = @(54202:0| null)
- MPI_PROD = @(54204:0| null)
- MPI_MAXLOC = @(54206:0| null)
- MPI_MINLOC = @(54208:0| null)
- MPI_BAND = @(54210:0| null)
- MPI_BOR = @(54212:0| null)
- MPI_BXOR = @(54214:0| null)
- MPI_LAND = @(54216:0| null)
- MPI_LOR = @(54218:0| null)
- MPI_LXOR = @(54220:0| null)
- MPI_GROUP_EMPTY = @(54222:0| null)
- MPI_COMM_WORLD_ = @(54226:0| null)
- MPI_COMM_SELF_ = @(54228:0| null)
- thread 0:
- #1: <_divine_start> [ entry.cpp:63 ] [ ctorcount = 5, ctors = 899219456, mainproto = 2, c = @(8:0| @(54884:80| invalid)), i = @(9:0| 5), r = @(10:0| 0?), i1 = @(11:0| 0?) ]
- #2: <_divine_mpi_global_initialize()> [ mpi.cpp:6323 ] []
- globals:
- key = @(48904:0| null)
- once = @(48906:0| { { 0, 0, 3, 0 } })
- stdin = @(48919:0| @(48920:0| { 48926:0 <...>, { null }, { [ 0, 0, 5, 0 ] }, 48930:0 <...>, 256, 0, 0, 0, 48935:0 <...>, 32778, { 0, { { [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ], [ 0, 0, 0, 0, 0, 0, 0, 0 ] }, 0, 0, 0 } }, null, 48941:0 <...> }))
- stdout = @(48967:0| 48941:0 <...>)
- stderr = @(48969:0| 48950:0 <...>)
- __cxa_terminate_handler = @(50652:0| 299:0)
- __cxa_unexpected_handler = @(50654:0| 300:0)
- __cxa_new_handler = @(51128:0| null)
- __dso_handle = @(54063:0| null)
- _mpi_num_processes = @(54069:0| 2)
- _mpi_exit_barrier = @(54071:0| 0)
- MPI_CHAR = @(54114:0| null)
- MPI_SHORT = @(54116:0| null)
- MPI_INT = @(54118:0| null)
- MPI_LONG = @(54120:0| null)
- MPI_LONG_LONG_INT = @(54122:0| null)
- MPI_LONG_LONG = @(54124:0| null)
- MPI_SIGNED_CHAR = @(54126:0| null)
- MPI_UNSIGNED_CHAR = @(54128:0| null)
- MPI_UNSIGNED_SHORT = @(54130:0| null)
- MPI_UNSIGNED = @(54132:0| null)
- MPI_UNSIGNED_LONG = @(54134:0| null)
- MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
- MPI_FLOAT = @(54138:0| null)
- MPI_DOUBLE = @(54140:0| null)
- MPI_LONG_DOUBLE = @(54142:0| null)
- MPI_WCHAR = @(54144:0| null)
- MPI_C_BOOL = @(54146:0| null)
- MPI_INT8_T = @(54148:0| null)
- MPI_INT16_T = @(54150:0| null)
- MPI_INT32_T = @(54152:0| null)
- MPI_INT64_T = @(54154:0| null)
- MPI_UINT8_T = @(54156:0| null)
- MPI_UINT16_T = @(54158:0| null)
- MPI_UINT32_T = @(54160:0| null)
- MPI_UINT64_T = @(54162:0| null)
- MPI_AINT = @(54164:0| null)
- MPI_COUNT = @(54166:0| null)
- MPI_OFFSET = @(54168:0| null)
- MPI_C_COMPLEX = @(54170:0| null)
- MPI_C_FLOAT_COMPLEX = @(54172:0| null)
- MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
- MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
- MPI_BYTE = @(54178:0| null)
- MPI_PACKED = @(54180:0| null)
- MPI_FLOAT_INT = @(54182:0| null)
- MPI_DOUBLE_INT = @(54184:0| null)
- MPI_LONG_INT = @(54186:0| null)
- MPI_2INT = @(54188:0| null)
- MPI_SHORT_INT = @(54190:0| null)
- MPI_LONG_DOUBLE_INT = @(54192:0| null)
- MPI_MAX = @(54198:0| null)
- MPI_MIN = @(54200:0| null)
- MPI_SUM = @(54202:0| null)
- MPI_PROD = @(54204:0| null)
- MPI_MAXLOC = @(54206:0| null)
- MPI_MINLOC = @(54208:0| null)
- MPI_BAND = @(54210:0| null)
- MPI_BOR = @(54212:0| null)
- MPI_BXOR = @(54214:0| null)
- MPI_LAND = @(54216:0| null)
- MPI_LOR = @(54218:0| null)
- MPI_LXOR = @(54220:0| null)
- MPI_GROUP_EMPTY = @(54222:0| null)
- MPI_COMM_WORLD_ = @(54226:0| null)
- MPI_COMM_SELF_ = @(54228:0| null)
- thread 0:
- #1: <_divine_start> [ entry.cpp:63 ] [ ctorcount = 5, ctors = 899219456, mainproto = 2, c = @(9:0| @(54884:80| invalid)), i = @(10:0| 5), r = @(11:0| 0?), i1 = @(12:0| 0?) ]
- #2: <_divine_mpi_global_initialize()> [ mpi.cpp:6324 ] []
- globals:
- key = @(48904:0| null)
- once = @(48906:0| { { 0, 0, 3, 0 } })
- stdin = @(48919:0| @(48920:0| { 48926:0 <...>, { null }, { [ 0, 0, 5, 0 ] }, 48930:0 <...>, 256, 0, 0, 0, 48935:0 <...>, 32778, { 0, { { [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ], [ 0, 0, 0, 0, 0, 0, 0, 0 ] }, 0, 0, 0 } }, null, 48941:0 <...> }))
- stdout = @(48967:0| 48941:0 <...>)
- stderr = @(48969:0| 48950:0 <...>)
- __cxa_terminate_handler = @(50652:0| 299:0)
- __cxa_unexpected_handler = @(50654:0| 300:0)
- __cxa_new_handler = @(51128:0| null)
- __dso_handle = @(54063:0| null)
- _mpi_num_processes = @(54069:0| 2)
- _mpi_exit_barrier = @(54071:0| 0)
- MPI_CHAR = @(54114:0| null)
- MPI_SHORT = @(54116:0| null)
- MPI_INT = @(54118:0| null)
- MPI_LONG = @(54120:0| null)
- MPI_LONG_LONG_INT = @(54122:0| null)
- MPI_LONG_LONG = @(54124:0| null)
- MPI_SIGNED_CHAR = @(54126:0| null)
- MPI_UNSIGNED_CHAR = @(54128:0| null)
- MPI_UNSIGNED_SHORT = @(54130:0| null)
- MPI_UNSIGNED = @(54132:0| null)
- MPI_UNSIGNED_LONG = @(54134:0| null)
- MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
- MPI_FLOAT = @(54138:0| null)
- MPI_DOUBLE = @(54140:0| null)
- MPI_LONG_DOUBLE = @(54142:0| null)
- MPI_WCHAR = @(54144:0| null)
- MPI_C_BOOL = @(54146:0| null)
- MPI_INT8_T = @(54148:0| null)
- MPI_INT16_T = @(54150:0| null)
- MPI_INT32_T = @(54152:0| null)
- MPI_INT64_T = @(54154:0| null)
- MPI_UINT8_T = @(54156:0| null)
- MPI_UINT16_T = @(54158:0| null)
- MPI_UINT32_T = @(54160:0| null)
- MPI_UINT64_T = @(54162:0| null)
- MPI_AINT = @(54164:0| null)
- MPI_COUNT = @(54166:0| null)
- MPI_OFFSET = @(54168:0| null)
- MPI_C_COMPLEX = @(54170:0| null)
- MPI_C_FLOAT_COMPLEX = @(54172:0| null)
- MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
- MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
- MPI_BYTE = @(54178:0| null)
- MPI_PACKED = @(54180:0| null)
- MPI_FLOAT_INT = @(54182:0| null)
- MPI_DOUBLE_INT = @(54184:0| null)
- MPI_LONG_INT = @(54186:0| null)
- MPI_2INT = @(54188:0| null)
- MPI_SHORT_INT = @(54190:0| null)
- MPI_LONG_DOUBLE_INT = @(54192:0| null)
- MPI_MAX = @(54198:0| null)
- MPI_MIN = @(54200:0| null)
- MPI_SUM = @(54202:0| null)
- MPI_PROD = @(54204:0| null)
- MPI_MAXLOC = @(54206:0| null)
- MPI_MINLOC = @(54208:0| null)
- MPI_BAND = @(54210:0| null)
- MPI_BOR = @(54212:0| null)
- MPI_BXOR = @(54214:0| null)
- MPI_LAND = @(54216:0| null)
- MPI_LOR = @(54218:0| null)
- MPI_LXOR = @(54220:0| null)
- MPI_GROUP_EMPTY = @(54222:0| null)
- MPI_COMM_WORLD_ = @(54226:0| null)
- MPI_COMM_SELF_ = @(54228:0| null)
- thread 0:
- #1: <_divine_start> [ entry.cpp:63 ] [ ctorcount = 5, ctors = 899219456, mainproto = 2, c = @(10:0| @(54884:80| invalid)), i = @(11:0| 5), r = @(12:0| 0?), i1 = @(13:0| 0?) ]
- #2: <_divine_mpi_global_initialize()> [ mpi.cpp:6325 ] []
- globals:
- key = @(48904:0| null)
- once = @(48906:0| { { 0, 0, 3, 0 } })
- stdin = @(48919:0| @(48920:0| { 48926:0 <...>, { null }, { [ 0, 0, 5, 0 ] }, 48930:0 <...>, 256, 0, 0, 0, 48935:0 <...>, 32778, { 0, { { [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ], [ 0, 0, 0, 0, 0, 0, 0, 0 ] }, 0, 0, 0 } }, null, 48941:0 <...> }))
- stdout = @(48967:0| 48941:0 <...>)
- stderr = @(48969:0| 48950:0 <...>)
- __cxa_terminate_handler = @(50652:0| 299:0)
- __cxa_unexpected_handler = @(50654:0| 300:0)
- __cxa_new_handler = @(51128:0| null)
- __dso_handle = @(54063:0| null)
- _mpi_num_processes = @(54069:0| 2)
- _mpi_exit_barrier = @(54071:0| 0)
- MPI_CHAR = @(54114:0| null)
- MPI_SHORT = @(54116:0| null)
- MPI_INT = @(54118:0| null)
- MPI_LONG = @(54120:0| null)
- MPI_LONG_LONG_INT = @(54122:0| null)
- MPI_LONG_LONG = @(54124:0| null)
- MPI_SIGNED_CHAR = @(54126:0| null)
- MPI_UNSIGNED_CHAR = @(54128:0| null)
- MPI_UNSIGNED_SHORT = @(54130:0| null)
- MPI_UNSIGNED = @(54132:0| null)
- MPI_UNSIGNED_LONG = @(54134:0| null)
- MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
- MPI_FLOAT = @(54138:0| null)
- MPI_DOUBLE = @(54140:0| null)
- MPI_LONG_DOUBLE = @(54142:0| null)
- MPI_WCHAR = @(54144:0| null)
- MPI_C_BOOL = @(54146:0| null)
- MPI_INT8_T = @(54148:0| null)
- MPI_INT16_T = @(54150:0| null)
- MPI_INT32_T = @(54152:0| null)
- MPI_INT64_T = @(54154:0| null)
- MPI_UINT8_T = @(54156:0| null)
- MPI_UINT16_T = @(54158:0| null)
- MPI_UINT32_T = @(54160:0| null)
- MPI_UINT64_T = @(54162:0| null)
- MPI_AINT = @(54164:0| null)
- MPI_COUNT = @(54166:0| null)
- MPI_OFFSET = @(54168:0| null)
- MPI_C_COMPLEX = @(54170:0| null)
- MPI_C_FLOAT_COMPLEX = @(54172:0| null)
- MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
- MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
- MPI_BYTE = @(54178:0| null)
- MPI_PACKED = @(54180:0| null)
- MPI_FLOAT_INT = @(54182:0| null)
- MPI_DOUBLE_INT = @(54184:0| null)
- MPI_LONG_INT = @(54186:0| null)
- MPI_2INT = @(54188:0| null)
- MPI_SHORT_INT = @(54190:0| null)
- MPI_LONG_DOUBLE_INT = @(54192:0| null)
- MPI_MAX = @(54198:0| null)
- MPI_MIN = @(54200:0| null)
- MPI_SUM = @(54202:0| null)
- MPI_PROD = @(54204:0| null)
- MPI_MAXLOC = @(54206:0| null)
- MPI_MINLOC = @(54208:0| null)
- MPI_BAND = @(54210:0| null)
- MPI_BOR = @(54212:0| null)
- MPI_BXOR = @(54214:0| null)
- MPI_LAND = @(54216:0| null)
- MPI_LOR = @(54218:0| null)
- MPI_LXOR = @(54220:0| null)
- MPI_GROUP_EMPTY = @(54222:0| null)
- MPI_COMM_WORLD_ = @(54226:0| null)
- MPI_COMM_SELF_ = @(54228:0| null)
- thread 0:
- #1: <_divine_start> [ entry.cpp:63 ] [ ctorcount = 5, ctors = 899219456, mainproto = 2, c = @(11:0| @(54884:80| invalid)), i = @(12:0| 5), r = @(13:0| 0?), i1 = @(14:0| 0?) ]
- #2: <_divine_mpi_global_initialize()> [ mpi.cpp:6329 ] []
- UNDEFINED VALUE (thread 0): <_divine_mpi_global_initialize()> [ mpi.cpp:6329 ] << %62 = select i1 %60, i64 -1, i64 %61, !dbg !110198 >>
- ===== The goal =====
- globals:
- key = @(48904:0| null)
- once = @(48906:0| { { 0, 0, 3, 0 } })
- stdin = @(48919:0| @(48920:0| { 48926:0 <...>, { null }, { [ 0, 0, 5, 0 ] }, 48930:0 <...>, 256, 0, 0, 0, 48935:0 <...>, 32778, { 0, { { [ 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 ], [ 0, 0, 0, 0, 0, 0, 0, 0 ] }, 0, 0, 0 } }, null, 48941:0 <...> }))
- stdout = @(48967:0| 48941:0 <...>)
- stderr = @(48969:0| 48950:0 <...>)
- __cxa_terminate_handler = @(50652:0| 299:0)
- __cxa_unexpected_handler = @(50654:0| 300:0)
- __cxa_new_handler = @(51128:0| null)
- __dso_handle = @(54063:0| null)
- _mpi_num_processes = @(54069:0| 2)
- _mpi_exit_barrier = @(54071:0| 0)
- MPI_CHAR = @(54114:0| null)
- MPI_SHORT = @(54116:0| null)
- MPI_INT = @(54118:0| null)
- MPI_LONG = @(54120:0| null)
- MPI_LONG_LONG_INT = @(54122:0| null)
- MPI_LONG_LONG = @(54124:0| null)
- MPI_SIGNED_CHAR = @(54126:0| null)
- MPI_UNSIGNED_CHAR = @(54128:0| null)
- MPI_UNSIGNED_SHORT = @(54130:0| null)
- MPI_UNSIGNED = @(54132:0| null)
- MPI_UNSIGNED_LONG = @(54134:0| null)
- MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
- MPI_FLOAT = @(54138:0| null)
- MPI_DOUBLE = @(54140:0| null)
- MPI_LONG_DOUBLE = @(54142:0| null)
- MPI_WCHAR = @(54144:0| null)
- MPI_C_BOOL = @(54146:0| null)
- MPI_INT8_T = @(54148:0| null)
- MPI_INT16_T = @(54150:0| null)
- MPI_INT32_T = @(54152:0| null)
- MPI_INT64_T = @(54154:0| null)
- MPI_UINT8_T = @(54156:0| null)
- MPI_UINT16_T = @(54158:0| null)
- MPI_UINT32_T = @(54160:0| null)
- MPI_UINT64_T = @(54162:0| null)
- MPI_AINT = @(54164:0| null)
- MPI_COUNT = @(54166:0| null)
- MPI_OFFSET = @(54168:0| null)
- MPI_C_COMPLEX = @(54170:0| null)
- MPI_C_FLOAT_COMPLEX = @(54172:0| null)
- MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
- MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
- MPI_BYTE = @(54178:0| null)
- MPI_PACKED = @(54180:0| null)
- MPI_FLOAT_INT = @(54182:0| null)
- MPI_DOUBLE_INT = @(54184:0| null)
- MPI_LONG_INT = @(54186:0| null)
- MPI_2INT = @(54188:0| null)
- MPI_SHORT_INT = @(54190:0| null)
- MPI_LONG_DOUBLE_INT = @(54192:0| null)
- MPI_MAX = @(54198:0| null)
- MPI_MIN = @(54200:0| null)
- MPI_SUM = @(54202:0| null)
- MPI_PROD = @(54204:0| null)
- MPI_MAXLOC = @(54206:0| null)
- MPI_MINLOC = @(54208:0| null)
- MPI_BAND = @(54210:0| null)
- MPI_BOR = @(54212:0| null)
- MPI_BXOR = @(54214:0| null)
- MPI_LAND = @(54216:0| null)
- MPI_LOR = @(54218:0| null)
- MPI_LXOR = @(54220:0| null)
- MPI_GROUP_EMPTY = @(54222:0| null)
- MPI_COMM_WORLD_ = @(54226:0| null)
- MPI_COMM_SELF_ = @(54228:0| null)
- thread 0:
- #1: <_divine_start> [ entry.cpp:63 ] [ ctorcount = 5, ctors = 899219456, mainproto = 2, c = @(11:0| @(54884:80| invalid)), i = @(12:0| 5), r = @(13:0| 0?), i1 = @(14:0| 0?) ]
- #2: <_divine_mpi_global_initialize()> [ mpi.cpp:6329 ] []
- UNDEFINED VALUE (thread 0): <_divine_mpi_global_initialize()> [ mpi.cpp:6329 ] << %62 = select i1 %60, i64 -1, i64 %61, !dbg !110198 >>
- =============================================
- The property DOES NOT hold
- =============================================
- <...>
- hashsize=524288; states=11; queues=1; vmpeak=143964; vm=143964; vmperst=13401739; rsspeak=41844; rss=33704; rssperst=3137536; statesmem=137; avgstate=12799; time=751;
- <...>
- hashsize=524288; states=11; queues=1; vmpeak=143964; vm=143964; vmperst=13401739; rsspeak=41844; rss=33704; rssperst=3137536; statesmem=137; avgstate=12799; time=1000;
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement