Thanks, Vadim!<br>I have successfully used run LDV-Tools in Docker images and get results in my browser.<br>But I have some confusion in results. <br>1. What BCE, DEG, DSCV, RI and RCV stand for? Verifiers or checkers?<br>2. Can LDV-Tools find null-pointer dereferences and memory leaks in device drivers?<br><br><blockquote name="replyContent" style="padding-left:5px;margin-left:5px;border-left:#b6b6b6 2px solid;margin-right:0">Hi Jia-Ju!<br><div class="moz-cite-prefix">
      <br>
      If you want just to run LDV-Tools then the best way is to use
      Docker images see our <strong><a target="_blank" href="http://forge.ispras.ru/projects/ldv/wiki/LDV_Tools_in_Docker">LDV

          Tools in Docker instructions</a>.<br>
      </strong><br>
      If you want to compile LDV-Tools yourself you need to install
      correct versions of dependences, see INSTALL file.<br>
      It looks like you are using newer version of ocaml. If you still
      want to use it please patch the sources:<br>
      <br>
      1. for ocaml 4.01<br>
      1.1 dscv/rcv/backends/blast - goto the submodule and apply the
      patch blast-Fix-hashtable-interface.patch<br>
      1.2 dscv/rcv/cil -  goto the submodule and apply the patch
      cil-ocaml.patch<br>
      <br>
      You may also have the newer version of gcc:<br>
      2. for gcc 4.8.2<br>
      2.1 ri/cif/aspectator - goto the submodule and apply the patch
      aspectator-gcc.patch<br>
      <br>
      Best,<br>
      Vadim<br>
      <br>
</div>
    
  

</blockquote><br><br><br>