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

proof/ROOT: RefineOrphanage: add quick and dirty option 

Piggybacking off of REFINE_QUICK_AND_DIRTY as they are usually linked.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski 2023-05-25 15:12:09 +10:00 committed by Gerwin Klein
parent 381ad05df9
commit 1e619439d2
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
1 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/ROOT
View File

@ -56,6 +56,8 @@ session Refine in "refine" = BaseRefine +
*)
session RefineOrphanage in "refine/$L4V_ARCH/orphanage" = Refine +
description \<open>Proof that the kernel does not orphan threads.\<close>
theories [condition = "REFINE_QUICK_AND_DIRTY", quick_and_dirty]
"Orphanage"
theories
"Orphanage"