adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

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
This commit is contained in:
Miki Tanaka 2016-07-20 16:37:42 +10:00 committed by Alejandro Gomez-Londono
parent 61dffdb6cc
commit d717896670
2 changed files with 7 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
run_tests
View File

@ -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 "$@"

2
spec/tests.xml
View File

@ -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>