@@ -890,9 +890,9 @@ fn seq_states(&_fn_info_map fm, &fn_info enclosing,
890
890
}
891
891
892
892
fn find_pre_post_state_exprs ( & _fn_info_map fm,
893
- & fn_info enclosing ,
894
- & prestate pres,
895
- & ann a, & vec[ @expr] es ) -> bool {
893
+ & fn_info enclosing ,
894
+ & prestate pres,
895
+ & ann a, & vec[ @expr] es ) -> bool {
896
896
auto res = seq_states ( fm, enclosing, pres, es) ;
897
897
set_prestate_ann ( a, pres) ;
898
898
set_poststate_ann ( a, res. _1 ) ;
@@ -918,21 +918,21 @@ fn find_pre_post_state_expr(&_fn_info_map fm, &fn_info enclosing,
918
918
case ( expr_call ( ?operator, ?operands, ?a) ) {
919
919
/* do the prestate for the rator */
920
920
changed = find_pre_post_state_expr ( fm, enclosing, pres, operator)
921
- || changed;
921
+ || changed;
922
922
/* rands go left-to-right */
923
923
ret ( find_pre_post_state_exprs ( fm, enclosing,
924
- expr_poststate ( * operator) , a, operands)
925
- || changed) ;
924
+ expr_poststate ( * operator) , a, operands)
925
+ || changed) ;
926
926
}
927
927
case ( expr_path ( _, _, ?a) ) {
928
928
pure_exp ( a, pres) ;
929
929
ret false;
930
930
}
931
931
case ( expr_log ( ?e, ?a) ) {
932
- changed = find_pre_post_state_expr ( fm, enclosing, pres, e) ;
933
- set_prestate_ann ( a, pres) ;
934
- set_poststate_ann ( a, expr_poststate ( * e) ) ;
935
- ret changed;
932
+ changed = find_pre_post_state_expr ( fm, enclosing, pres, e) ;
933
+ set_prestate_ann ( a, pres) ;
934
+ set_poststate_ann ( a, expr_poststate ( * e) ) ;
935
+ ret changed;
936
936
}
937
937
case ( _) {
938
938
log ( "find_pre_post_state_expr: implement this case!" ) ;
@@ -954,23 +954,23 @@ fn find_pre_post_state_stmt(&_fn_info_map fm, &fn_info enclosing,
954
954
case ( ast. decl_local ( ?alocal) ) {
955
955
alt ( alocal. init ) {
956
956
case ( some[ ast. initializer ] ( ?an_init) ) {
957
- changed = find_pre_post_state_expr
958
- ( fm, enclosing, pres, an_init. expr ) || changed;
959
- set_prestate ( stmt_ann, expr_prestate ( * an_init. expr ) ) ;
960
- set_poststate ( stmt_ann, expr_poststate ( * an_init. expr ) ) ;
961
- gen ( enclosing, stmt_ann, alocal. id ) ;
962
- ret changed;
963
- }
964
- case ( none[ ast. initializer ] ) {
965
- set_prestate ( stmt_ann, pres) ;
966
- set_poststate ( stmt_ann, pres) ;
967
- ret false;
968
- }
957
+ changed = find_pre_post_state_expr
958
+ ( fm, enclosing, pres, an_init. expr ) || changed;
959
+ set_prestate ( stmt_ann, expr_prestate ( * an_init. expr ) ) ;
960
+ set_poststate ( stmt_ann, expr_poststate ( * an_init. expr ) ) ;
961
+ gen ( enclosing, stmt_ann, alocal. id ) ;
962
+ ret changed;
963
+ }
964
+ case ( none[ ast. initializer ] ) {
965
+ set_prestate ( stmt_ann, pres) ;
966
+ set_poststate ( stmt_ann, pres) ;
967
+ ret false;
968
+ }
969
969
}
970
970
}
971
- case ( ast. decl_item ( ?an_item) ) {
972
- be find_pre_post_state_item ( fm, an_item) ;
973
- }
971
+ case ( ast. decl_item ( ?an_item) ) {
972
+ be find_pre_post_state_item ( fm, an_item) ;
973
+ }
974
974
}
975
975
}
976
976
case ( stmt_expr ( ?e, ?a) ) {
@@ -989,7 +989,6 @@ fn find_pre_post_state_stmt(&_fn_info_map fm, &fn_info enclosing,
989
989
returns a boolean flag saying whether any pre- or poststates changed */
990
990
fn find_pre_post_state_block( & _fn_info_map fm, & fn_info enclosing , block b)
991
991
-> bool {
992
- log ( "pre_post_state_block: " + uistr ( fm. size ( ) ) + " " + uistr ( enclosing. size ( ) ) ) ;
993
992
994
993
auto changed = false ;
995
994
auto num_local_vars = num_locals ( enclosing) ;
@@ -1023,11 +1022,8 @@ fn find_pre_post_state_fn(&_fn_info_map f_info, &fn_info fi, &ast._fn f)
1023
1022
}
1024
1023
1025
1024
fn fixed_point_states ( _fn_info_map fm, fn_info f_info,
1026
- // with no ampersands for the first two args, and likewise for find_pre_post_state_fn,
1027
- // I got a segfault
1028
1025
fn ( & _fn_info_map , & fn_info , & ast . _fn) -> bool f,
1029
1026
& ast. _fn start ) -> ( ) {
1030
- log ( "fixed_point_states: " + uistr ( fm. size ( ) ) + " " + uistr ( f_info. size ( ) ) ) ;
1031
1027
1032
1028
auto changed = f ( fm, f_info, start) ;
1033
1029
@@ -1061,11 +1057,11 @@ fn check_states_stmt(fn_info enclosing, &stmt s) -> () {
1061
1057
1062
1058
if ( !implies ( pres, prec) ) {
1063
1059
log ( "check_states_stmt: unsatisfied precondition for " ) ;
1064
- log_stmt ( s) ;
1065
- log ( "Precondition: " ) ;
1066
- log_bitv ( enclosing, prec) ;
1067
- log ( "Prestate: " ) ;
1068
- log_bitv ( enclosing, pres) ;
1060
+ log_stmt ( s) ;
1061
+ log ( "Precondition: " ) ;
1062
+ log_bitv ( enclosing, prec) ;
1063
+ log ( "Prestate: " ) ;
1064
+ log_bitv ( enclosing, pres) ;
1069
1065
fail;
1070
1066
}
1071
1067
}
@@ -1095,8 +1091,6 @@ fn check_item_fn_state(&_fn_info_map f_info_map, &span sp, ident i,
1095
1091
check ( f_info_map. contains_key ( id) ) ;
1096
1092
auto f_info = f_info_map. get ( id) ;
1097
1093
1098
- log ( "check_item_fn_state: id = " + i + " " + uistr ( f_info_map. size ( ) ) + " " + uistr ( f_info. size ( ) ) ) ;
1099
-
1100
1094
/* Compute the pre- and post-states for this function */
1101
1095
auto g = find_pre_post_state_fn;
1102
1096
fixed_point_states ( f_info_map, f_info, g, f) ;
0 commit comments