examples/msg/mc/bugged1_liveness_stack_cleaner

   1 #!/bin/sh
   2 # Run the same test compiled with -fstack-cleaner / f-no-stack-cleaner
   3 # and compare the output.
   4
   5 srcdir="$1"
   6 bindir="$2"
   7
   8 cd "$srcdir"
   9
  10 die() {
  11   echo "$@" >&2
  12   exit 1
  13 }
  14
  15 assert() {
  16   if ! eval "$1"; then
  17     die "Assertion failed: $@"
  18   fi
  19 }
  20
  21 # If we don't have timeout, fake it:
  22 if ! which timeout > /dev/null; then
  23   timeout() {
  24     shift
  25     "$@"
  26   }
  27 fi
  28
  29 run() {
  30   state=$1
  31   shift
  32   timeout 30s ${bindir:=.}/bugged1_liveness_cleaner_$state \
  33     ${srcdir:=.}/../../platforms/platform.xml \
  34     ${srcdir:=.}/deploy_bugged1_liveness.xml \
  35     --cfg=model-check:1 "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" \
  36     --cfg=contexts/factory:ucontext \
  37     --cfg=contexts/stack_size:256
  38   assert 'test $? = 134'
  39 }
  40
  41 get_states() {
  42   echo "$1" | grep "Expanded pairs = " | sed "s/^.*Expanded pairs = //" | head -n1
  43 }
  44
  45 RES_ON="$(run on 2>&1 1>/dev/null)"
  46 RES_OFF="$(run off 2>&1 1>/dev/null)"
  47
  48 STATES_ON=$(get_states "$RES_ON")
  49 STATES_OFF=$(get_states "$RES_OFF")
  50
  51 # Both runs finished:
  52 assert 'test -n "$STATES_ON"'
  53 assert 'test -n "$STATES_OFF"'
  54
  55 # We expect 21 visited pairs with the stack cleaner:
  56 assert 'test "$STATES_ON" = 21'
  57
  58 # We expect more states without the stack cleaner:
  59 assert 'test "$STATES_ON" -lt "$STATES_OFF"'