verify: add goto-analyzer cross-analyzation step

if UNSATISFIABLE

GNUmakefile

@@ -96,12 +96,22 @@ verify/%.vfy: source/algos/%.c $(ALGOSINC) algocfg
 	b=`basename $@ .vfy`; ./algocfg $$b cbmc; args=`./algocfg $$b cbmc`; \
 	  echo $(TIMEOUT_4m) cbmc $$args $(CBMC_ARGS) $< > $@; \
 	  $(TIMEOUT_4m) cbmc $$args $(CBMC_ARGS) $< | tee -a $@
+	if grep UNSATISFIABLE $@ >/dev/null; then \
+	  echo | tee -a $@; b=`basename $@ .vfy`; \
+	  echo goto-analyzer --verify --recursive-interprocedural source/algos/$$b.c | tee -a $@; \
+	  goto-analyzer --verify --recursive-interprocedural source/algos/$$b.c | tee -a $@; \
+	fi
 CMBC_TRACE_ARGS = --trace --reachability-slice-fb
 verify/%.vfy-trace: source/algos/%.c $(ALGOSINC) algocfg
 	@$(MAKE) -s algocfg
 	b=`basename $@ .vfy-trace`; ./algocfg $$b cbmc; args=`./algocfg $$b cbmc`; \
 	  echo $(TIMEOUT_4m) cbmc $(CMBC_TRACE_ARGS) $$args $(CBMC_ARGS) $< > $@; \
 	  $(TIMEOUT_4m) cbmc $(CMBC_TRACE_ARGS) $$args $(CBMC_ARGS) $< | tee -a $@
+	if grep UNSATISFIABLE $@ >/dev/null; then \
+	  echo | tee -a $@; b=`basename $@ .vfy`; \
+	  echo goto-analyzer --verify --recursive-interprocedural source/algos/$$b.c | tee -a $@; \
+	  goto-analyzer --verify --recursive-interprocedural source/algos/$$b.c | tee -a $@; \
+	fi
 
 .PHONY: check clean all lint verify check-verify verify-trace fmt cppcheck clang-tidy fuzz
 check: all
@@ -158,6 +168,10 @@ verify/verify.log: $(ALGOSRC) algocfg
             (echo cbmc $$args $(CBMC_ARGS) "$$c FAILED"; \
 	    test $(( `./algocfg $$b VFY_FAIL` + `./algocfg $$b VFY_TIMEOUT` )) -gt 0 || exit 1); \
 	done | tee verify/verify.log
+	for b in `./algocfg UNSATISFIABLE` `./algocfg VFY_TIMEOUT`; do \
+	  echo goto-analyzer --verify --recursive-interprocedural source/algos/$$b.c; \
+	  goto-analyzer --verify --recursive-interprocedural source/algos/$$b.c; \
+	done | tee -a verify/verify.log
 check-verify:
 	for c in $(addsuffix .c, $(addprefix source/algos/,$(filter-out $(TIMEOUT_VERIFY),$(TESTS)))); \
 	do \