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

refine: add intermediate BaseRefine2 session for small machines

This commit is contained in:
Gerwin Klein 2017-03-25 13:00:56 +01:00 committed by Alejandro Gomez-Londono
parent 96958113ef
commit 682dde4155
2 changed files with 10 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
proof/Makefile
View File

@ -23,7 +23,7 @@ report-regression:
#
# Refine heaps.
HEAPS += AInvs BaseRefine Refine
HEAPS += AInvs BaseRefine BaseRefine2 Refine
# CRefine heaps.
HEAPS += CKernel CSpec CBaseRefine CRefine

9
proof/ROOT
View File

@ -37,6 +37,15 @@ session Refine = BaseRefine +
theories
"refine/$L4V_ARCH/Refine"
session BaseRefine2 = BaseRefine +
description {* Intermediate point in refinement proof. Useful for machines with small RAM. *}
theories [condition = "SKIP_INVS_PROOFS", quick_and_dirty, skip_proofs]
"refine/$L4V_ARCH/Untyped_R"
"refine/$L4V_ARCH/Schedule_R"
theories
"refine/$L4V_ARCH/Untyped_R"
"refine/$L4V_ARCH/Schedule_R"
session BaseRefine = AInvs +
description {* Background theory and libraries for refinement proof. *}
theories [condition = "SKIP_INVS_PROOFS", quick_and_dirty, skip_proofs]