[ldv-project] An error of batHashtbl.ml when compiling LDV tools

[白家驹]

Thanks, Vadim!
I have successfully used run LDV-Tools in Docker images and get results in my browser.
But I have some confusion in results.
1. What BCE, DEG, DSCV, RI and RCV stand for? Verifiers or checkers?
2. Can LDV-Tools find null-pointer dereferences and memory leaks in device drivers?

Hi Jia-Ju!


If you want just to run LDV-Tools then the best way is to use Docker images see our LDV Tools in Docker instructions.

If you want to compile LDV-Tools yourself you need to install correct versions of dependences, see INSTALL file.
It looks like you are using newer version of ocaml. If you still want to use it please patch the sources:

1. for ocaml 4.01
1.1 dscv/rcv/backends/blast - goto the submodule and apply the patch blast-Fix-hashtable-interface.patch
1.2 dscv/rcv/cil -  goto the submodule and apply the patch cil-ocaml.patch

You may also have the newer version of gcc:
2. for gcc 4.8.2
2.1 ri/cif/aspectator - goto the submodule and apply the patch aspectator-gcc.patch

Best,
Vadim




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://linuxtesting.org/pipermail/ldv-project/attachments/20150610/84565152/attachment.html>