mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Rewrite pre_postconditions to use walk instead of fold

Browse Source
This commit is contained in:
Tim Chevalier 2011-05-18 16:59:34 -07:00 committed by Graydon Hoare
parent 2cd769e358
commit c0f728712b
2 changed files with 7 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/comp/middle/tstate/ck.rs
View File

@ -62,7 +62,7 @@
import annotate::annotate_crate;
import collect_locals::mk_f_to_fn_info;
import pre_post_conditions::check_item_fn;
import pre_post_conditions::fn_pre_post;
import states::find_pre_post_state_fn;
fn check_states_expr(&fn_ctxt fcx, @expr e) -> () {
@ -199,11 +199,10 @@ fn check_crate(ty::node_type_table nt, ty::ctxt cx, @crate crate) -> @crate {
annotate_crate(ccx, *crate);
/* Compute the pre and postcondition for every subexpression */
auto fld = new_identity_fold[crate_ctxt]();
fld = @rec(fold_item_fn = bind check_item_fn(_,_,_,_,_,_,_) with *fld);
auto with_pre_postconditions =
fold_crate[crate_ctxt](ccx, fld, crate);
auto do_pre_post = walk::default_visitor();
do_pre_post = rec(visit_fn_pre = bind fn_pre_post(ccx, _, _, _)
with do_pre_post);
walk::walk_crate(do_pre_post, *crate);
auto fld1 = new_identity_fold[crate_ctxt]();
@ -211,7 +210,7 @@ fn check_crate(ty::node_type_table nt, ty::ctxt cx, @crate crate) -> @crate {
fold_obj = bind check_obj_state(_,_,_,_)
with *fld1);
ret fold_crate[crate_ctxt](ccx, fld1, with_pre_postconditions);
ret fold_crate[crate_ctxt](ccx, fld1, crate);
}
//

9
src/comp/middle/tstate/pre_post_conditions.rs
View File

@ -679,18 +679,11 @@ fn find_pre_post_fn(&fn_ctxt fcx, &_fn f) -> () {
find_pre_post_block(fcx, f.body);
}
fn check_item_fn(&crate_ctxt ccx, &span sp, &ident i, &_fn f,
&vec[ty_param] ty_params,
&def_id id, &ann a) -> @item {
log("check_item_fn:");
log_fn(f, i, ty_params);
fn fn_pre_post(crate_ctxt ccx, &_fn f, &ident i, &def_id id) -> () {
assert (ccx.fm.contains_key(id));
auto fcx = rec(enclosing=ccx.fm.get(id),
id=id, name=i, ccx=ccx);
find_pre_post_fn(fcx, f);
ret @respan(sp, item_fn(i, f, ty_params, id, a));
}
//