teshsuite/mc/random-bug/random-bug.tesh

   1 #!/usr/bin/env tesh
   2 ! expect return 1
   3 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning
   4 > [  0.000000] (0:maestro@) Behavior: assert
   5 > [  0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
   6 > [  0.000000] (0:maestro@) Behavior: assert
   7 > [  0.000000] (0:maestro@) Behavior: assert
   8 > [  0.000000] (0:maestro@) Behavior: assert
   9 > [  0.000000] (0:maestro@) Behavior: assert
  10 > [  0.000000] (0:maestro@) Behavior: assert
  11 > [  0.000000] (0:maestro@) Behavior: assert
  12 > [  0.000000] (0:maestro@) Behavior: assert
  13 > [  0.000000] (0:maestro@) Behavior: assert
  14 > [  0.000000] (0:maestro@) Behavior: assert
  15 > [  0.000000] (0:maestro@) Behavior: assert
  16 > [  0.000000] (0:maestro@) Behavior: assert
  17 > [  0.000000] (0:maestro@) Behavior: assert
  18 > [  0.000000] (0:maestro@) Behavior: assert
  19 > [  0.000000] (0:maestro@) Behavior: assert
  20 > [  0.000000] (0:maestro@) Behavior: assert
  21 > [  0.000000] (0:maestro@) Behavior: assert
  22 > [  0.000000] (0:maestro@) Behavior: assert
  23 > [  0.000000] (0:maestro@) Behavior: assert
  24 > [  0.000000] (0:maestro@) Behavior: assert
  25 > [  0.000000] (0:maestro@) Behavior: assert
  26 > [  0.000000] (0:maestro@) Behavior: assert
  27 > [  0.000000] (0:maestro@) Behavior: assert
  28 > [  0.000000] (0:maestro@) **************************
  29 > [  0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
  30 > [  0.000000] (0:maestro@) **************************
  31 > [  0.000000] (0:maestro@) Counter-example execution trace:
  32 > [  0.000000] (0:maestro@)   1: Random([0;5] ~> 3)
  33 > [  0.000000] (0:maestro@)   1: Random([0;5] ~> 4)
  34 > [  0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
  35 > [  0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall)
  36
  37 ! expect return 6
  38 # because SIMGRID_MC_EXIT_PROGRAM_CRASH = 6
  39 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug abort ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning --log=no_loc
  40 > [  0.000000] (0:maestro@) Behavior: abort
  41 > [  0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
  42 > [  0.000000] (0:maestro@) Behavior: abort
  43 > [  0.000000] (0:maestro@) Behavior: abort
  44 > [  0.000000] (0:maestro@) Behavior: abort
  45 > [  0.000000] (0:maestro@) Behavior: abort
  46 > [  0.000000] (0:maestro@) Behavior: abort
  47 > [  0.000000] (0:maestro@) Behavior: abort
  48 > [  0.000000] (0:maestro@) Behavior: abort
  49 > [  0.000000] (0:maestro@) Behavior: abort
  50 > [  0.000000] (0:maestro@) Behavior: abort
  51 > [  0.000000] (0:maestro@) Behavior: abort
  52 > [  0.000000] (0:maestro@) Behavior: abort
  53 > [  0.000000] (0:maestro@) Behavior: abort
  54 > [  0.000000] (0:maestro@) Behavior: abort
  55 > [  0.000000] (0:maestro@) Behavior: abort
  56 > [  0.000000] (0:maestro@) Behavior: abort
  57 > [  0.000000] (0:maestro@) Behavior: abort
  58 > [  0.000000] (0:maestro@) Behavior: abort
  59 > [  0.000000] (0:maestro@) Behavior: abort
  60 > [  0.000000] (0:maestro@) Behavior: abort
  61 > [  0.000000] (0:maestro@) Behavior: abort
  62 > [  0.000000] (0:maestro@) Behavior: abort
  63 > [  0.000000] (0:maestro@) Behavior: abort
  64 > [  0.000000] (0:maestro@) **************************
  65 > [  0.000000] (0:maestro@) ** CRASH IN THE PROGRAM **
  66 > [  0.000000] (0:maestro@) **************************
  67 > [  0.000000] (0:maestro@) From signal: Aborted
  68 > [  0.000000] (0:maestro@) Counter-example execution trace:
  69 > [  0.000000] (0:maestro@)   1: Random([0;5] ~> 3)
  70 > [  0.000000] (0:maestro@)   1: Random([0;5] ~> 4)
  71 > [  0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
  72 > [  0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall)
  73 > [  0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc
  74
  75 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug printf ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning
  76 > [  0.000000] (0:maestro@) Behavior: printf
  77 > [  0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
  78 > [  0.000000] (0:maestro@) Behavior: printf
  79 > [  0.000000] (0:maestro@) Behavior: printf
  80 > [  0.000000] (0:maestro@) Behavior: printf
  81 > [  0.000000] (0:maestro@) Behavior: printf
  82 > [  0.000000] (0:maestro@) Behavior: printf
  83 > [  0.000000] (0:maestro@) Behavior: printf
  84 > [  0.000000] (0:maestro@) Behavior: printf
  85 > [  0.000000] (0:maestro@) Behavior: printf
  86 > [  0.000000] (0:maestro@) Behavior: printf
  87 > [  0.000000] (0:maestro@) Behavior: printf
  88 > [  0.000000] (0:maestro@) Behavior: printf
  89 > [  0.000000] (0:maestro@) Behavior: printf
  90 > [  0.000000] (0:maestro@) Behavior: printf
  91 > [  0.000000] (0:maestro@) Behavior: printf
  92 > [  0.000000] (0:maestro@) Behavior: printf
  93 > [  0.000000] (0:maestro@) Behavior: printf
  94 > [  0.000000] (0:maestro@) Behavior: printf
  95 > [  0.000000] (0:maestro@) Behavior: printf
  96 > [  0.000000] (0:maestro@) Behavior: printf
  97 > [  0.000000] (0:maestro@) Behavior: printf
  98 > [  0.000000] (0:maestro@) Behavior: printf
  99 > [  0.000000] (0:maestro@) Behavior: printf
 100 > [  0.000000] (1:app@Fafard) Error reached
 101 > [  0.000000] (0:maestro@) Behavior: printf
 102 > [  0.000000] (0:maestro@) Behavior: printf
 103 > [  0.000000] (0:maestro@) Behavior: printf
 104 > [  0.000000] (0:maestro@) Behavior: printf
 105 > [  0.000000] (0:maestro@) Behavior: printf
 106 > [  0.000000] (0:maestro@) Behavior: printf
 107 > [  0.000000] (0:maestro@) Behavior: printf
 108 > [  0.000000] (0:maestro@) Behavior: printf
 109 > [  0.000000] (0:maestro@) Behavior: printf
 110 > [  0.000000] (0:maestro@) Behavior: printf
 111 > [  0.000000] (0:maestro@) Behavior: printf
 112 > [  0.000000] (0:maestro@) Behavior: printf
 113 > [  0.000000] (0:maestro@) Behavior: printf
 114 > [  0.000000] (0:maestro@) DFS exploration ended. 43 unique states visited; 36 backtracks (108 transition replays, 30 states visited overall)
 115
 116 ! expect return 6
 117 # because SIMGRID_MC_EXIT_PROGRAM_CRASH = 6
 118 $ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/random-bug segv ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%a@%h)%e%m%n" --log=xbt_cfg.thresh:warning --log=no_loc
 119 > [  0.000000] (0:maestro@) Behavior: segv
 120 > [  0.000000] (0:maestro@) Start a DFS exploration. Reduction is: dpor.
 121 > [  0.000000] (0:maestro@) Behavior: segv
 122 > [  0.000000] (0:maestro@) Behavior: segv
 123 > [  0.000000] (0:maestro@) Behavior: segv
 124 > [  0.000000] (0:maestro@) Behavior: segv
 125 > [  0.000000] (0:maestro@) Behavior: segv
 126 > [  0.000000] (0:maestro@) Behavior: segv
 127 > [  0.000000] (0:maestro@) Behavior: segv
 128 > [  0.000000] (0:maestro@) Behavior: segv
 129 > [  0.000000] (0:maestro@) Behavior: segv
 130 > [  0.000000] (0:maestro@) Behavior: segv
 131 > [  0.000000] (0:maestro@) Behavior: segv
 132 > [  0.000000] (0:maestro@) Behavior: segv
 133 > [  0.000000] (0:maestro@) Behavior: segv
 134 > [  0.000000] (0:maestro@) Behavior: segv
 135 > [  0.000000] (0:maestro@) Behavior: segv
 136 > [  0.000000] (0:maestro@) Behavior: segv
 137 > [  0.000000] (0:maestro@) Behavior: segv
 138 > [  0.000000] (0:maestro@) Behavior: segv
 139 > [  0.000000] (0:maestro@) Behavior: segv
 140 > [  0.000000] (0:maestro@) Behavior: segv
 141 > [  0.000000] (0:maestro@) Behavior: segv
 142 > [  0.000000] (0:maestro@) Behavior: segv
 143 > Segmentation fault.
 144 > [  0.000000] (0:maestro@) **************************
 145 > [  0.000000] (0:maestro@) ** CRASH IN THE PROGRAM **
 146 > [  0.000000] (0:maestro@) **************************
 147 > [  0.000000] (0:maestro@) From signal: Segmentation fault
 148 > [  0.000000] (0:maestro@) Counter-example execution trace:
 149 > [  0.000000] (0:maestro@)   1: Random([0;5] ~> 3)
 150 > [  0.000000] (0:maestro@)   1: Random([0;5] ~> 4)
 151 > [  0.000000] (0:maestro@) You can debug the problem (and see the whole details) by rerunning out of simgrid-mc with --cfg=model-check/replay:'1/3;1/4'
 152 > [  0.000000] (0:maestro@) DFS exploration ended. 27 unique states visited; 22 backtracks (68 transition replays, 19 states visited overall)
 153 > [  0.000000] (0:maestro@) Stack trace not displayed because you passed --log=no_loc