Failed
projectroot.MBI.mbi_ReqLifecycle_MissingWait_Isend_Recv_init_nok (from CTest)
Stacktrace
| Compiling ./mbi_ReqLifecycle_MissingWait_Isend_Recv_init_nok.c (batchinfo:) | | $ | | | Executing the command | $ /builds/workspace/SimGrid-DynamicAnalysis-Coverage/label/debian-testing/build/smpi_script/bin/smpirun -wrapper '/builds/workspace/SimGrid-DynamicAnalysis-Coverage/label/debian-testing/build/bin/simgrid-mc --cfg=model-check/reduction:odpor --log=mc_safety.t:info' -platform ./cluster.xml -analyze --cfg=smpi/barrier-finalization:on --cfg=smpi/list-leaks:10 --cfg=model-check/max-depth:10000 -np 2 ./mbi_ReqLifecycle_MissingWait_Isend_Recv_init_nok | | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/privatization' to 'ON' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/np' to '2' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/hostfile' to '' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'precision/timing' to '1e-9' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'network/model' to 'SMPI' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/display-timing' to 'yes' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/display-allocs' to 'yes' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/list-leaks' to '50' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/pedantic' to 'true' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/barrier-collectives' to 'true' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/barrier-finalization' to 'on' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/list-leaks' to '10' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/max-depth' to '10000' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/tmpdir' to '/tmp' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/privatization' to 'ON' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/np' to '2' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/hostfile' to '' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'precision/timing' to '1e-9' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'network/model' to 'SMPI' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/display-timing' to 'yes' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/display-allocs' to 'yes' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/list-leaks' to '50' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/pedantic' to 'true' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/barrier-collectives' to 'true' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/barrier-finalization' to 'on' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/list-leaks' to '10' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/max-depth' to '10000' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/tmpdir' to '/tmp' | Hello from rank 0 | Hello from rank 1 | [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor. | Rank 0 finished normally | Rank 1 finished normally | [0.000000] [smpi_utils/INFO] Allocations analysis asked, but 0 bytes were allocated through malloc/calloc calls intercepted by SMPI. | The code may not use malloc() to allocate memory, or it was built with SMPI_NO_OVERRIDE_MALLOC | [0.000000] [mc_dfs/INFO] DFS exploration ended. 13 unique states visited; 1 explored traces (0 transition replays, 13 states visited overall) | | Wait up to 300 seconds Command return code: 0, elapsed time: 0.1952686309814453 XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX SimGrid gave the wrong result on ./mbi_ReqLifecycle_MissingWait_Isend_Recv_init_nok (OK instead of MissingWait). Expected diagnostic: ERROR: MissingWait
Standard Output
| Compiling ./mbi_ReqLifecycle_MissingWait_Isend_Recv_init_nok.c (batchinfo:) | | $ | | | Executing the command | $ /builds/workspace/SimGrid-DynamicAnalysis-Coverage/label/debian-testing/build/smpi_script/bin/smpirun -wrapper '/builds/workspace/SimGrid-DynamicAnalysis-Coverage/label/debian-testing/build/bin/simgrid-mc --cfg=model-check/reduction:odpor --log=mc_safety.t:info' -platform ./cluster.xml -analyze --cfg=smpi/barrier-finalization:on --cfg=smpi/list-leaks:10 --cfg=model-check/max-depth:10000 -np 2 ./mbi_ReqLifecycle_MissingWait_Isend_Recv_init_nok | | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/reduction' to 'odpor' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/privatization' to 'ON' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/np' to '2' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/hostfile' to '' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'precision/timing' to '1e-9' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'network/model' to 'SMPI' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/display-timing' to 'yes' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/display-allocs' to 'yes' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/list-leaks' to '50' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/pedantic' to 'true' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/barrier-collectives' to 'true' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/barrier-finalization' to 'on' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/list-leaks' to '10' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/max-depth' to '10000' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/tmpdir' to '/tmp' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/privatization' to 'ON' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/np' to '2' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/hostfile' to '' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'precision/timing' to '1e-9' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'network/model' to 'SMPI' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/display-timing' to 'yes' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/display-allocs' to 'yes' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/list-leaks' to '50' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/pedantic' to 'true' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/barrier-collectives' to 'true' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/barrier-finalization' to 'on' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/list-leaks' to '10' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'model-check/max-depth' to '10000' | [0.000000] [xbt_cfg/INFO] Configuration change: Set 'smpi/tmpdir' to '/tmp' | Hello from rank 0 | Hello from rank 1 | [0.000000] [mc_dfs/INFO] Start a DFS exploration. Reduction is: odpor. | Rank 0 finished normally | Rank 1 finished normally | [0.000000] [smpi_utils/INFO] Allocations analysis asked, but 0 bytes were allocated through malloc/calloc calls intercepted by SMPI. | The code may not use malloc() to allocate memory, or it was built with SMPI_NO_OVERRIDE_MALLOC | [0.000000] [mc_dfs/INFO] DFS exploration ended. 13 unique states visited; 1 explored traces (0 transition replays, 13 states visited overall) | | Wait up to 300 seconds Command return code: 0, elapsed time: 0.1952686309814453 XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX SimGrid gave the wrong result on ./mbi_ReqLifecycle_MissingWait_Isend_Recv_init_nok (OK instead of MissingWait). Expected diagnostic: ERROR: MissingWait