Failure when creating harness in scripts/cpa_witness2test.py
This issue was discovered when I tried to reproduce #339 (closed).
I closed that issue and open this one because otherwise the issue title is misleading.
Command to reproduce:
scripts/cpa_witness2test.py -preprocess -witness2test -setprop analysis.summaryEdges=true -witness output/Counterexample.1.graphml.gz -spec test/programs/benchmarks/properties/unreach-call.prp alloc.c
Output:
INFO: /home/stephen/work/workspace/CPAchecker/scripts/cpa.sh -preprocess -witness2test -setprop analysis.summaryEdges=true -witness output/Counterexample.1.graphml.gz -spec test/programs/benchmarks/properties/unreach-call.prp alloc.c -witness2test
Language C detected and set for analysis (CPAMain.detectFrontendLanguageIfNecessary, INFO)
CPAchecker 1.9.1-svn / witness2test (OpenJDK 64-Bit Server VM 11.0.7) started (CPAchecker.run, INFO)
Parsing CFA from file(s) "alloc.c" (CPAchecker.parse, INFO)
Error: Invalid configuration (Cannot parse witness: Neiter the SHA-1 hash value of given verification-task source-code file (5a6da3bf79aa6ccfafdb25d5aa91a2d7c9b859f3) nor the corresponding SHA-256 hash value (53afd66c7f7abf85c74b887f75392d71fe8c87234175355f463918742fb72a68) match the program hash value given in the witness. The witness is likely unrelated to the verification task.) (AutomatonGraphmlParser.checkHashSum, SEVERE)
INFO: Looking at output/Counterexample.1.harness.c
INFO: clang -D__alias__(x)= -m32 -std=gnu11 -o output/test_cex1 -include alloc.c output/Counterexample.1.harness.c
INFO: /tmp/Counterexample-3ff563.o: In function `main':
INFO: Counterexample.1.harness.c:(.text+0x2b): undefined reference to `foo'
INFO: Counterexample.1.harness.c:(.text+0x30): undefined reference to `bar'
INFO: Counterexample.1.harness.c:(.text+0x44): undefined reference to `__VERIFIER_error'
INFO: clang: error: linker command failed with exit code 1 (use -v to see invocation)
INFO:
INFO: clang -D__alias__(x)= -m32 -std=gnu90 -o output/test_cex1 -include alloc.c output/Counterexample.1.harness.c
INFO: /tmp/Counterexample-855f8b.o: In function `main':
INFO: Counterexample.1.harness.c:(.text+0x2b): undefined reference to `foo'
INFO: Counterexample.1.harness.c:(.text+0x30): undefined reference to `bar'
INFO: Counterexample.1.harness.c:(.text+0x44): undefined reference to `__VERIFIER_error'
INFO: clang: error: linker command failed with exit code 1 (use -v to see invocation)
INFO:
WARNING: Compilation failed for harness output/Counterexample.1.harness.c
ERROR: Compilation failed for every harness/file pair.
Verification result: ERROR.