proof/ROOT: add CREFINE_QUICK_AND_DIRTY flag
Use to build CRefine in quick_and_dirty mode.
This commit is contained in:
parent
84f63763e0
commit
96c13859e0
|
@ -77,6 +77,8 @@ session CRefineSyscall = CBaseRefine +
|
||||||
"crefine/$L4V_ARCH/Syscall_C"
|
"crefine/$L4V_ARCH/Syscall_C"
|
||||||
|
|
||||||
session CRefine = CBaseRefine +
|
session CRefine = CBaseRefine +
|
||||||
|
theories [condition = "CREFINE_QUICK_AND_DIRTY", quick_and_dirty]
|
||||||
|
"crefine/$L4V_ARCH/Refine_C"
|
||||||
theories
|
theories
|
||||||
"crefine/$L4V_ARCH/Refine_C"
|
"crefine/$L4V_ARCH/Refine_C"
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue