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
|
(*
* This file is part of Coccinelle, licensed under the terms of the GPL v2.
* See copyright.txt in the Coccinelle source code for more information.
* The Coccinelle source code can be obtained at http://coccinelle.lip6.fr
*)
open Ast_ctl
module type SUBST =
sig
type value
type mvar
val eq_mvar : mvar -> mvar -> bool
val eq_val : value -> value -> bool
val merge_val : value -> value -> value
val print_mvar : mvar -> unit
val print_value : value -> unit
end
module type GRAPH =
sig
type node
type cfg
val predecessors: cfg -> node -> node list
val successors: cfg -> node -> node list
val direct_predecessors: cfg -> node -> node list
val direct_successors: cfg -> node -> node list
val extract_is_loop : cfg -> node -> bool
val print_node : node -> unit
val size : cfg -> int
val print_graph : cfg -> string option ->
(node * string) list -> (node * string) list -> string -> unit
end
module OGRAPHEXT_GRAPH :
sig
type node = int
module G : Ograph_extended.S
type cfg = string G.ograph_mutable
val predecessors : cfg -> node -> node list
val print_node : node -> unit
end
module type PREDICATE =
sig
type t
val print_predicate : t -> unit
end
module CTL_ENGINE :
functor (SUB : SUBST) ->
functor (G : GRAPH) ->
functor (P : PREDICATE) ->
sig
type substitution = (SUB.mvar, SUB.value) Ast_ctl.generic_subst list
type ('pred,'anno) witness =
(G.node, substitution,
('pred, SUB.mvar, 'anno) Ast_ctl.generic_ctl list)
Ast_ctl.generic_witnesstree
type ('pred,'anno) triples =
(G.node * substitution * ('pred,'anno) witness list) list
val sat :
G.cfg * (P.t -> (P.t,'anno) triples) * (P.t -> bool) *
G.node list ->
(P.t, SUB.mvar, 'c) Ast_ctl.generic_ctl ->
(P.t list list (* optional and required things *)) ->
(P.t,'anno) triples
val print_bench : unit -> unit
end
val get_graph_files : unit -> string list
val get_graph_comp_files : string -> string list
|
