run_tests: move selection of RefineOrphanage to run_tests

This is more consistent with how we handle other broken proof sessions
in the run_tests framework.
This commit is contained in:
Japheth Lim 2018-10-03 10:28:38 +10:00
parent 18e0d934cc
commit 1a504d1f6c
2 changed files with 6 additions and 2 deletions

View File

@ -55,7 +55,7 @@ session Refine = BaseRefine +
*)
session RefineOrphanage = Refine +
description {* Proof that the kernel does not orphan threads. *}
theories [condition = "L4V_ARCH_IS_ARM"]
theories
"refine/$L4V_ARCH/Orphanage"
session BaseRefine2 = BaseRefine +

View File

@ -59,6 +59,7 @@ EXCLUDE["ARM_HYP"]=[
"Access",
"Bisim",
"DRefine",
"RefineOrphanage",
"SimplExportAndRefine"]
EXCLUDE["ARM"]=[]
@ -71,9 +72,11 @@ EXCLUDE["X64"]=[
"CamkesGlueProofs",
"DBaseRefine",
"DSpec",
"RefineOrphanage",
"SepTacticsExamples",
"SimplExportAndRefine",
"AsmRefine"]
"AsmRefine"
]
EXCLUDE["RISCV64"]=[
"AInvs",
@ -84,6 +87,7 @@ EXCLUDE["RISCV64"]=[
"CSpec",
"CamkesDarpaReport",
"CamkesGlueProofs",
"RefineOrphanage",
"AsmRefine"
]