Nico Huber has submitted this change and it was merged. ( https://review.coreboot.org/c/libhwbase/+/26850 )
Change subject: Makefile.proof: Add --no-inlining to SPARKFLAGS ......................................................................
Makefile.proof: Add --no-inlining to SPARKFLAGS
With `--no-inlining`, proof is about 10% faster for libgfxinit.
Change-Id: Ia6055da326901c1c25b9d0c757767891284bc515 Signed-off-by: Nico Huber nico.huber@secunet.com Reviewed-on: https://review.coreboot.org/c/libhwbase/+/26850 Tested-by: Nico Huber nico.h@gmx.de Reviewed-by: Reto Buerki reet@codelabs.ch --- M Makefile.proof 1 file changed, 1 insertion(+), 0 deletions(-)
Approvals: Nico Huber: Verified Reto Buerki: Looks good to me, approved
diff --git a/Makefile.proof b/Makefile.proof index 6c16a40..729ecab 100644 --- a/Makefile.proof +++ b/Makefile.proof @@ -11,6 +11,7 @@ SPARKFLAGS += --mode=$(PROOF_MODE) SPARKFLAGS += --report=fail SPARKFLAGS += --warnings=error +SPARKFLAGS += --no-inlining SPARKFLAGS += --prover=z3 --steps=500 --timeout=1 # FIXME: timeout used because steps seems broken
quote-list = $(subst $(space),$(comma),$(patsubst %,"%",$(1)))