Skip to content

Commit

Permalink
Fix "result" target
Browse files Browse the repository at this point in the history
We were missing a rule to produce result.txt, rendering the "result"
infeasible.
  • Loading branch information
tautschnig committed Dec 11, 2023
1 parent ba019b2 commit eff62e7
Showing 1 changed file with 17 additions and 0 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -833,6 +833,23 @@ $(LOGDIR)/result.xml: $(HARNESS_GOTO).goto
--stderr-file $(LOGDIR)/result-err-log.txt \
--description "$(PROOF_UID): checking safety properties"

$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
$(LITANI) add-job \
$(POOL) \
--command \
'$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \
--inputs $^ \
--outputs $@ \
--ci-stage test \
--stdout-file $@ \
$(MEMORY_PROFILING) \
--ignore-returns 10 \
--timeout $(CBMC_TIMEOUT) \
--pipeline-name "$(PROOF_UID)" \
--tags "stats-group:safety checks" \
--stderr-file $(LOGDIR)/result-err-log.txt \
--description "$(PROOF_UID): checking safety properties"

$(LOGDIR)/property.xml: $(HARNESS_GOTO).goto
$(LITANI) add-job \
--command \
Expand Down

0 comments on commit eff62e7

Please sign in to comment.