/dyn_instr

Primary LanguageOCaml

dyn_instr

  • Install opam: https://opam.ocaml.org/doc/Install.html
  • Install OCaml 4.05.0: 
    opam switch create 4.05.0
  • Install Dune, CIL and other dependencies: 
    opam install dune cil num csv ocamlbuild ocamlfind menhir
  • If you want to use ocaml-lsp-server with an IDE such as Visual Studio Code or Emacs, you need to install OCaml >= 4.06.0 and compile and install CIL from https://github.com/letonchanh/cil.
  • vtrace instrumentation: 
    dune exec -- src/instr.exe -dig input.c [-nopre] [-nonla]
    The instrumentation result is the file input_instr.c in the same folder as input.c.
  • Validation instrumentation: 
    dune exec -- src/instr.exe -val input.c -inv inv.csv [-pre cond] [-case label]
    The instrumentation result is the file input_validate.c in the same folder as input.c. Note that input.c must be the same source file in the vtrace instrumentation.