Makefile

# Top-level Makefile for jsmn CBMC proofs
#
# Proofs are discovered automatically: any subdirectory of proofs/
# containing a Makefile is treated as a proof target.

# Discovery: find all proofs/*/Makefile, extract the directory name
PROOF_DIRS := $(wildcard proofs/*/Makefile)
PROOFS := $(patsubst proofs/%/Makefile,%,$(PROOF_DIRS))

.PHONY: all list help $(PROOFS)
# Default target
all: $(PROOFS)
	$(info )
	$(info === All proofs completed ===)
	@cd .

# Run AI verifier agent
.PHONY: ai
ai:
	@python3 tools/ai-agent/verify_agent.py all || (echo "Python or agent failed" && exit 1)

# List available proofs
list:
	$(foreach p,$(PROOFS),$(info $(p)))
	@cd .

# Run individual proof
$(PROOFS):
	$(info )
	$(info === Running proof: $@ ===)
	@$(MAKE) --no-print-directory -C proofs/$@

# Help target
help:
	$(info Usage:)
	$(info   make            - Run all proofs [default])
	$(info   make all        - Run all proofs)
	$(info   make list       - List all available proofs)
	$(info   make <proof>    - Run a specific proof by name)
	$(info   make help       - Show this help message)
	$(info )
	$(info Available proofs:)
	$(foreach p,$(PROOFS),$(info   $(p)))
	@cd .