From 3d978d7df38fc501ada91db1498d6cf16be6f56c Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Thu, 16 Feb 2023 17:38:30 +1030 Subject: [PATCH] rt crefine: switch on quick_and_dirty for RISCV64 CRefine Allow sorries during development. Signed-off-by: Michael McInerney --- proof/Makefile | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/proof/Makefile b/proof/Makefile index ffa463db9e..959c0b056e 100644 --- a/proof/Makefile +++ b/proof/Makefile @@ -15,6 +15,11 @@ ifeq "$(L4V_ARCH)" "AARCH64" export REFINE_QUICK_AND_DIRTY=1 endif +# Allow sorry command in RISCV64 CRefine during development: +ifeq "$(L4V_ARCH)" "RISCV64" + export CREFINE_QUICK_AND_DIRTY=1 +endif + # # Setup heaps. #