[klee-dev] [klee] [zesti] ZESTI Coreutils Experiments

[Anton Vasilyev]

Hello,

I'm interesting in integration KLEE with version control (e.g. git). It
seems to be similar with project ZESTI.
But due to lack of ZESTI documentation it requires source investigation
before using.


First I tried to reproduce ZESTI Coreutils Experiment and faced with
several mistypes in bash script "run-test.sh" published at
http://srg.doc.ic.ac.uk/projects/zesti/coreutils.html

---------
#!/bin/bash

-if [ "X$1" == X ]; then
+if [ "X$1" == "X" ]; then
  echo "Usage: $0 <executable> [test folder] [tests]"
else
-  if [ "X$2" == X ]; then
+  if [ "X$2" == "X" ]; then
    TDIR=$1
  else
    TDIR=$2
  fi
fi

cd src

-for f in \*.bc; do
+for f in *.bc; do
  fsimple=${f%.*}
  rm -f $fsimple

-  if [ -x /bin/$fsimple ]; then
+  if [ -x "/bin/$fsimple" ]; then
    ln -s /bin/$fsimple
-  elif [ -x /usr/bin/$fsimple ]; then
+  elif [ -x "/usr/bin/$fsimple" ]; then
    ln -s /usr/bin/$fsimple
  fi
done

rm -f $1

cd ..
sed "s/TEMPLATE-EXE/$1/g" zesti.tmpl > src/$1
chmod 755 src/$1

if [ "X$3" == "X" ]; then
  make check -C tests/$TDIR/
else
  make check -C tests/$TDIR/ "TESTS=$3"
fi
---------


I have several questions:

1. Whether it is necessary to replace compiled coreutils-6.11/src with
links to installed on system?
2. Is it correct that we need to mark patch by functions
"klee_patch_begin()" and "klee_patch_end()" for processing by ZESTI ?



-- 
With best regards,
Anton Vasilyev
-------------- next part --------------
HTML attachment scrubbed and removed