From d71789667050c2d46885f8fa037bd2395097215a Mon Sep 17 00:00:00 2001
From: Miki Tanaka <miki.tanaka@nicta.com.au>
Date: Wed, 20 Jul 2016 16:37:42 +1000
Subject: [PATCH] arm-hyp test: regression for ARM_HYP

* add SpecCheck test, also add ASpec and ExecSpec tests for ARM arch
  (the error messages that ARMxxx tests give are not prefixed with "ARM")
* export L4V_ARCH=ARM_HYP in run_tests
---
 run_tests      | 6 +++++-
 spec/tests.xml | 2 ++
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/run_tests b/run_tests
index 543d50f6f..98ea83ad8 100755
--- a/run_tests
+++ b/run_tests
@@ -16,7 +16,11 @@ 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}:"
+
 # Run the tests from the script directory.
 cd ${DIR}
-python ./misc/regression/run_tests.py "$@"
+python ./misc/regression/run_tests.py -x AInvs -x BaseRefine -x Refine -x AutoCorresSEL4 -x CamkesAdlSpec -x CamkesGlueSpec -x SimpleSystem -x RelyGuarantee -x SepTactics -x SepTacticsExamples ASpec ExecSpec ASpec_ARM ExecSpec_ARM AInvs BaseRefine Refine SpecCheck -x Access -x InfoFlow -x ArmConfidentiality -x WholeSys -x WholeSysExamples -x DSpec -x DBaseRefine -x DRefine -x DPolicy -x CamkesCdlRefine -x SepDSpec -x DSpecProofs -x TakeGrant -x ASepSpec -x Bisim -x SysInit -x SysInitExamples -x InfoFlowC -x WholeSysExamplesC -x SimplExportAndRefine -x CParserTest -x CParserTools -x AutoCorres -x CamkesGlueProofs -x CamkesDarpaReport -x AutoCorresDoc -x AutoCorresTest -x CParser -x CKernel -x CSpec -x CBaseRefine -x CRefine "$@"
 
diff --git a/spec/tests.xml b/spec/tests.xml
index 869e67fe5..3d6054ca6 100644
--- a/spec/tests.xml
+++ b/spec/tests.xml
@@ -28,6 +28,8 @@
         <!-- Various seL4 specifications. -->
         <test name="ASpec" depends="haskell-translator">make ASpec</test>
         <test name="ExecSpec" depends="haskell-translator">make ExecSpec</test>
+        <test name="ASpec_ARM">L4V_ARCH=ARM make ASpec</test>
+        <test name="ExecSpec_ARM">L4V_ARCH=ARM make ExecSpec</test>
         <test name="DSpec">make DSpec</test>
         <test name="TakeGrant">make TakeGrant</test>
         <test name="ASepSpec" depends="ASpec">make ASepSpec</test>