Revision 36454535
Added by Pierre-Loïc Garoche over 10 years ago
src/corelang.mli | ||
---|---|---|
80 | 80 |
| Expr_phclock of expr * rat |
81 | 81 |
and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *) |
82 | 82 |
|
83 |
type assert_t = |
|
84 |
{ |
|
85 |
assert_expr: expr; |
|
86 |
assert_loc: Location.t |
|
87 |
} |
|
88 |
|
|
89 | 83 |
type eq = |
90 | 84 |
{eq_lhs: ident list; |
91 | 85 |
eq_rhs: expr; |
92 | 86 |
eq_loc: Location.t} |
93 | 87 |
|
88 |
type assert_t = |
|
89 |
{ |
|
90 |
assert_expr: expr * eq list; |
|
91 |
assert_loc: Location.t |
|
92 |
} |
|
93 |
|
|
94 | 94 |
type node_desc = |
95 | 95 |
{node_id: ident; |
96 | 96 |
mutable node_type: Types.type_expr; |
... | ... | |
250 | 250 |
|
251 | 251 |
val update_expr_annot: expr -> LustreSpec.expr_annot -> expr |
252 | 252 |
|
253 |
val substitute_expr: var_decl list -> eq list -> expr -> expr |
|
253 | 254 |
|
254 | 255 |
(** Annotation expression related functions *) |
255 | 256 |
val mkeexpr: Location.t -> expr -> eexpr |
Also available in: Unified diff
Merged horn_traces branch