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