#!/bin/bash
if [ -f $1.out ]; then
  echo "Warning, output file $1.out already exists, this analysis might be already running... exit."
  exit 1
fi
rm -f $1.true* $1.false* $1.fail*
TStart=`dateutils.dconv now`
./proverif $1 | grep -v "RESULT (but" > $1.out
TEnd=`dateutils.dconv now`
echo "TOTAL TIME : " `dateutils.ddiff $TStart $TEnd -f '%dd %Hh %Mm %Ss'` >> $1.out
Ext=`grep RESULT $1.out | sed "s/.*is //; s/.*cannot be proved/failed/; s/\..*$//"`
Ext=`echo $Ext | tr ' ' '.' | tr '\n' '.' | sed "s/\.$//"`
if [ "$Ext" = "" ]; then Ext="empty"; fi
mv $1.out `echo $1 | sed "s/expanded/result/; s/\.pv$//"`.$Ext