netkat-verify/_oasis at master · mpmilano/netkat-verify · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
OASISFormat: 0.3
Name:        verify
Version:     0.9
Synopsis:    The frenetic Verification suite
Authors:     Nate Foster, Matthew Milano
License:     LGPL
Plugins:     META (0.3), StdFiles (0.3), DevFiles (0.3)
BuildTools:
  ocamlbuild,
  ocamldoc

XStdFilesREADME: False
XStdFilesAUTHORS: False

Library verify_lib
  Path: lib
  BuildDepends:
    lwt,
    lwt.unix,
    cstruct,
    dprle,
    lwt.syntax,
    lwt.syntax.log,
    str,
    ocamlgraph,
    packet,
    openflow,
    topology,
    threads,
    netcore
  InternalModules:
    NetKAT_Sat,
    NetKAT_Verify_Tools,
    NetKAT_Dehop_Graph
  Modules:
    NetKAT_Verify_Equivalence,
    NetKAT_Verify_Reachability

Library quickcheck
  Findlibparent: verify_lib
  Findlibname: quickcheck
  Path: quickcheck
  BuildDepends:
    quickcheck,
    netcore,
    verify_lib
  Modules:
    Verify_Dummy

Executable testtool
  Path: test
  MainIs: Test.ml
  BuildDepends:
    oUnit,packet,
    netcore,
    verify_lib,
    pa_ounit,
    pa_ounit.syntax,
    quickcheck,
    verify_lib.quickcheck
  Install: False

Test all_tests
  Command: $testtool inline-test-runner dummy
  Run$: flag(tests)
  TestTools: testtool

Executable verify
  Path: verify
  MainIs: Verify.ml
  Install$: flag(installexec)
  BuildDepends:
    lwt,
    lwt.syntax,
    netcore,
    verify_lib