lh-l4v/run_tests

#!/bin/bash
#
#
# Copyright 2014, NICTA
#
# This software may be distributed and modified according to the terms of
# the BSD 2-Clause license. Note that NO WARRANTY is provided.
# See "LICENSE_BSD2.txt" for details.
#
# @TAG(NICTA_BSD)
#

# Fetch directory this script is stored in.
DIR="$(cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd)"

# Add repo version of Isabelle to our path.
export PATH="${DIR}/isabelle/bin:$PATH"

# Export L4V_ARCH variable as ARM_HYP
export L4V_ARCH="${L4V_ARCH:-ARM_HYP}"
echo "Testing for L4V_ARCH=${L4V_ARCH}:"

# Enable quick_and_dirty mode for various images
if [ -n "${QUICK_AND_DIRTY}" ]
   then
       export INVS_QUICK_AND_DIRTY=1
       export REFINE_QUICK_AND_DIRTY=1
       export CREFINE_QUICK_AND_DIRTY=1
       echo "Testing with QUICK_AND_DIRTY"
fi

# Enable skip_proofs mode for various images

if [ -n "${REFINE_PROOFS}" ]
then
    export SKIP_REFINE_PROOFS=1
    export SKIP_INVS_PROOFS=1
    echo "Testing with SKIP_PROOFS"
fi

# Run the tests from the script directory.
cd ${DIR}

# Default exclusions for ARM_HYP

declare -A EXCLUDE

EXCLUDE[ARM_HYP]="
-r CamkesAdlSpec \
-r CamkesGlueSpec \
-r SimpleSystem \
-r RelyGuarantee \
-r Sep_Algebra \
-r tests-xml-correct \
-r SepTactics \
-r SepTacticsExamples \
-r DBaseRefine \
-r DRefine \
-r Access \
-r InfoFlow \
-r ArmConfidentiality \
-r DPolicy \
-r CamkesCdlRefine \
-r Bisim \
-r DSpec \
-r SepDSpec \
-r DSpecProofs \
-r TakeGrant \
-r ASepSpec \
-r HaskellKernel \
-r SysInit \
-r SysInitExamples \
-r InfoFlowCBase \
-r InfoFlowC \
-r SimplExportAndRefine \
-r CParserTest \
-r CParserTestX64 \
-r CParserTools \
-r AutoCorres \
-r CamkesGlueProofs \
-r CamkesDarpaReport \
-r theory_imports \
-r AutoCorresDoc \
-r AutoCorresTest \
-r AutoCorresSEL4 \
"

python ./misc/regression/run_tests.py ${EXCLUDE[${L4V_ARCH}]} $@