_oasis

OASISFormat: 0.4
Name:        llvm2smt
Version:     0.1
Synopsis:    Transform llvm control flow graph into smt formulas
Authors:     Gabriel Radanne <drupyog@zoho.com>
License:     MIT
Plugins:     META (0.3), DevFiles (0.3)

BuildTools: ocamlbuild


Library llvm2smt
  Path: src
  InternalModules: Utils
  Modules:
    Llvm2smt, Llvmcfg, Smtgraph
  BuildDepends: llvm, z3overlay, ocamlgraph, llvmgraph


AlphaFeatures: ocamlbuild_more_args
Document "api"
  Title: API reference for Llvm_nts
  Type: ocamlbuild (0.3)
  Install: false
  BuildTools: ocamldoc
  XOCamlbuildPath: ./
  XOCamlbuildLibraries: llvm2smt
  XOCamlbuildExtraArgs: "-docflags '-colorize-code, -short-functors, -charset, utf-8'"


Executable read_and_dot
  Path: tests
  Build$: flag(tests)
  Install: false
  MainIs: read_and_dot.ml
  BuildDepends: llvm2smt, llvm.bitreader, llvm.scalar_opts
  CompiledObject: best

Test example_dot
  Command:
    clang -c -emit-llvm -o example.bc ../tests/example.c
    $read_and_dot example.bc example.dot example.break.dot example.smt.dot
  TestTools: read_and_dot
  WorkingDirectory: _build

Test nested_loop_dot
  Command:
    clang -c -emit-llvm -o nested_loop.bc ../tests/nested_loop.c
    $read_and_dot nested_loop.bc nested_loop.dot nested_loop.break.dot nested_loop.smt.dot
  TestTools: read_and_dot
  WorkingDirectory: _build