import std::uint;
import syntax::ast::*;
import syntax::codemap::span;
+import syntax::visit;
import util::common;
import util::common::log_block;
import std::map::new_int_hash;
fn eq(&tup(ident, def_id) p, &tup(ident, def_id) q) -> bool {
ret p._1 == q._1;
}
-
- // FIXME: Remove this vec->ivec conversion.
- let (@constr_arg_use)[] cau_ivec = ~[];
- for (@constr_arg_use cau in pd.node.args) {
- cau_ivec += ~[cau];
- }
- if (ty::args_eq(eq, cau_ivec, occ)) { ret pd.node.bit_num; }
+ if (ty::args_eq(eq, pd.node.args, occ)) { ret pd.node.bit_num; }
}
fcx.ccx.tcx.sess.bug("match_args: no match for occurring args");
}
case (_) { oper_assign }
}
}
+
+// default function visitor
+fn do_nothing[T](&_fn f, &ty_param[] tp, &span sp, &fn_ident i,
+ node_id iid, &T cx, &visit::vt[T] v) {
+}
//
// Local Variables:
// mode: rust
import ast::return;
import ast::noreturn;
import ast::expr;
-import syntax::walk;
+import syntax::visit;
import syntax::codemap::span;
import middle::ty::type_is_nil;
import middle::ty::ret_ty_of_fn;
}
}
-fn check_states_expr(&fn_ctxt fcx, &@expr e) {
+fn check_states_expr(&@expr e, &fn_ctxt fcx, &visit::vt[fn_ctxt] v) {
+ visit::visit_expr(e, fcx, v);
+
let precond prec = expr_precond(fcx.ccx, e);
let prestate pres = expr_prestate(fcx.ccx, e);
}
}
-fn check_states_stmt(&fn_ctxt fcx, &@stmt s) {
+fn check_states_stmt(&@stmt s, &fn_ctxt fcx, &visit::vt[fn_ctxt] v) {
+ visit::visit_stmt(s, fcx, v);
+
auto a = stmt_to_ann(fcx.ccx, *s);
let precond prec = ann_precond(a);
let prestate pres = ann_prestate(a);
because we want the smallest possible erroneous statement
or expression. */
- let @mutable bool keepgoing = @mutable true;
-
- /* TODO probably should use visit instead */
-
- fn quit(@mutable bool keepgoing, &@ast::item i) {
- *keepgoing = false;
- }
- fn kg(@mutable bool keepgoing) -> bool {
- ret *keepgoing;
- }
+ auto visitor = visit::default_visitor[fn_ctxt]();
- auto v = rec (visit_stmt_post=bind check_states_stmt(fcx, _),
- visit_expr_post=bind check_states_expr(fcx, _),
- visit_item_pre=bind quit(keepgoing, _),
- keep_going=bind kg(keepgoing)
- with walk::default_visitor());
-
- walk::walk_fn(v, f, tps, sp, i, id);
+ visitor = @rec(visit_stmt=check_states_stmt,
+ visit_expr=check_states_expr,
+ visit_fn=do_nothing
+ with *visitor);
+ visit::visit_fn(f, tps, sp, i, id, fcx, visit::mk_vt(visitor));
/* Check that the return value is initialized */
auto post = aux::block_poststate(fcx.ccx, f.body);
check_states_against_conditions(fcx, f, tps, id, sp, i);
}
-fn fn_states(&crate_ctxt ccx, &_fn f, &ast::ty_param[] tps,
- &span sp, &fn_ident i, node_id id) {
+fn fn_states(&_fn f, &ast::ty_param[] tps,
+ &span sp, &fn_ident i, node_id id, &crate_ctxt ccx,
+ &visit::vt[crate_ctxt] v) {
+ visit::visit_fn(f, tps, sp, i, id, ccx, v);
/* Look up the var-to-bit-num map for this function */
-
+
assert (ccx.fm.contains_key(id));
auto f_info = ccx.fm.get(id);
auto name = option::from_maybe("anon", i);
annotate_crate(ccx, *crate);
/* Compute the pre and postcondition for every subexpression */
- auto do_pre_post = walk::default_visitor();
- do_pre_post =
- rec(visit_fn_post=bind fn_pre_post(ccx, _, _, _, _, _)
- with do_pre_post);
- walk::walk_crate(do_pre_post, *crate);
+ auto vtor = visit::default_visitor[crate_ctxt]();
+ vtor = @rec(visit_fn=fn_pre_post with *vtor);
+ visit::visit_crate(*crate, ccx, visit::mk_vt(vtor));
+
/* Check the pre- and postcondition against the pre- and poststate
for every expression */
-
- auto do_states = walk::default_visitor();
- do_states =
- rec(visit_fn_post=bind fn_states(ccx, _, _, _, _, _)
- with do_states);
- walk::walk_crate(do_states, *crate);
+ vtor = @rec(visit_fn=fn_states with *vtor);
+ visit::visit_crate(*crate, ccx, visit::mk_vt(vtor));
}
//
// Local Variables:
import walk::walk_crate;
import walk::walk_fn;
import walk::ast_visitor;
-import aux::cinit;
-import aux::ninit;
-import aux::npred;
-import aux::cpred;
-import aux::constraint;
-import aux::fn_info;
-import aux::crate_ctxt;
-import aux::num_constraints;
-import aux::constr_map;
-import aux::expr_to_constr;
-import aux::constraints_expr;
-import aux::node_id_to_def_strict;
+import aux::*;
import std::map::new_int_hash;
import util::common::new_def_hash;
import syntax::codemap::span;
// visit subexpressions
visit::visit_expr(e, cx, v);
}
-
-fn do_nothing(&_fn f, &ty_param[] tp, &span sp, &fn_ident i,
- node_id iid, &ctxt cx, &visit::vt[ctxt] v) {
-}
fn find_locals(&ty::ctxt tcx, &_fn f, &ty_param[] tps, &span sp, &fn_ident i,
node_id id) -> ctxt {
import bitvectors::gen;
import tritv::tritv_clone;
import syntax::ast::*;
+import syntax::visit;
import std::map::new_int_hash;
import util::common::new_def_hash;
import util::common::log_expr;
}
}
-fn fn_pre_post(crate_ctxt ccx, &_fn f, &ty_param[] tps,
- &span sp, &fn_ident i, node_id id) {
+fn fn_pre_post(&_fn f, &ty_param[] tps,
+ &span sp, &fn_ident i, node_id id, &crate_ctxt ccx,
+ &visit::vt[crate_ctxt] v) {
+ visit::visit_fn(f, tps, sp, i, id, ccx, v);
assert (ccx.fm.contains_key(id));
auto fcx = rec(enclosing=ccx.fm.get(id), id=id,
name=fn_ident_to_string(id, i), ccx=ccx);
import tstate::ann::set_prestate;
import tstate::ann::set_poststate;
import aux::*;
-/*
-import aux::crate_ctxt;
-import aux::fn_ctxt;
-import aux::num_constraints;
-import aux::expr_pp;
-import aux::stmt_pp;
-import aux::block_pp;
-import aux::set_pre_and_post;
-import aux::expr_prestate;
-import aux::expr_precond;
-import aux::expr_postcond;
-import aux::stmt_poststate;
-import aux::expr_poststate;
-import aux::block_prestate;
-import aux::block_poststate;
-import aux::block_precond;
-import aux::block_postcond;
-import aux::fn_info;
-import aux::log_pp;
-import aux::log_pp_err;
-import aux::extend_prestate_ann;
-import aux::extend_poststate_ann;
-import aux::set_prestate_ann;
-import aux::set_poststate_ann;
-import aux::pure_exp;
-import aux::log_tritv;
-import aux::log_tritv_err;
-import aux::stmt_to_ann;
-import aux::log_states;
-import aux::log_states_err;
-import aux::block_states;
-import aux::controlflow_expr;
-import aux::node_id_to_def;
-import aux::expr_to_constr;
-import aux::ninit;
-import aux::npred;
-import aux::path_to_ident;
-import aux::if_ty;
-import aux::if_check;
-import aux::plain_if;
-import aux::forget_in_poststate;
-import aux::forget_in_poststate_still_init;
-import aux::copy_in_poststate;
-import aux::copy_in_poststate_two;
-import aux::local_node_id_to_def;
-*/
import tritv::tritv_clone;
import tritv::tritv_set;
import tritv::ttrue;
auto changed = set_prestate_ann(fcx.ccx, id, loop_pres) |
find_pre_post_state_expr(fcx, pres, index);
- find_pre_post_state_block(fcx, expr_poststate(fcx.ccx, index), body);
+
+ // Make sure the index var is considered initialized
+ // in the body
+ auto index_post = tritv_clone(expr_poststate(fcx.ccx, index));
+ set_in_poststate_ident(fcx, l.node.id, l.node.ident, index_post);
+
+ changed |= find_pre_post_state_block(fcx, index_post, body);
if (has_nonlocal_exits(body)) {
// See [Break-unsound]
else {
auto res_p = intersect_states(expr_poststate(fcx.ccx, index),
block_poststate(fcx.ccx, body));
- /*
- auto res_p =
- intersect_postconds([expr_poststate(fcx.ccx, index),
- block_poststate(fcx.ccx, body)]); */
-
ret changed | set_poststate_ann(fcx.ccx, id, res_p);
}
}