API tools faq
paste
Advertisement
Guest User

Untitled

a guest
Dec 7th, 2015
66
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 34.02 KB | None | 0 0
raw download clone embed print report
  1. input: hello.bc
  2. <...> property { safety }: [assert + memory + arithmetic + leak + user + guard + mutex]
  3. ---------------- Reachability ----------------
  4.  
  5. meta: model=hello.bc; algorithm=reachability; visitor=shared; compression=tree; threads=8; mpinodes=1;
  6. searching... 10 states, 10 edges, GOAL
  7.  
  8. ===== Trace from initial =====
  9.  
  10. globals:
  11. key = @(48904:0| null)
  12. once = @(48906:0| { { 0, 0, 3, 0 } })
  13. 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 <...> }))
  14. stdout = @(48967:0| 48941:0 <...>)
  15. stderr = @(48969:0| 48950:0 <...>)
  16. __cxa_terminate_handler = @(50652:0| 299:0)
  17. __cxa_unexpected_handler = @(50654:0| 300:0)
  18. __cxa_new_handler = @(51128:0| null)
  19. __dso_handle = @(54063:0| null)
  20. _mpi_num_processes = @(54069:0| 0)
  21. _mpi_exit_barrier = @(54071:0| 0)
  22. MPI_CHAR = @(54114:0| null)
  23. MPI_SHORT = @(54116:0| null)
  24. MPI_INT = @(54118:0| null)
  25. MPI_LONG = @(54120:0| null)
  26. MPI_LONG_LONG_INT = @(54122:0| null)
  27. MPI_LONG_LONG = @(54124:0| null)
  28. MPI_SIGNED_CHAR = @(54126:0| null)
  29. MPI_UNSIGNED_CHAR = @(54128:0| null)
  30. MPI_UNSIGNED_SHORT = @(54130:0| null)
  31. MPI_UNSIGNED = @(54132:0| null)
  32. MPI_UNSIGNED_LONG = @(54134:0| null)
  33. MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
  34. MPI_FLOAT = @(54138:0| null)
  35. MPI_DOUBLE = @(54140:0| null)
  36. MPI_LONG_DOUBLE = @(54142:0| null)
  37. MPI_WCHAR = @(54144:0| null)
  38. MPI_C_BOOL = @(54146:0| null)
  39. MPI_INT8_T = @(54148:0| null)
  40. MPI_INT16_T = @(54150:0| null)
  41. MPI_INT32_T = @(54152:0| null)
  42. MPI_INT64_T = @(54154:0| null)
  43. MPI_UINT8_T = @(54156:0| null)
  44. MPI_UINT16_T = @(54158:0| null)
  45. MPI_UINT32_T = @(54160:0| null)
  46. MPI_UINT64_T = @(54162:0| null)
  47. MPI_AINT = @(54164:0| null)
  48. MPI_COUNT = @(54166:0| null)
  49. MPI_OFFSET = @(54168:0| null)
  50. MPI_C_COMPLEX = @(54170:0| null)
  51. MPI_C_FLOAT_COMPLEX = @(54172:0| null)
  52. MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
  53. MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
  54. MPI_BYTE = @(54178:0| null)
  55. MPI_PACKED = @(54180:0| null)
  56. MPI_FLOAT_INT = @(54182:0| null)
  57. MPI_DOUBLE_INT = @(54184:0| null)
  58. MPI_LONG_INT = @(54186:0| null)
  59. MPI_2INT = @(54188:0| null)
  60. MPI_SHORT_INT = @(54190:0| null)
  61. MPI_LONG_DOUBLE_INT = @(54192:0| null)
  62. MPI_MAX = @(54198:0| null)
  63. MPI_MIN = @(54200:0| null)
  64. MPI_SUM = @(54202:0| null)
  65. MPI_PROD = @(54204:0| null)
  66. MPI_MAXLOC = @(54206:0| null)
  67. MPI_MINLOC = @(54208:0| null)
  68. MPI_BAND = @(54210:0| null)
  69. MPI_BOR = @(54212:0| null)
  70. MPI_BXOR = @(54214:0| null)
  71. MPI_LAND = @(54216:0| null)
  72. MPI_LOR = @(54218:0| null)
  73. MPI_LXOR = @(54220:0| null)
  74. MPI_GROUP_EMPTY = @(54222:0| null)
  75. MPI_COMM_WORLD_ = @(54226:0| null)
  76. MPI_COMM_SELF_ = @(54228:0| null)
  77. thread 0:
  78. #1: <_divine_start> << %1 = alloca i32, align 4 >> [ ctorcount = 5, ctors = 899219456, mainproto = 2, c = 0?, i = 0?, r = 0?, i1 = 0? ]
  79.  
  80. globals:
  81. key = @(48904:0| null)
  82. once = @(48906:0| { { 0, 0, 3, 0 } })
  83. 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 <...> }))
  84. stdout = @(48967:0| 48941:0 <...>)
  85. stderr = @(48969:0| 48950:0 <...>)
  86. __cxa_terminate_handler = @(50652:0| 299:0)
  87. __cxa_unexpected_handler = @(50654:0| 300:0)
  88. __cxa_new_handler = @(51128:0| null)
  89. __dso_handle = @(54063:0| null)
  90. _mpi_num_processes = @(54069:0| 0)
  91. _mpi_exit_barrier = @(54071:0| 0)
  92. MPI_CHAR = @(54114:0| null)
  93. MPI_SHORT = @(54116:0| null)
  94. MPI_INT = @(54118:0| null)
  95. MPI_LONG = @(54120:0| null)
  96. MPI_LONG_LONG_INT = @(54122:0| null)
  97. MPI_LONG_LONG = @(54124:0| null)
  98. MPI_SIGNED_CHAR = @(54126:0| null)
  99. MPI_UNSIGNED_CHAR = @(54128:0| null)
  100. MPI_UNSIGNED_SHORT = @(54130:0| null)
  101. MPI_UNSIGNED = @(54132:0| null)
  102. MPI_UNSIGNED_LONG = @(54134:0| null)
  103. MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
  104. MPI_FLOAT = @(54138:0| null)
  105. MPI_DOUBLE = @(54140:0| null)
  106. MPI_LONG_DOUBLE = @(54142:0| null)
  107. MPI_WCHAR = @(54144:0| null)
  108. MPI_C_BOOL = @(54146:0| null)
  109. MPI_INT8_T = @(54148:0| null)
  110. MPI_INT16_T = @(54150:0| null)
  111. MPI_INT32_T = @(54152:0| null)
  112. MPI_INT64_T = @(54154:0| null)
  113. MPI_UINT8_T = @(54156:0| null)
  114. MPI_UINT16_T = @(54158:0| null)
  115. MPI_UINT32_T = @(54160:0| null)
  116. MPI_UINT64_T = @(54162:0| null)
  117. MPI_AINT = @(54164:0| null)
  118. MPI_COUNT = @(54166:0| null)
  119. MPI_OFFSET = @(54168:0| null)
  120. MPI_C_COMPLEX = @(54170:0| null)
  121. MPI_C_FLOAT_COMPLEX = @(54172:0| null)
  122. MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
  123. MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
  124. MPI_BYTE = @(54178:0| null)
  125. MPI_PACKED = @(54180:0| null)
  126. MPI_FLOAT_INT = @(54182:0| null)
  127. MPI_DOUBLE_INT = @(54184:0| null)
  128. MPI_LONG_INT = @(54186:0| null)
  129. MPI_2INT = @(54188:0| null)
  130. MPI_SHORT_INT = @(54190:0| null)
  131. MPI_LONG_DOUBLE_INT = @(54192:0| null)
  132. MPI_MAX = @(54198:0| null)
  133. MPI_MIN = @(54200:0| null)
  134. MPI_SUM = @(54202:0| null)
  135. MPI_PROD = @(54204:0| null)
  136. MPI_MAXLOC = @(54206:0| null)
  137. MPI_MINLOC = @(54208:0| null)
  138. MPI_BAND = @(54210:0| null)
  139. MPI_BOR = @(54212:0| null)
  140. MPI_BXOR = @(54214:0| null)
  141. MPI_LAND = @(54216:0| null)
  142. MPI_LOR = @(54218:0| null)
  143. MPI_LXOR = @(54220:0| null)
  144. MPI_GROUP_EMPTY = @(54222:0| null)
  145. MPI_COMM_WORLD_ = @(54226:0| null)
  146. MPI_COMM_SELF_ = @(54228:0| null)
  147. thread 0:
  148. #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?) ]
  149. #2: <init_stdio> [ posix/_PDCLIB_stdinit.c:792 ] []
  150. #3: <mtx_init> << %1 = alloca i32, align 4 >> [ mtx = 801849360, type = 1, rc = 0?, attr = 0? ]
  151.  
  152. globals:
  153. key = @(48904:0| null)
  154. once = @(48906:0| { { 0, 0, 3, 0 } })
  155. 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 <...> }))
  156. stdout = @(48967:0| 48941:0 <...>)
  157. stderr = @(48969:0| 48950:0 <...>)
  158. __cxa_terminate_handler = @(50652:0| 299:0)
  159. __cxa_unexpected_handler = @(50654:0| 300:0)
  160. __cxa_new_handler = @(51128:0| null)
  161. __dso_handle = @(54063:0| null)
  162. _mpi_num_processes = @(54069:0| 0)
  163. _mpi_exit_barrier = @(54071:0| 0)
  164. MPI_CHAR = @(54114:0| null)
  165. MPI_SHORT = @(54116:0| null)
  166. MPI_INT = @(54118:0| null)
  167. MPI_LONG = @(54120:0| null)
  168. MPI_LONG_LONG_INT = @(54122:0| null)
  169. MPI_LONG_LONG = @(54124:0| null)
  170. MPI_SIGNED_CHAR = @(54126:0| null)
  171. MPI_UNSIGNED_CHAR = @(54128:0| null)
  172. MPI_UNSIGNED_SHORT = @(54130:0| null)
  173. MPI_UNSIGNED = @(54132:0| null)
  174. MPI_UNSIGNED_LONG = @(54134:0| null)
  175. MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
  176. MPI_FLOAT = @(54138:0| null)
  177. MPI_DOUBLE = @(54140:0| null)
  178. MPI_LONG_DOUBLE = @(54142:0| null)
  179. MPI_WCHAR = @(54144:0| null)
  180. MPI_C_BOOL = @(54146:0| null)
  181. MPI_INT8_T = @(54148:0| null)
  182. MPI_INT16_T = @(54150:0| null)
  183. MPI_INT32_T = @(54152:0| null)
  184. MPI_INT64_T = @(54154:0| null)
  185. MPI_UINT8_T = @(54156:0| null)
  186. MPI_UINT16_T = @(54158:0| null)
  187. MPI_UINT32_T = @(54160:0| null)
  188. MPI_UINT64_T = @(54162:0| null)
  189. MPI_AINT = @(54164:0| null)
  190. MPI_COUNT = @(54166:0| null)
  191. MPI_OFFSET = @(54168:0| null)
  192. MPI_C_COMPLEX = @(54170:0| null)
  193. MPI_C_FLOAT_COMPLEX = @(54172:0| null)
  194. MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
  195. MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
  196. MPI_BYTE = @(54178:0| null)
  197. MPI_PACKED = @(54180:0| null)
  198. MPI_FLOAT_INT = @(54182:0| null)
  199. MPI_DOUBLE_INT = @(54184:0| null)
  200. MPI_LONG_INT = @(54186:0| null)
  201. MPI_2INT = @(54188:0| null)
  202. MPI_SHORT_INT = @(54190:0| null)
  203. MPI_LONG_DOUBLE_INT = @(54192:0| null)
  204. MPI_MAX = @(54198:0| null)
  205. MPI_MIN = @(54200:0| null)
  206. MPI_SUM = @(54202:0| null)
  207. MPI_PROD = @(54204:0| null)
  208. MPI_MAXLOC = @(54206:0| null)
  209. MPI_MINLOC = @(54208:0| null)
  210. MPI_BAND = @(54210:0| null)
  211. MPI_BOR = @(54212:0| null)
  212. MPI_BXOR = @(54214:0| null)
  213. MPI_LAND = @(54216:0| null)
  214. MPI_LOR = @(54218:0| null)
  215. MPI_LXOR = @(54220:0| null)
  216. MPI_GROUP_EMPTY = @(54222:0| null)
  217. MPI_COMM_WORLD_ = @(54226:0| null)
  218. MPI_COMM_SELF_ = @(54228:0| null)
  219. thread 0:
  220. #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?) ]
  221. #2: <init_stdio> [ posix/_PDCLIB_stdinit.c:794 ] []
  222. #3: <mtx_init> << %1 = alloca i32, align 4 >> [ mtx = 801996816, type = 1, rc = 0?, attr = 0? ]
  223.  
  224. globals:
  225. key = @(48904:0| null)
  226. once = @(48906:0| { { 0, 0, 3, 0 } })
  227. 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 <...> }))
  228. stdout = @(48967:0| 48941:0 <...>)
  229. stderr = @(48969:0| 48950:0 <...>)
  230. __cxa_terminate_handler = @(50652:0| 299:0)
  231. __cxa_unexpected_handler = @(50654:0| 300:0)
  232. __cxa_new_handler = @(51128:0| null)
  233. __dso_handle = @(54063:0| null)
  234. _mpi_num_processes = @(54069:0| 0)
  235. _mpi_exit_barrier = @(54071:0| 0)
  236. MPI_CHAR = @(54114:0| null)
  237. MPI_SHORT = @(54116:0| null)
  238. MPI_INT = @(54118:0| null)
  239. MPI_LONG = @(54120:0| null)
  240. MPI_LONG_LONG_INT = @(54122:0| null)
  241. MPI_LONG_LONG = @(54124:0| null)
  242. MPI_SIGNED_CHAR = @(54126:0| null)
  243. MPI_UNSIGNED_CHAR = @(54128:0| null)
  244. MPI_UNSIGNED_SHORT = @(54130:0| null)
  245. MPI_UNSIGNED = @(54132:0| null)
  246. MPI_UNSIGNED_LONG = @(54134:0| null)
  247. MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
  248. MPI_FLOAT = @(54138:0| null)
  249. MPI_DOUBLE = @(54140:0| null)
  250. MPI_LONG_DOUBLE = @(54142:0| null)
  251. MPI_WCHAR = @(54144:0| null)
  252. MPI_C_BOOL = @(54146:0| null)
  253. MPI_INT8_T = @(54148:0| null)
  254. MPI_INT16_T = @(54150:0| null)
  255. MPI_INT32_T = @(54152:0| null)
  256. MPI_INT64_T = @(54154:0| null)
  257. MPI_UINT8_T = @(54156:0| null)
  258. MPI_UINT16_T = @(54158:0| null)
  259. MPI_UINT32_T = @(54160:0| null)
  260. MPI_UINT64_T = @(54162:0| null)
  261. MPI_AINT = @(54164:0| null)
  262. MPI_COUNT = @(54166:0| null)
  263. MPI_OFFSET = @(54168:0| null)
  264. MPI_C_COMPLEX = @(54170:0| null)
  265. MPI_C_FLOAT_COMPLEX = @(54172:0| null)
  266. MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
  267. MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
  268. MPI_BYTE = @(54178:0| null)
  269. MPI_PACKED = @(54180:0| null)
  270. MPI_FLOAT_INT = @(54182:0| null)
  271. MPI_DOUBLE_INT = @(54184:0| null)
  272. MPI_LONG_INT = @(54186:0| null)
  273. MPI_2INT = @(54188:0| null)
  274. MPI_SHORT_INT = @(54190:0| null)
  275. MPI_LONG_DOUBLE_INT = @(54192:0| null)
  276. MPI_MAX = @(54198:0| null)
  277. MPI_MIN = @(54200:0| null)
  278. MPI_SUM = @(54202:0| null)
  279. MPI_PROD = @(54204:0| null)
  280. MPI_MAXLOC = @(54206:0| null)
  281. MPI_MINLOC = @(54208:0| null)
  282. MPI_BAND = @(54210:0| null)
  283. MPI_BOR = @(54212:0| null)
  284. MPI_BXOR = @(54214:0| null)
  285. MPI_LAND = @(54216:0| null)
  286. MPI_LOR = @(54218:0| null)
  287. MPI_LXOR = @(54220:0| null)
  288. MPI_GROUP_EMPTY = @(54222:0| null)
  289. MPI_COMM_WORLD_ = @(54226:0| null)
  290. MPI_COMM_SELF_ = @(54228:0| null)
  291. thread 0:
  292. #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?) ]
  293.  
  294. globals:
  295. key = @(48904:0| null)
  296. once = @(48906:0| { { 0, 0, 3, 0 } })
  297. 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 <...> }))
  298. stdout = @(48967:0| 48941:0 <...>)
  299. stderr = @(48969:0| 48950:0 <...>)
  300. __cxa_terminate_handler = @(50652:0| 299:0)
  301. __cxa_unexpected_handler = @(50654:0| 300:0)
  302. __cxa_new_handler = @(51128:0| null)
  303. __dso_handle = @(54063:0| null)
  304. _mpi_num_processes = @(54069:0| 0)
  305. _mpi_exit_barrier = @(54071:0| 0)
  306. MPI_CHAR = @(54114:0| null)
  307. MPI_SHORT = @(54116:0| null)
  308. MPI_INT = @(54118:0| null)
  309. MPI_LONG = @(54120:0| null)
  310. MPI_LONG_LONG_INT = @(54122:0| null)
  311. MPI_LONG_LONG = @(54124:0| null)
  312. MPI_SIGNED_CHAR = @(54126:0| null)
  313. MPI_UNSIGNED_CHAR = @(54128:0| null)
  314. MPI_UNSIGNED_SHORT = @(54130:0| null)
  315. MPI_UNSIGNED = @(54132:0| null)
  316. MPI_UNSIGNED_LONG = @(54134:0| null)
  317. MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
  318. MPI_FLOAT = @(54138:0| null)
  319. MPI_DOUBLE = @(54140:0| null)
  320. MPI_LONG_DOUBLE = @(54142:0| null)
  321. MPI_WCHAR = @(54144:0| null)
  322. MPI_C_BOOL = @(54146:0| null)
  323. MPI_INT8_T = @(54148:0| null)
  324. MPI_INT16_T = @(54150:0| null)
  325. MPI_INT32_T = @(54152:0| null)
  326. MPI_INT64_T = @(54154:0| null)
  327. MPI_UINT8_T = @(54156:0| null)
  328. MPI_UINT16_T = @(54158:0| null)
  329. MPI_UINT32_T = @(54160:0| null)
  330. MPI_UINT64_T = @(54162:0| null)
  331. MPI_AINT = @(54164:0| null)
  332. MPI_COUNT = @(54166:0| null)
  333. MPI_OFFSET = @(54168:0| null)
  334. MPI_C_COMPLEX = @(54170:0| null)
  335. MPI_C_FLOAT_COMPLEX = @(54172:0| null)
  336. MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
  337. MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
  338. MPI_BYTE = @(54178:0| null)
  339. MPI_PACKED = @(54180:0| null)
  340. MPI_FLOAT_INT = @(54182:0| null)
  341. MPI_DOUBLE_INT = @(54184:0| null)
  342. MPI_LONG_INT = @(54186:0| null)
  343. MPI_2INT = @(54188:0| null)
  344. MPI_SHORT_INT = @(54190:0| null)
  345. MPI_LONG_DOUBLE_INT = @(54192:0| null)
  346. MPI_MAX = @(54198:0| null)
  347. MPI_MIN = @(54200:0| null)
  348. MPI_SUM = @(54202:0| null)
  349. MPI_PROD = @(54204:0| null)
  350. MPI_MAXLOC = @(54206:0| null)
  351. MPI_MINLOC = @(54208:0| null)
  352. MPI_BAND = @(54210:0| null)
  353. MPI_BOR = @(54212:0| null)
  354. MPI_BXOR = @(54214:0| null)
  355. MPI_LAND = @(54216:0| null)
  356. MPI_LOR = @(54218:0| null)
  357. MPI_LXOR = @(54220:0| null)
  358. MPI_GROUP_EMPTY = @(54222:0| null)
  359. MPI_COMM_WORLD_ = @(54226:0| null)
  360. MPI_COMM_SELF_ = @(54228:0| null)
  361. thread 0:
  362. #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?) ]
  363.  
  364. globals:
  365. key = @(48904:0| null)
  366. once = @(48906:0| { { 0, 0, 3, 0 } })
  367. 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 <...> }))
  368. stdout = @(48967:0| 48941:0 <...>)
  369. stderr = @(48969:0| 48950:0 <...>)
  370. __cxa_terminate_handler = @(50652:0| 299:0)
  371. __cxa_unexpected_handler = @(50654:0| 300:0)
  372. __cxa_new_handler = @(51128:0| null)
  373. __dso_handle = @(54063:0| null)
  374. _mpi_num_processes = @(54069:0| 0)
  375. _mpi_exit_barrier = @(54071:0| 0)
  376. MPI_CHAR = @(54114:0| null)
  377. MPI_SHORT = @(54116:0| null)
  378. MPI_INT = @(54118:0| null)
  379. MPI_LONG = @(54120:0| null)
  380. MPI_LONG_LONG_INT = @(54122:0| null)
  381. MPI_LONG_LONG = @(54124:0| null)
  382. MPI_SIGNED_CHAR = @(54126:0| null)
  383. MPI_UNSIGNED_CHAR = @(54128:0| null)
  384. MPI_UNSIGNED_SHORT = @(54130:0| null)
  385. MPI_UNSIGNED = @(54132:0| null)
  386. MPI_UNSIGNED_LONG = @(54134:0| null)
  387. MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
  388. MPI_FLOAT = @(54138:0| null)
  389. MPI_DOUBLE = @(54140:0| null)
  390. MPI_LONG_DOUBLE = @(54142:0| null)
  391. MPI_WCHAR = @(54144:0| null)
  392. MPI_C_BOOL = @(54146:0| null)
  393. MPI_INT8_T = @(54148:0| null)
  394. MPI_INT16_T = @(54150:0| null)
  395. MPI_INT32_T = @(54152:0| null)
  396. MPI_INT64_T = @(54154:0| null)
  397. MPI_UINT8_T = @(54156:0| null)
  398. MPI_UINT16_T = @(54158:0| null)
  399. MPI_UINT32_T = @(54160:0| null)
  400. MPI_UINT64_T = @(54162:0| null)
  401. MPI_AINT = @(54164:0| null)
  402. MPI_COUNT = @(54166:0| null)
  403. MPI_OFFSET = @(54168:0| null)
  404. MPI_C_COMPLEX = @(54170:0| null)
  405. MPI_C_FLOAT_COMPLEX = @(54172:0| null)
  406. MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
  407. MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
  408. MPI_BYTE = @(54178:0| null)
  409. MPI_PACKED = @(54180:0| null)
  410. MPI_FLOAT_INT = @(54182:0| null)
  411. MPI_DOUBLE_INT = @(54184:0| null)
  412. MPI_LONG_INT = @(54186:0| null)
  413. MPI_2INT = @(54188:0| null)
  414. MPI_SHORT_INT = @(54190:0| null)
  415. MPI_LONG_DOUBLE_INT = @(54192:0| null)
  416. MPI_MAX = @(54198:0| null)
  417. MPI_MIN = @(54200:0| null)
  418. MPI_SUM = @(54202:0| null)
  419. MPI_PROD = @(54204:0| null)
  420. MPI_MAXLOC = @(54206:0| null)
  421. MPI_MINLOC = @(54208:0| null)
  422. MPI_BAND = @(54210:0| null)
  423. MPI_BOR = @(54212:0| null)
  424. MPI_BXOR = @(54214:0| null)
  425. MPI_LAND = @(54216:0| null)
  426. MPI_LOR = @(54218:0| null)
  427. MPI_LXOR = @(54220:0| null)
  428. MPI_GROUP_EMPTY = @(54222:0| null)
  429. MPI_COMM_WORLD_ = @(54226:0| null)
  430. MPI_COMM_SELF_ = @(54228:0| null)
  431. thread 0:
  432. #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?) ]
  433.  
  434. globals:
  435. key = @(48904:0| null)
  436. once = @(48906:0| { { 0, 0, 3, 0 } })
  437. 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 <...> }))
  438. stdout = @(48967:0| 48941:0 <...>)
  439. stderr = @(48969:0| 48950:0 <...>)
  440. __cxa_terminate_handler = @(50652:0| 299:0)
  441. __cxa_unexpected_handler = @(50654:0| 300:0)
  442. __cxa_new_handler = @(51128:0| null)
  443. __dso_handle = @(54063:0| null)
  444. _mpi_num_processes = @(54069:0| 2)
  445. _mpi_exit_barrier = @(54071:0| 0)
  446. MPI_CHAR = @(54114:0| null)
  447. MPI_SHORT = @(54116:0| null)
  448. MPI_INT = @(54118:0| null)
  449. MPI_LONG = @(54120:0| null)
  450. MPI_LONG_LONG_INT = @(54122:0| null)
  451. MPI_LONG_LONG = @(54124:0| null)
  452. MPI_SIGNED_CHAR = @(54126:0| null)
  453. MPI_UNSIGNED_CHAR = @(54128:0| null)
  454. MPI_UNSIGNED_SHORT = @(54130:0| null)
  455. MPI_UNSIGNED = @(54132:0| null)
  456. MPI_UNSIGNED_LONG = @(54134:0| null)
  457. MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
  458. MPI_FLOAT = @(54138:0| null)
  459. MPI_DOUBLE = @(54140:0| null)
  460. MPI_LONG_DOUBLE = @(54142:0| null)
  461. MPI_WCHAR = @(54144:0| null)
  462. MPI_C_BOOL = @(54146:0| null)
  463. MPI_INT8_T = @(54148:0| null)
  464. MPI_INT16_T = @(54150:0| null)
  465. MPI_INT32_T = @(54152:0| null)
  466. MPI_INT64_T = @(54154:0| null)
  467. MPI_UINT8_T = @(54156:0| null)
  468. MPI_UINT16_T = @(54158:0| null)
  469. MPI_UINT32_T = @(54160:0| null)
  470. MPI_UINT64_T = @(54162:0| null)
  471. MPI_AINT = @(54164:0| null)
  472. MPI_COUNT = @(54166:0| null)
  473. MPI_OFFSET = @(54168:0| null)
  474. MPI_C_COMPLEX = @(54170:0| null)
  475. MPI_C_FLOAT_COMPLEX = @(54172:0| null)
  476. MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
  477. MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
  478. MPI_BYTE = @(54178:0| null)
  479. MPI_PACKED = @(54180:0| null)
  480. MPI_FLOAT_INT = @(54182:0| null)
  481. MPI_DOUBLE_INT = @(54184:0| null)
  482. MPI_LONG_INT = @(54186:0| null)
  483. MPI_2INT = @(54188:0| null)
  484. MPI_SHORT_INT = @(54190:0| null)
  485. MPI_LONG_DOUBLE_INT = @(54192:0| null)
  486. MPI_MAX = @(54198:0| null)
  487. MPI_MIN = @(54200:0| null)
  488. MPI_SUM = @(54202:0| null)
  489. MPI_PROD = @(54204:0| null)
  490. MPI_MAXLOC = @(54206:0| null)
  491. MPI_MINLOC = @(54208:0| null)
  492. MPI_BAND = @(54210:0| null)
  493. MPI_BOR = @(54212:0| null)
  494. MPI_BXOR = @(54214:0| null)
  495. MPI_LAND = @(54216:0| null)
  496. MPI_LOR = @(54218:0| null)
  497. MPI_LXOR = @(54220:0| null)
  498. MPI_GROUP_EMPTY = @(54222:0| null)
  499. MPI_COMM_WORLD_ = @(54226:0| null)
  500. MPI_COMM_SELF_ = @(54228:0| null)
  501. thread 0:
  502. #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?) ]
  503.  
  504. globals:
  505. key = @(48904:0| null)
  506. once = @(48906:0| { { 0, 0, 3, 0 } })
  507. 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 <...> }))
  508. stdout = @(48967:0| 48941:0 <...>)
  509. stderr = @(48969:0| 48950:0 <...>)
  510. __cxa_terminate_handler = @(50652:0| 299:0)
  511. __cxa_unexpected_handler = @(50654:0| 300:0)
  512. __cxa_new_handler = @(51128:0| null)
  513. __dso_handle = @(54063:0| null)
  514. _mpi_num_processes = @(54069:0| 2)
  515. _mpi_exit_barrier = @(54071:0| 0)
  516. MPI_CHAR = @(54114:0| null)
  517. MPI_SHORT = @(54116:0| null)
  518. MPI_INT = @(54118:0| null)
  519. MPI_LONG = @(54120:0| null)
  520. MPI_LONG_LONG_INT = @(54122:0| null)
  521. MPI_LONG_LONG = @(54124:0| null)
  522. MPI_SIGNED_CHAR = @(54126:0| null)
  523. MPI_UNSIGNED_CHAR = @(54128:0| null)
  524. MPI_UNSIGNED_SHORT = @(54130:0| null)
  525. MPI_UNSIGNED = @(54132:0| null)
  526. MPI_UNSIGNED_LONG = @(54134:0| null)
  527. MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
  528. MPI_FLOAT = @(54138:0| null)
  529. MPI_DOUBLE = @(54140:0| null)
  530. MPI_LONG_DOUBLE = @(54142:0| null)
  531. MPI_WCHAR = @(54144:0| null)
  532. MPI_C_BOOL = @(54146:0| null)
  533. MPI_INT8_T = @(54148:0| null)
  534. MPI_INT16_T = @(54150:0| null)
  535. MPI_INT32_T = @(54152:0| null)
  536. MPI_INT64_T = @(54154:0| null)
  537. MPI_UINT8_T = @(54156:0| null)
  538. MPI_UINT16_T = @(54158:0| null)
  539. MPI_UINT32_T = @(54160:0| null)
  540. MPI_UINT64_T = @(54162:0| null)
  541. MPI_AINT = @(54164:0| null)
  542. MPI_COUNT = @(54166:0| null)
  543. MPI_OFFSET = @(54168:0| null)
  544. MPI_C_COMPLEX = @(54170:0| null)
  545. MPI_C_FLOAT_COMPLEX = @(54172:0| null)
  546. MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
  547. MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
  548. MPI_BYTE = @(54178:0| null)
  549. MPI_PACKED = @(54180:0| null)
  550. MPI_FLOAT_INT = @(54182:0| null)
  551. MPI_DOUBLE_INT = @(54184:0| null)
  552. MPI_LONG_INT = @(54186:0| null)
  553. MPI_2INT = @(54188:0| null)
  554. MPI_SHORT_INT = @(54190:0| null)
  555. MPI_LONG_DOUBLE_INT = @(54192:0| null)
  556. MPI_MAX = @(54198:0| null)
  557. MPI_MIN = @(54200:0| null)
  558. MPI_SUM = @(54202:0| null)
  559. MPI_PROD = @(54204:0| null)
  560. MPI_MAXLOC = @(54206:0| null)
  561. MPI_MINLOC = @(54208:0| null)
  562. MPI_BAND = @(54210:0| null)
  563. MPI_BOR = @(54212:0| null)
  564. MPI_BXOR = @(54214:0| null)
  565. MPI_LAND = @(54216:0| null)
  566. MPI_LOR = @(54218:0| null)
  567. MPI_LXOR = @(54220:0| null)
  568. MPI_GROUP_EMPTY = @(54222:0| null)
  569. MPI_COMM_WORLD_ = @(54226:0| null)
  570. MPI_COMM_SELF_ = @(54228:0| null)
  571. thread 0:
  572. #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?) ]
  573. #2: <_divine_mpi_global_initialize()> [ mpi.cpp:6323 ] []
  574.  
  575. globals:
  576. key = @(48904:0| null)
  577. once = @(48906:0| { { 0, 0, 3, 0 } })
  578. 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 <...> }))
  579. stdout = @(48967:0| 48941:0 <...>)
  580. stderr = @(48969:0| 48950:0 <...>)
  581. __cxa_terminate_handler = @(50652:0| 299:0)
  582. __cxa_unexpected_handler = @(50654:0| 300:0)
  583. __cxa_new_handler = @(51128:0| null)
  584. __dso_handle = @(54063:0| null)
  585. _mpi_num_processes = @(54069:0| 2)
  586. _mpi_exit_barrier = @(54071:0| 0)
  587. MPI_CHAR = @(54114:0| null)
  588. MPI_SHORT = @(54116:0| null)
  589. MPI_INT = @(54118:0| null)
  590. MPI_LONG = @(54120:0| null)
  591. MPI_LONG_LONG_INT = @(54122:0| null)
  592. MPI_LONG_LONG = @(54124:0| null)
  593. MPI_SIGNED_CHAR = @(54126:0| null)
  594. MPI_UNSIGNED_CHAR = @(54128:0| null)
  595. MPI_UNSIGNED_SHORT = @(54130:0| null)
  596. MPI_UNSIGNED = @(54132:0| null)
  597. MPI_UNSIGNED_LONG = @(54134:0| null)
  598. MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
  599. MPI_FLOAT = @(54138:0| null)
  600. MPI_DOUBLE = @(54140:0| null)
  601. MPI_LONG_DOUBLE = @(54142:0| null)
  602. MPI_WCHAR = @(54144:0| null)
  603. MPI_C_BOOL = @(54146:0| null)
  604. MPI_INT8_T = @(54148:0| null)
  605. MPI_INT16_T = @(54150:0| null)
  606. MPI_INT32_T = @(54152:0| null)
  607. MPI_INT64_T = @(54154:0| null)
  608. MPI_UINT8_T = @(54156:0| null)
  609. MPI_UINT16_T = @(54158:0| null)
  610. MPI_UINT32_T = @(54160:0| null)
  611. MPI_UINT64_T = @(54162:0| null)
  612. MPI_AINT = @(54164:0| null)
  613. MPI_COUNT = @(54166:0| null)
  614. MPI_OFFSET = @(54168:0| null)
  615. MPI_C_COMPLEX = @(54170:0| null)
  616. MPI_C_FLOAT_COMPLEX = @(54172:0| null)
  617. MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
  618. MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
  619. MPI_BYTE = @(54178:0| null)
  620. MPI_PACKED = @(54180:0| null)
  621. MPI_FLOAT_INT = @(54182:0| null)
  622. MPI_DOUBLE_INT = @(54184:0| null)
  623. MPI_LONG_INT = @(54186:0| null)
  624. MPI_2INT = @(54188:0| null)
  625. MPI_SHORT_INT = @(54190:0| null)
  626. MPI_LONG_DOUBLE_INT = @(54192:0| null)
  627. MPI_MAX = @(54198:0| null)
  628. MPI_MIN = @(54200:0| null)
  629. MPI_SUM = @(54202:0| null)
  630. MPI_PROD = @(54204:0| null)
  631. MPI_MAXLOC = @(54206:0| null)
  632. MPI_MINLOC = @(54208:0| null)
  633. MPI_BAND = @(54210:0| null)
  634. MPI_BOR = @(54212:0| null)
  635. MPI_BXOR = @(54214:0| null)
  636. MPI_LAND = @(54216:0| null)
  637. MPI_LOR = @(54218:0| null)
  638. MPI_LXOR = @(54220:0| null)
  639. MPI_GROUP_EMPTY = @(54222:0| null)
  640. MPI_COMM_WORLD_ = @(54226:0| null)
  641. MPI_COMM_SELF_ = @(54228:0| null)
  642. thread 0:
  643. #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?) ]
  644. #2: <_divine_mpi_global_initialize()> [ mpi.cpp:6324 ] []
  645.  
  646. globals:
  647. key = @(48904:0| null)
  648. once = @(48906:0| { { 0, 0, 3, 0 } })
  649. 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 <...> }))
  650. stdout = @(48967:0| 48941:0 <...>)
  651. stderr = @(48969:0| 48950:0 <...>)
  652. __cxa_terminate_handler = @(50652:0| 299:0)
  653. __cxa_unexpected_handler = @(50654:0| 300:0)
  654. __cxa_new_handler = @(51128:0| null)
  655. __dso_handle = @(54063:0| null)
  656. _mpi_num_processes = @(54069:0| 2)
  657. _mpi_exit_barrier = @(54071:0| 0)
  658. MPI_CHAR = @(54114:0| null)
  659. MPI_SHORT = @(54116:0| null)
  660. MPI_INT = @(54118:0| null)
  661. MPI_LONG = @(54120:0| null)
  662. MPI_LONG_LONG_INT = @(54122:0| null)
  663. MPI_LONG_LONG = @(54124:0| null)
  664. MPI_SIGNED_CHAR = @(54126:0| null)
  665. MPI_UNSIGNED_CHAR = @(54128:0| null)
  666. MPI_UNSIGNED_SHORT = @(54130:0| null)
  667. MPI_UNSIGNED = @(54132:0| null)
  668. MPI_UNSIGNED_LONG = @(54134:0| null)
  669. MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
  670. MPI_FLOAT = @(54138:0| null)
  671. MPI_DOUBLE = @(54140:0| null)
  672. MPI_LONG_DOUBLE = @(54142:0| null)
  673. MPI_WCHAR = @(54144:0| null)
  674. MPI_C_BOOL = @(54146:0| null)
  675. MPI_INT8_T = @(54148:0| null)
  676. MPI_INT16_T = @(54150:0| null)
  677. MPI_INT32_T = @(54152:0| null)
  678. MPI_INT64_T = @(54154:0| null)
  679. MPI_UINT8_T = @(54156:0| null)
  680. MPI_UINT16_T = @(54158:0| null)
  681. MPI_UINT32_T = @(54160:0| null)
  682. MPI_UINT64_T = @(54162:0| null)
  683. MPI_AINT = @(54164:0| null)
  684. MPI_COUNT = @(54166:0| null)
  685. MPI_OFFSET = @(54168:0| null)
  686. MPI_C_COMPLEX = @(54170:0| null)
  687. MPI_C_FLOAT_COMPLEX = @(54172:0| null)
  688. MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
  689. MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
  690. MPI_BYTE = @(54178:0| null)
  691. MPI_PACKED = @(54180:0| null)
  692. MPI_FLOAT_INT = @(54182:0| null)
  693. MPI_DOUBLE_INT = @(54184:0| null)
  694. MPI_LONG_INT = @(54186:0| null)
  695. MPI_2INT = @(54188:0| null)
  696. MPI_SHORT_INT = @(54190:0| null)
  697. MPI_LONG_DOUBLE_INT = @(54192:0| null)
  698. MPI_MAX = @(54198:0| null)
  699. MPI_MIN = @(54200:0| null)
  700. MPI_SUM = @(54202:0| null)
  701. MPI_PROD = @(54204:0| null)
  702. MPI_MAXLOC = @(54206:0| null)
  703. MPI_MINLOC = @(54208:0| null)
  704. MPI_BAND = @(54210:0| null)
  705. MPI_BOR = @(54212:0| null)
  706. MPI_BXOR = @(54214:0| null)
  707. MPI_LAND = @(54216:0| null)
  708. MPI_LOR = @(54218:0| null)
  709. MPI_LXOR = @(54220:0| null)
  710. MPI_GROUP_EMPTY = @(54222:0| null)
  711. MPI_COMM_WORLD_ = @(54226:0| null)
  712. MPI_COMM_SELF_ = @(54228:0| null)
  713. thread 0:
  714. #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?) ]
  715. #2: <_divine_mpi_global_initialize()> [ mpi.cpp:6325 ] []
  716.  
  717. globals:
  718. key = @(48904:0| null)
  719. once = @(48906:0| { { 0, 0, 3, 0 } })
  720. 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 <...> }))
  721. stdout = @(48967:0| 48941:0 <...>)
  722. stderr = @(48969:0| 48950:0 <...>)
  723. __cxa_terminate_handler = @(50652:0| 299:0)
  724. __cxa_unexpected_handler = @(50654:0| 300:0)
  725. __cxa_new_handler = @(51128:0| null)
  726. __dso_handle = @(54063:0| null)
  727. _mpi_num_processes = @(54069:0| 2)
  728. _mpi_exit_barrier = @(54071:0| 0)
  729. MPI_CHAR = @(54114:0| null)
  730. MPI_SHORT = @(54116:0| null)
  731. MPI_INT = @(54118:0| null)
  732. MPI_LONG = @(54120:0| null)
  733. MPI_LONG_LONG_INT = @(54122:0| null)
  734. MPI_LONG_LONG = @(54124:0| null)
  735. MPI_SIGNED_CHAR = @(54126:0| null)
  736. MPI_UNSIGNED_CHAR = @(54128:0| null)
  737. MPI_UNSIGNED_SHORT = @(54130:0| null)
  738. MPI_UNSIGNED = @(54132:0| null)
  739. MPI_UNSIGNED_LONG = @(54134:0| null)
  740. MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
  741. MPI_FLOAT = @(54138:0| null)
  742. MPI_DOUBLE = @(54140:0| null)
  743. MPI_LONG_DOUBLE = @(54142:0| null)
  744. MPI_WCHAR = @(54144:0| null)
  745. MPI_C_BOOL = @(54146:0| null)
  746. MPI_INT8_T = @(54148:0| null)
  747. MPI_INT16_T = @(54150:0| null)
  748. MPI_INT32_T = @(54152:0| null)
  749. MPI_INT64_T = @(54154:0| null)
  750. MPI_UINT8_T = @(54156:0| null)
  751. MPI_UINT16_T = @(54158:0| null)
  752. MPI_UINT32_T = @(54160:0| null)
  753. MPI_UINT64_T = @(54162:0| null)
  754. MPI_AINT = @(54164:0| null)
  755. MPI_COUNT = @(54166:0| null)
  756. MPI_OFFSET = @(54168:0| null)
  757. MPI_C_COMPLEX = @(54170:0| null)
  758. MPI_C_FLOAT_COMPLEX = @(54172:0| null)
  759. MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
  760. MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
  761. MPI_BYTE = @(54178:0| null)
  762. MPI_PACKED = @(54180:0| null)
  763. MPI_FLOAT_INT = @(54182:0| null)
  764. MPI_DOUBLE_INT = @(54184:0| null)
  765. MPI_LONG_INT = @(54186:0| null)
  766. MPI_2INT = @(54188:0| null)
  767. MPI_SHORT_INT = @(54190:0| null)
  768. MPI_LONG_DOUBLE_INT = @(54192:0| null)
  769. MPI_MAX = @(54198:0| null)
  770. MPI_MIN = @(54200:0| null)
  771. MPI_SUM = @(54202:0| null)
  772. MPI_PROD = @(54204:0| null)
  773. MPI_MAXLOC = @(54206:0| null)
  774. MPI_MINLOC = @(54208:0| null)
  775. MPI_BAND = @(54210:0| null)
  776. MPI_BOR = @(54212:0| null)
  777. MPI_BXOR = @(54214:0| null)
  778. MPI_LAND = @(54216:0| null)
  779. MPI_LOR = @(54218:0| null)
  780. MPI_LXOR = @(54220:0| null)
  781. MPI_GROUP_EMPTY = @(54222:0| null)
  782. MPI_COMM_WORLD_ = @(54226:0| null)
  783. MPI_COMM_SELF_ = @(54228:0| null)
  784. thread 0:
  785. #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?) ]
  786. #2: <_divine_mpi_global_initialize()> [ mpi.cpp:6329 ] []
  787. UNDEFINED VALUE (thread 0): <_divine_mpi_global_initialize()> [ mpi.cpp:6329 ] << %62 = select i1 %60, i64 -1, i64 %61, !dbg !110198 >>
  788.  
  789.  
  790. ===== The goal =====
  791.  
  792. globals:
  793. key = @(48904:0| null)
  794. once = @(48906:0| { { 0, 0, 3, 0 } })
  795. 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 <...> }))
  796. stdout = @(48967:0| 48941:0 <...>)
  797. stderr = @(48969:0| 48950:0 <...>)
  798. __cxa_terminate_handler = @(50652:0| 299:0)
  799. __cxa_unexpected_handler = @(50654:0| 300:0)
  800. __cxa_new_handler = @(51128:0| null)
  801. __dso_handle = @(54063:0| null)
  802. _mpi_num_processes = @(54069:0| 2)
  803. _mpi_exit_barrier = @(54071:0| 0)
  804. MPI_CHAR = @(54114:0| null)
  805. MPI_SHORT = @(54116:0| null)
  806. MPI_INT = @(54118:0| null)
  807. MPI_LONG = @(54120:0| null)
  808. MPI_LONG_LONG_INT = @(54122:0| null)
  809. MPI_LONG_LONG = @(54124:0| null)
  810. MPI_SIGNED_CHAR = @(54126:0| null)
  811. MPI_UNSIGNED_CHAR = @(54128:0| null)
  812. MPI_UNSIGNED_SHORT = @(54130:0| null)
  813. MPI_UNSIGNED = @(54132:0| null)
  814. MPI_UNSIGNED_LONG = @(54134:0| null)
  815. MPI_UNSIGNED_LONG_LONG = @(54136:0| null)
  816. MPI_FLOAT = @(54138:0| null)
  817. MPI_DOUBLE = @(54140:0| null)
  818. MPI_LONG_DOUBLE = @(54142:0| null)
  819. MPI_WCHAR = @(54144:0| null)
  820. MPI_C_BOOL = @(54146:0| null)
  821. MPI_INT8_T = @(54148:0| null)
  822. MPI_INT16_T = @(54150:0| null)
  823. MPI_INT32_T = @(54152:0| null)
  824. MPI_INT64_T = @(54154:0| null)
  825. MPI_UINT8_T = @(54156:0| null)
  826. MPI_UINT16_T = @(54158:0| null)
  827. MPI_UINT32_T = @(54160:0| null)
  828. MPI_UINT64_T = @(54162:0| null)
  829. MPI_AINT = @(54164:0| null)
  830. MPI_COUNT = @(54166:0| null)
  831. MPI_OFFSET = @(54168:0| null)
  832. MPI_C_COMPLEX = @(54170:0| null)
  833. MPI_C_FLOAT_COMPLEX = @(54172:0| null)
  834. MPI_C_DOUBLE_COMPLEX = @(54174:0| null)
  835. MPI_C_LONG_DOUBLE_COMPLEX = @(54176:0| null)
  836. MPI_BYTE = @(54178:0| null)
  837. MPI_PACKED = @(54180:0| null)
  838. MPI_FLOAT_INT = @(54182:0| null)
  839. MPI_DOUBLE_INT = @(54184:0| null)
  840. MPI_LONG_INT = @(54186:0| null)
  841. MPI_2INT = @(54188:0| null)
  842. MPI_SHORT_INT = @(54190:0| null)
  843. MPI_LONG_DOUBLE_INT = @(54192:0| null)
  844. MPI_MAX = @(54198:0| null)
  845. MPI_MIN = @(54200:0| null)
  846. MPI_SUM = @(54202:0| null)
  847. MPI_PROD = @(54204:0| null)
  848. MPI_MAXLOC = @(54206:0| null)
  849. MPI_MINLOC = @(54208:0| null)
  850. MPI_BAND = @(54210:0| null)
  851. MPI_BOR = @(54212:0| null)
  852. MPI_BXOR = @(54214:0| null)
  853. MPI_LAND = @(54216:0| null)
  854. MPI_LOR = @(54218:0| null)
  855. MPI_LXOR = @(54220:0| null)
  856. MPI_GROUP_EMPTY = @(54222:0| null)
  857. MPI_COMM_WORLD_ = @(54226:0| null)
  858. MPI_COMM_SELF_ = @(54228:0| null)
  859. thread 0:
  860. #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?) ]
  861. #2: <_divine_mpi_global_initialize()> [ mpi.cpp:6329 ] []
  862. UNDEFINED VALUE (thread 0): <_divine_mpi_global_initialize()> [ mpi.cpp:6329 ] << %62 = select i1 %60, i64 -1, i64 %61, !dbg !110198 >>
  863.  
  864. =============================================
  865. The property DOES NOT hold
  866. =============================================
  867. <...>
  868. hashsize=524288; states=11; queues=1; vmpeak=143964; vm=143964; vmperst=13401739; rsspeak=41844; rss=33704; rssperst=3137536; statesmem=137; avgstate=12799; time=751;
  869. <...>
  870. 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
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!