30e8c600b2cebef61fff76ddfd45bd806b5c0f59
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.
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.
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.
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/>.
20 * The authors reserve the right to distribute this or future versions of
21 * Coccinelle under other licenses.
26 (* ---------------------------------------------------------------------- *)
28 (* ---------------------------------------------------------------------- *)
30 type strict
= STRICT
| NONSTRICT
32 type keep_binding
= bool (* true = put in witness tree *)
34 (* CTL parameterised on basic predicates and metavar's*)
35 type ('pred
,'mvar
,'anno
) generic_ctl
=
39 | Not
of (('pred
,'mvar
,'anno
) generic_ctl
)
40 | Exists
of keep_binding
* 'mvar
* (('pred
,'mvar
,'anno
) generic_ctl
)
41 | And
of strict
* (('pred
,'mvar
,'anno
) generic_ctl
) *
42 (('pred
,'mvar
,'anno
) generic_ctl
)
43 | AndAny
of direction
* strict
* (('pred
,'mvar
,'anno
) generic_ctl
) *
44 (('pred
,'mvar
,'anno
) generic_ctl
)
45 | HackForStmt
of direction
* strict
* (('pred
,'mvar
,'anno
) generic_ctl
) *
46 (('pred
,'mvar
,'anno
) generic_ctl
)
47 | Or
of (('pred
,'mvar
,'anno
) generic_ctl
) *
48 (('pred
,'mvar
,'anno
) generic_ctl
)
49 | Implies
of (('pred
,'mvar
,'anno
) generic_ctl
) *
50 (('pred
,'mvar
,'anno
) generic_ctl
)
51 | AF
of direction
* strict
* (('pred
,'mvar
,'anno
) generic_ctl
)
52 | AX
of direction
* strict
* (('pred
,'mvar
,'anno
) generic_ctl
)
53 | AG
of direction
* strict
* (('pred
,'mvar
,'anno
) generic_ctl
)
54 | AW
of direction
* strict
*
55 (* versions with exists v *)
56 (('pred
,'mvar
,'anno
) generic_ctl
) * (('pred
,'mvar
,'anno
) generic_ctl
)
57 | AU
of direction
* strict
*
58 (* versions with exists v *)
59 (('pred
,'mvar
,'anno
) generic_ctl
) * (('pred
,'mvar
,'anno
) generic_ctl
)
60 | EF
of direction
* (('pred
,'mvar
,'anno
) generic_ctl
)
61 | EX
of direction
* (('pred
,'mvar
,'anno
) generic_ctl
)
62 | EG
of direction
* (('pred
,'mvar
,'anno
) generic_ctl
)
63 | EU
of direction
* (('pred
,'mvar
,'anno
) generic_ctl
) *
64 (('pred
,'mvar
,'anno
) generic_ctl
)
66 (('pred
,'mvar
,'anno
) generic_ctl
) *
67 (('pred
,'mvar
,'anno
) generic_ctl
)
68 | LetR
of direction
* string * (* evals phi1 wrt reachable states *)
69 (('pred
,'mvar
,'anno
) generic_ctl
) *
70 (('pred
,'mvar
,'anno
) generic_ctl
)
72 | SeqOr
of (('pred
,'mvar
,'anno
) generic_ctl
) *
73 (('pred
,'mvar
,'anno
) generic_ctl
)
74 | Uncheck
of (('pred
,'mvar
,'anno
) generic_ctl
)
75 | InnerAnd
of (('pred
,'mvar
,'anno
) generic_ctl
)
76 | XX
of (('pred
,'mvar
,'anno
) generic_ctl
) (* fake, used in asttoctl *)
78 and direction
= FORWARD
(* the normal way *) | BACKWARD
(* toward the start *)
80 let unwrap (ctl
,_
) = ctl
81 let rewrap (_
,model
) ctl
= (ctl
,model
)
82 let get_line (_
,l
) = l
85 (* NOTE: No explicit representation of the bottom subst., i.e., FALSE *)
86 type ('mvar
,'
value) generic_subst
=
87 | Subst
of 'mvar
* '
value
88 | NegSubst
of 'mvar
* '
value
89 type ('mvar
,'
value) generic_substitution
= ('mvar
,'
value) generic_subst list
91 type ('state
,'subst
,'anno
) generic_witnesstree
=
93 'state
* 'subst
* 'anno
* ('state
,'subst
,'anno
) generic_witnesstree list
94 | NegWit
of ('state
,'subst
,'anno
) generic_witnesstree
96 (* ---------------------------------------------------------------------- *)
98 type 'a modif
= Modif
of 'a
| UnModif
of 'a
| Control
100 (* ---------------------------------------------------------------------- *)