Add makefile for model checking

Usage 1) Verify islet using model checking (in plat/fvp) $ make verify Usage 2) Remove generated output (in plat/fvp) $ make clean
islet-project · Nov 7, 2023 · a8731b0 · a8731b0
1 parent ae3e6b8
commit a8731b0
Showing 1 changed file with 12 additions and 0 deletions.
diff --git a/plat/fvp/Makefile b/plat/fvp/Makefile
@@ -0,0 +1,12 @@
+KANI_FLAGS := \
+	--enable-unstable \
+	--ignore-global-asm \
+	--restrict-vtable
+
+.PHONY: verify
+verify:
+	cargo kani $(KANI_FLAGS)
+
+.PHONY: clean
+clean:
+	cargo clean