Revision 52cfee34 src/inliner.ml
src/inliner.ml | ||
---|---|---|
209 | 209 |
let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in |
210 | 210 |
mkexpr loc (Expr_appl ("=", args, None)) |
211 | 211 |
}]; |
212 |
node_dec_stateless = true; |
|
213 |
node_stateless = None; |
|
212 | 214 |
node_spec = Some |
213 | 215 |
{requires = []; |
214 | 216 |
ensures = [EnsuresExpr (mkeexpr loc (EExpr_ident ok_ident))]; |
Also available in: Unified diff