Commit af31762a authored by Andrei Paskevich's avatar Andrei Paskevich

labels, labels, labels

parent 2e43db62
......@@ -74,6 +74,7 @@ type dloop_annotation = {
type dexpr = {
dexpr_desc : dexpr_desc;
dexpr_type : Denv.dty;
dexpr_lab : Ident.label list;
dexpr_loc : loc;
}
......@@ -101,7 +102,6 @@ and dexpr_desc =
| DEassert of assertion_kind * Ptree.lexpr
| DEmark of string * dexpr
| DEany of dutype_c
| DEnamed of Ptree.label * dexpr
and drecfun = (ident * Denv.dty) * dubinder list * dvariant option * dtriple
......@@ -173,6 +173,7 @@ and ipat_node =
type iexpr = {
iexpr_desc : iexpr_desc;
iexpr_type : ty;
iexpr_lab : Ident.label list;
iexpr_loc : loc;
}
......@@ -201,7 +202,6 @@ and iexpr_desc =
| IEassert of assertion_kind * Term.term
| IEmark of mark * iexpr
| IEany of itype_c
| IEnamed of Ptree.label * iexpr
and irecfun = ivsymbol * ibinder list * irec_variant option * itriple
......
This diff is collapsed.
......@@ -619,7 +619,7 @@ and wp_desc env rm e q = match e.expr_desc with
(* TODO: propagate call labels into c.c_post *)
let w = opaque_wp env rm c.c_effect.E.writes c.c_post q in
let p = wp_expl "precondition" c.c_pre in
let p = t_label ~loc:e.expr_loc p.t_label p in
let p = t_label ~loc:e.expr_loc (p.t_label @ e.expr_lab) p in
wp_and p w
and wp_triple env rm bl (p, e, q) =
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment