2 * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen
3 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
4 * This file is part of Coccinelle.
6 * Coccinelle is free software: you can redistribute it and/or modify
7 * it under the terms of the GNU General Public License as published by
8 * the Free Software Foundation, according to version 2 of the License.
10 * Coccinelle is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
15 * You should have received a copy of the GNU General Public License
16 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
18 * The authors reserve the right to distribute this or future versions of
19 * Coccinelle under other licenses.
24 * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen
25 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
26 * This file is part of Coccinelle.
28 * Coccinelle is free software: you can redistribute it and/or modify
29 * it under the terms of the GNU General Public License as published by
30 * the Free Software Foundation, according to version 2 of the License.
32 * Coccinelle is distributed in the hope that it will be useful,
33 * but WITHOUT ANY WARRANTY; without even the implied warranty of
34 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
35 * GNU General Public License for more details.
37 * You should have received a copy of the GNU General Public License
38 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
40 * The authors reserve the right to distribute this or future versions of
41 * Coccinelle under other licenses.
46 (* ---------------------------------------------------------------------- *)
48 (* ---------------------------------------------------------------------- *)
50 type strict
= STRICT
| NONSTRICT
52 type keep_binding
= bool (* true = put in witness tree *)
54 (* CTL parameterised on basic predicates and metavar's*)
55 type ('pred
,'mvar
,'anno
) generic_ctl
=
59 | Not
of (('pred
,'mvar
,'anno
) generic_ctl
)
60 | Exists
of keep_binding
* 'mvar
* (('pred
,'mvar
,'anno
) generic_ctl
)
61 | And
of strict
* (('pred
,'mvar
,'anno
) generic_ctl
) *
62 (('pred
,'mvar
,'anno
) generic_ctl
)
63 | AndAny
of direction
* strict
* (('pred
,'mvar
,'anno
) generic_ctl
) *
64 (('pred
,'mvar
,'anno
) generic_ctl
)
65 | HackForStmt
of direction
* strict
* (('pred
,'mvar
,'anno
) generic_ctl
) *
66 (('pred
,'mvar
,'anno
) generic_ctl
)
67 | Or
of (('pred
,'mvar
,'anno
) generic_ctl
) *
68 (('pred
,'mvar
,'anno
) generic_ctl
)
69 | Implies
of (('pred
,'mvar
,'anno
) generic_ctl
) *
70 (('pred
,'mvar
,'anno
) generic_ctl
)
71 | AF
of direction
* strict
* (('pred
,'mvar
,'anno
) generic_ctl
)
72 | AX
of direction
* strict
* (('pred
,'mvar
,'anno
) generic_ctl
)
73 | AG
of direction
* strict
* (('pred
,'mvar
,'anno
) generic_ctl
)
74 | AW
of direction
* strict
*
75 (* versions with exists v *)
76 (('pred
,'mvar
,'anno
) generic_ctl
) * (('pred
,'mvar
,'anno
) generic_ctl
)
77 | AU
of direction
* strict
*
78 (* versions with exists v *)
79 (('pred
,'mvar
,'anno
) generic_ctl
) * (('pred
,'mvar
,'anno
) generic_ctl
)
80 | EF
of direction
* (('pred
,'mvar
,'anno
) generic_ctl
)
81 | EX
of direction
* (('pred
,'mvar
,'anno
) generic_ctl
)
82 | EG
of direction
* (('pred
,'mvar
,'anno
) generic_ctl
)
83 | EU
of direction
* (('pred
,'mvar
,'anno
) generic_ctl
) *
84 (('pred
,'mvar
,'anno
) generic_ctl
)
86 (('pred
,'mvar
,'anno
) generic_ctl
) *
87 (('pred
,'mvar
,'anno
) generic_ctl
)
88 | LetR
of direction
* string * (* evals phi1 wrt reachable states *)
89 (('pred
,'mvar
,'anno
) generic_ctl
) *
90 (('pred
,'mvar
,'anno
) generic_ctl
)
92 | SeqOr
of (('pred
,'mvar
,'anno
) generic_ctl
) *
93 (('pred
,'mvar
,'anno
) generic_ctl
)
94 | Uncheck
of (('pred
,'mvar
,'anno
) generic_ctl
)
95 | InnerAnd
of (('pred
,'mvar
,'anno
) generic_ctl
)
96 | XX
of (('pred
,'mvar
,'anno
) generic_ctl
) (* fake, used in asttoctl *)
98 and direction
= FORWARD
(* the normal way *) | BACKWARD
(* toward the start *)
100 let unwrap (ctl
,_
) = ctl
101 let rewrap (_
,model
) ctl
= (ctl
,model
)
102 let get_line (_
,l
) = l
105 (* NOTE: No explicit representation of the bottom subst., i.e., FALSE *)
106 type ('mvar
,'
value) generic_subst
=
107 | Subst
of 'mvar
* '
value
108 | NegSubst
of 'mvar
* '
value
109 type ('mvar
,'
value) generic_substitution
= ('mvar
,'
value) generic_subst list
111 type ('state
,'subst
,'anno
) generic_witnesstree
=
113 'state
* 'subst
* 'anno
* ('state
,'subst
,'anno
) generic_witnesstree list
114 | NegWit
of ('state
,'subst
,'anno
) generic_witnesstree
116 (* ---------------------------------------------------------------------- *)
118 type 'a modif
= Modif
of 'a
| UnModif
of 'a
| Control
120 (* ---------------------------------------------------------------------- *)