Commit | Line | Data |
---|---|---|
9bc82bae C |
1 | (* |
2 | * Copyright 2010, INRIA, University of Copenhagen | |
3 | * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix | |
4 | * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen | |
5 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix | |
6 | * This file is part of Coccinelle. | |
7 | * | |
8 | * Coccinelle is free software: you can redistribute it and/or modify | |
9 | * it under the terms of the GNU General Public License as published by | |
10 | * the Free Software Foundation, according to version 2 of the License. | |
11 | * | |
12 | * Coccinelle is distributed in the hope that it will be useful, | |
13 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
14 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
15 | * GNU General Public License for more details. | |
16 | * | |
17 | * You should have received a copy of the GNU General Public License | |
18 | * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>. | |
19 | * | |
20 | * The authors reserve the right to distribute this or future versions of | |
21 | * Coccinelle under other licenses. | |
22 | *) | |
23 | ||
24 | ||
c491d8ee C |
25 | (* |
26 | * Copyright 2010, INRIA, University of Copenhagen | |
27 | * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix | |
28 | * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen | |
29 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix | |
30 | * This file is part of Coccinelle. | |
31 | * | |
32 | * Coccinelle is free software: you can redistribute it and/or modify | |
33 | * it under the terms of the GNU General Public License as published by | |
34 | * the Free Software Foundation, according to version 2 of the License. | |
35 | * | |
36 | * Coccinelle is distributed in the hope that it will be useful, | |
37 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
38 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
39 | * GNU General Public License for more details. | |
40 | * | |
41 | * You should have received a copy of the GNU General Public License | |
42 | * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>. | |
43 | * | |
44 | * The authors reserve the right to distribute this or future versions of | |
45 | * Coccinelle under other licenses. | |
46 | *) | |
47 | ||
48 | ||
34e49164 C |
49 | open Ast_ctl |
50 | ||
51 | module type SUBST = | |
52 | sig | |
53 | type value | |
54 | type mvar | |
55 | val eq_mvar : mvar -> mvar -> bool | |
56 | val eq_val : value -> value -> bool | |
57 | val merge_val : value -> value -> value | |
58 | val print_mvar : mvar -> unit | |
59 | val print_value : value -> unit | |
60 | end | |
61 | ||
62 | module type GRAPH = | |
ae4735db C |
63 | sig |
64 | type node | |
65 | type cfg | |
34e49164 C |
66 | val predecessors: cfg -> node -> node list |
67 | val successors: cfg -> node -> node list | |
68 | val extract_is_loop : cfg -> node -> bool | |
69 | val print_node : node -> unit | |
70 | val size : cfg -> int | |
485bce71 C |
71 | val print_graph : cfg -> string option -> |
72 | (node * string) list -> (node * string) list -> string -> unit | |
34e49164 C |
73 | end |
74 | ||
75 | module OGRAPHEXT_GRAPH : | |
76 | sig | |
77 | type node = int | |
78 | type cfg = (string, unit) Ograph_extended.ograph_mutable | |
79 | val predecessors : | |
80 | < predecessors : 'a -> < tolist : ('b * 'c) list; .. >; .. > -> | |
81 | 'a -> 'b list | |
82 | val print_node : node -> unit | |
83 | end | |
84 | ||
85 | module type PREDICATE = | |
86 | sig | |
87 | type t | |
88 | val print_predicate : t -> unit | |
89 | end | |
90 | ||
91 | module CTL_ENGINE : | |
92 | functor (SUB : SUBST) -> | |
93 | functor (G : GRAPH) -> | |
94 | functor (P : PREDICATE) -> | |
95 | sig | |
96 | ||
97 | type substitution = (SUB.mvar, SUB.value) Ast_ctl.generic_subst list | |
98 | ||
99 | type ('pred,'anno) witness = | |
100 | (G.node, substitution, | |
101 | ('pred, SUB.mvar, 'anno) Ast_ctl.generic_ctl list) | |
102 | Ast_ctl.generic_witnesstree | |
103 | ||
104 | type ('pred,'anno) triples = | |
105 | (G.node * substitution * ('pred,'anno) witness list) list | |
106 | ||
107 | val sat : | |
108 | G.cfg * (P.t -> (P.t,'anno) triples) * G.node list -> | |
109 | (P.t, SUB.mvar, 'c) Ast_ctl.generic_ctl -> | |
110 | (P.t list list (* optional and required things *)) -> | |
111 | (P.t,'anno) triples | |
112 | ||
113 | val print_bench : unit -> unit | |
114 | end | |
485bce71 C |
115 | |
116 | val get_graph_files : unit -> string list | |
117 | val get_graph_comp_files : string -> string list | |
ae4735db | 118 |