search

gernst / legion-symcc

Fresh implementation of the Legion algorithm on top of SyMCC
Other
0 stars 1 forks source link

[TestComp-2022] Unimplemented function `__VERIFIER_nondet_unsigned_char` #16

Closed DonggeLiu closed 2 years ago

DonggeLiu commented 2 years ago

Legion-SymCC terminated on some benchmarking programs because of undefined reference to __VERIFIER_nondet_unsigned_char:

/usr/bin/ld: /tmp/mea8000-978a16.o: in function `main':
mea8000.c:(.text+0xac13): undefined reference to `__VERIFIER_nondet_unsigned_char'
clang: error: linker command failed with exit code 1 (use -v to see invocation)
clang -Xclang -load -Xclang ubuntu2004/lib/libSymbolize.so -m32 ../../sv-benchmarks/c/float-benchs/mea8000.c __VERIFIER.c -o ../../sv-benchmarks/c/float-benchs/mea8000 -lstdc++ -lm -lSymRuntime -Lubuntu2004/lib32 -Wl,-rpath,ubuntu2004/lib32

Sample program: float-benchs/mea8000.yml

gernst commented 2 years ago

sv-benchmarks/c/float-benchs/mea8000.c times out, check why