ticketlock-testwait/lock_progress_4_bits_per_byte.log

   1 make[1]: Entering directory `/home/compudj/doc/userspace-rcu/ticketlock-testwait'
   2 rm -f pan* trail.out .input.spin* *.spin.trail .input.define
   3 touch .input.define
   4 cat .input.define > pan.ltl
   5 cat DEFINES >> pan.ltl
   6 spin -f "!(`cat lock_progress.ltl | grep -v ^//`)" >> pan.ltl
   7 cp config_4_bits_per_byte.define .input.define
   8 cat DEFINES > .input.spin
   9 cat .input.define >> .input.spin
  10 cat mem.spin >> .input.spin
  11 rm -f .input.spin.trail
  12 spin -a -X -N pan.ltl .input.spin
  13 spin: line  73 "pan.___", Error: undeclared variable: do_pause  saw ''(' = '40''
  14 spin: line  73 "pan.___", Error: syntax error   saw ''(' = '40''
  15 spin: line  99 "pan.___", Error: bad call to proc_is_safe
  16 spin: line  99 "pan.___", Error: bad call to proc_is_safe
  17 spin: line  99 "pan.___", Error: bad call to proc_is_safe
  18 spin: line  99 "pan.___", Error: bad call to proc_is_safe
  19 spin: line  99 "pan.___", Error: bad call to proc_is_safe
  20 spin: line  81 "pan.___", Error: proctype proc_X not found
  21 spin: 1 error(s) - aborting
  22 make[1]: Leaving directory `/home/compudj/doc/userspace-rcu/ticketlock-testwait'