diff options
| author | Son Ho | 2023-12-22 19:09:16 +0100 |
|---|---|---|
| committer | Son Ho | 2023-12-22 19:09:16 +0100 |
| commit | 3688596f27a1ba461f48e88446b8812ec73f1a2f (patch) | |
| tree | 54c620f0370e20cdcdcf4b8e889a2f306addb429 /Makefile | |
| parent | 632e2ddc0c5ed0c785b37fdc41394336e467f623 (diff) | |
Add an option to split the fwd/back functions and fix a minor issue
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 19 |
1 files changed, 17 insertions, 2 deletions
@@ -256,14 +256,29 @@ testp-%: gen-llbcp-% tfstarp-% tcoqp-% tleanp-% thol4p-% .PHONY: tfstar-% tfstar-%: OPTIONS += -backend fstar tfstar-%: BACKEND_SUBDIR := fstar -tfstar-%: +tfstar-%: tsplit-fstar-% $(AENEAS_CMD) # "p" stands for "Polonius" .PHONY: tfstarp-% tfstarp-%: OPTIONS += -backend fstar tfstarp-%: BACKEND_SUBDIR := fstar -tfstarp-%: +tfstarp-%: tsplit-fstarp-% + $(AENEAS_CMD) + +# Test where we split the forward/backward functions +.PHONY: tsplit-fstar-% +tsplit-fstar-%: OPTIONS += -backend fstar -split-fwd-back +tsplit-fstar-%: BACKEND_SUBDIR := fstar-split +tsplit-fstar-%: + $(AENEAS_CMD) + +# Test where we split the forward/backward functions +# "p" stands for "Polonius" +.PHONY: tsplit-fstarp-% +tsplit-fstarp-%: OPTIONS += -backend fstar -split-fwd-back +tsplit-fstarp-%: BACKEND_SUBDIR := fstar-split +tsplit-fstarp-%: $(AENEAS_CMD) .PHONY: tcoq-% |