prove-all

#!/bin/sh

if [ ! -z "$PVS_DIR" ]; then
    provethem="$PVS_DIR/provethem"
else
    provethem=`which provethem`
    if [ ! $provethem  ]; then
	printf "The script 'provethem' could not be located. Either define \$PVS_DIR to point to the PVS directory or add the PVS directory to the environment variable \$PATH.\n"
	exit 1;
    fi
fi

readVersion() {
    if ! type "$provethem" > /dev/null 2>&1  || ! VERSION=$($provethem --version) ; then
	printf "The script 'provethem' could not be located. Either define \$PVS_DIR to point to the PVS directory or add the PVS directory to the environment variable \$PATH.\n"
	exit 1;
    fi
}

usage() {
    echo "NAME
  prove-all $VERSION -- runs proveit on all the libraries in the NASALib

SYNOPSIS

  prove-all <options>

DESCRIPTION
  This script wraps provethem to provide a specific kind of run. By default, it removes 
  .pvscontext and the binary files from the pvsbin folder in each library directory, replaces 
  the pvs library path by the current directory, and runs proveit as indicated by the 
  nasalib.all file.

  To supersede this particular configuration, the same options accepted by provethem can
  be used on this script.

  The list of libraries to be processed is read from the file 'all-libraries' if there is no
  'nasalib.all' file in the current folder.

SEE ALSO
  provethem -- for iterating proveit on a list of directories
"
}

for opt in "$@"
do
    if [ $opt = "--help" -o $opt = "-help" -o $opt = "-h" ]; then
	usage
	exit 0
    fi
done

all_libraries_file="nasalib.all"
if [ ! -f $all_libraries_file ]; then 
    all_libraries_file="all-libraries";
    if [ ! -f $all_libraries_file ]; then 
	all_libraries_file="all-theories";
	if [ -f $all_libraries_file ]; then
	    echo "Warning: all-theories is no longer supported as default input file name, please rename it to all-libraries."
	else
	    echo "Error: input file not found.";
	    exit 1;
	fi;
    fi
fi

if [ "$provethem" ]; then
    $provethem --clean-only --action-name="Cleaning" "$@" $ADDITIONALARGS $all_libraries_file
    $provethem --clearpath --addpath --force "$@" $all_libraries_file
fi