#!/usr/bin/sh

  f=$1
  bn=$2

  cf_expect=""
  if [ $model = tso ] ; then
    if [ $expect_tso = FAILED ] ; then
      cf_expect=fail
    else
      cf_expect=pass
    fi
  elif [ $model = sc ] ; then
    cf_expect=pass
  fi
  if [ -z "$cf_expect" ] ; then
    return
  fi

  cat $bn.c | grep -v '__CPROVER_ASYNC' > $bn.checkfence.c
  sed -i '1i\
#include "lsl_protos.h" \
#define __CPROVER_assume(x) lsl_assume(x) \
#define __CPROVER_assert(x, t) lsl_assert(x) \
#define fence lsl_fence("load-load") \
#define lwfence lsl_fence("store-store")' $bn.checkfence.c
  threads="`grep __CPROVER_ASYNC_ $bn.c | cut -f2 -d: | sed 's/(.*//'`"
  LD_LIBRARY_PATH=$path/new-tools/ C2LSL_HOME=$path/new-tools/ \
    $path/new-tools/c2lsl -I $path/new-tools/ $bn.checkfence.c ${bn}_$model.lsl
  echo "test $bn [memmodel=$model, expect=$cf_expect]" >> ${bn}_$model.lsl
  for t in $threads ; do
    cat >> ${bn}_$model.lsl <<EOF
  thread $t {
    _ = $t(0)
  }
EOF
  done
  cat >> ${bn}_$model.lsl <<"EOF"
  thread t {
    _ = main()
  }
end
EOF

  echo -n "<br>Checkfence: " >> ${f}_notes
  $path/cpbm-0.4/cpbm run --claim ALL_CLAIMS $expected_cpbm \
    --timeout $timeout --cmd $path/new-tools/checkfence ${bn}_$model.lsl -- > \
    $path/results.checkfence/$arch/$prefix/$f.vr
  logf=`grep ^LOGFILE $path/results.checkfence/$arch/$prefix/$f.vr | cut -f2 -d:`
  grep "RESULT:" $logf | sed 's/.*" //' | sed 's/\..*//' >> ${f}_notes
  grep 'User time' $logf | cut -f2 -d: | sed 's/$/sec/' >> ${f}_notes

