Repository navigation
Expand file tree
/
Copy path_oasis
More file actions
113 lines (98 loc) · 3.95 KB
/
Copy path_oasis
File metadata and controls
113 lines (98 loc) · 3.95 KB
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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
OASISFormat: 0.4
Name: duet
Version: 0.1.3
Synopsis: Duet program analyzer
Authors: Zachary Kincaid
License: GPL-3.0
Plugins: META (0.4), StdFiles (0.4), DevFiles (0.4)
AlphaFeatures: ocamlbuild_more_args
BuildTools: ocamlbuild, ocamldoc, menhir
Library srk
Path: srk/src
FindlibName: srk
Pack: true
Modules: SrkUtil, Log, DisjointSet, Memo, FeatureTree, QQ, ZZ, Syntax, Interval, Smt, SrkZ3, Linear, Polynomial, Interpretation, SrkApron, Polyhedron, SrkSimplify, Abstract, Nonlinear, CoordinateSystem, Wedge, Quantifier, Iteration, Transition, BigO, WeightedGraph
BuildDepends: batteries, ppx_deriving, ppx_deriving.show, ppx_deriving.ord, gmp, camlidl, apron, Z3, ocrs, ntl, ocamlgraph
XMETADescription: Symbolic Reasoning Kit
Executable test_srk
Build$: flag(tests)
Path: srk/src
MainIs: test_srk.ml
BuildDepends: batteries, ppx_deriving, ppx_deriving.ord, gmp, camlidl, apron, apron.boxMPQ, apron.octMPQ, apron.polkaMPQ, Z3, oUnit, ocrs, ntl
CompiledObject: native
Install: false
Executable bigtop
Build$: flag(tests)
Path: srk/src
MainIs: bigtop.ml
BuildDepends: batteries, ppx_deriving, ppx_deriving.ord, gmp, camlidl, apron, apron.boxMPQ, apron.octMPQ, apron.polkaMPQ, Z3, ocrs, ntl
CompiledObject: native
Install: false
Library apak
Path: apak
FindlibName: apak
Pack: true
Modules: Dll, Enumeration, EvalLink, ExtGraph, Fixpoint,Ka, Lattice, Loop, Monoid, Pathexp, Persistent, RecGraph, Semilattice, Sese, Sig, Tagged, Putil
BuildDepends: batteries, ppx_deriving, ppx_deriving.show, ppx_deriving.ord, ocamlgraph, Z3, srk
Install: false
XMETADescription: Algebraic Program Analysis Kit
Executable test_apak
Build$: flag(tests)
Path: apak
MainIs: test_apak.ml
BuildDepends: batteries, ppx_deriving, ppx_deriving.show, ppx_deriving.ord, ocamlgraph, Z3, apron, apron.boxMPQ, apron.octMPQ, apron.polkaMPQ, srk, oUnit
CompiledObject: native
Install: false
Library pa
Path: pa
Pack: true
FindlibName: pa
InternalModules: PaSmt, PaFormula, Struct, PredicateAutomata
BuildDepends: batteries, ppx_deriving, ppx_deriving.show, ppx_deriving.ord, srk, Z3
Install: false
XMETADescription: Predicate Automata tools
Executable test_patools
Path: patools
MainIs: test_patools.ml
BuildDepends: batteries, ppx_deriving, ppx_deriving.show, ppx_deriving.ord, srk, Z3, apron, apron.boxMPQ, apron.octMPQ, apron.polkaMPQ, pa, oUnit
Install: false
CompiledObject: native
Executable patools
Path: patools
BuildDepends: batteries, ppx_deriving, ppx_deriving.show, ppx_deriving.ord, srk, Z3, apron, apron.boxMPQ, apron.octMPQ, apron.polkaMPQ, pa
MainIs: patools.ml
CCOpt: -annot
CompiledObject: native
Executable duet
Path: duet
MainIs: duet.ml
BuildDepends: batteries, ppx_deriving, ppx_deriving.show, ppx_deriving.ord, gmp, camlidl, apron, apron.boxMPQ, apron.octMPQ, apron.polkaMPQ, Z3, srk, apak, cil, cil.default-features, pa, ocrs
CompiledObject: native
Install: false
Executable cca
Path: cca
MainIs: cca.ml
BuildDepends: batteries, ppx_deriving, ppx_deriving.show, ppx_deriving.ord, gmp, camlidl, apron, apron.boxMPQ, apron.octMPQ, apron.polkaMPQ, Z3, srk, apak, cil, cil.default-features, pa, ocrs
CompiledObject: native
Install: false
Test apak
Command: $test_apak
TestTools: test_apak
run$: flag(tests)
Test srk
Command: $test_srk
TestTools: test_srk
run$: flag(tests)
Test patools
Command: $test_patools
TestTools: test_patools
run$: flag(tests)
Test regression
Command: ./regression.sh run pa coarsen hdfg chdfg proofspace cra
TestTools: duet
run$: flag(tests)
Document API
Title: API reference for Srk
Type: OCamlbuild (0.4)
XOCamlbuildPath: .
XOCamlbuildLibraries: srk, apak