@@ -20,13 +20,13 @@ type poststate = bitv::t; /* 1 means "this variable is definitely initialized"
20
20
initialized" */
21
21
22
22
/* named thus so as not to confuse with prestate and poststate */
23
- type pre_and_post = rec ( precond precondition , postcond postcondition ) ;
23
+ type pre_and_post = @ rec ( precond precondition , postcond postcondition ) ;
24
24
/* FIXME: once it's implemented: */
25
25
// : ((*.precondition).nbits == (*.postcondition).nbits);
26
26
27
27
type pre_and_post_state = rec ( prestate prestate, poststate poststate) ;
28
28
29
- type ts_ann = rec ( pre_and_post conditions, pre_and_post_state states) ;
29
+ type ts_ann = @ rec ( pre_and_post conditions, pre_and_post_state states) ;
30
30
31
31
fn true_precond ( uint num_vars ) -> precond {
32
32
be bitv:: create ( num_vars, false ) ;
@@ -49,18 +49,18 @@ fn false_postcond(uint num_vars) -> postcond {
49
49
}
50
50
51
51
fn empty_pre_post ( uint num_vars ) -> pre_and_post {
52
- ret ( rec ( precondition=empty_prestate ( num_vars) ,
53
- postcondition=empty_poststate ( num_vars) ) ) ;
52
+ ret ( @ rec ( precondition=empty_prestate ( num_vars) ,
53
+ postcondition=empty_poststate ( num_vars) ) ) ;
54
54
}
55
55
56
56
fn empty_states ( uint num_vars ) -> pre_and_post_state {
57
57
ret ( rec ( prestate=true_precond ( num_vars) ,
58
- poststate=true_postcond ( num_vars) ) ) ;
58
+ poststate=true_postcond ( num_vars) ) ) ;
59
59
}
60
60
61
61
fn empty_ann ( uint num_vars ) -> ts_ann {
62
- ret ( rec ( conditions=empty_pre_post ( num_vars) ,
63
- states=empty_states ( num_vars) ) ) ;
62
+ ret ( @ rec ( conditions=empty_pre_post ( num_vars) ,
63
+ states=empty_states ( num_vars) ) ) ;
64
64
}
65
65
66
66
fn get_pre ( & pre_and_post p) -> precond {
@@ -111,25 +111,25 @@ fn set_in_poststate(uint i, &pre_and_post_state s) -> bool {
111
111
112
112
// Sets all the bits in a's precondition to equal the
113
113
// corresponding bit in p's precondition.
114
- fn set_precondition ( @ ts_ann a , & precond p) -> ( ) {
114
+ fn set_precondition ( ts_ann a, & precond p) -> ( ) {
115
115
bitv:: copy ( a. conditions . precondition , p) ;
116
116
}
117
117
118
118
// Sets all the bits in a's postcondition to equal the
119
119
// corresponding bit in p's postcondition.
120
- fn set_postcondition ( @ ts_ann a , & postcond p) -> ( ) {
120
+ fn set_postcondition ( ts_ann a, & postcond p) -> ( ) {
121
121
bitv:: copy ( a. conditions . postcondition , p) ;
122
122
}
123
123
124
124
// Sets all the bits in a's prestate to equal the
125
125
// corresponding bit in p's prestate.
126
- fn set_prestate ( @ ts_ann a , & prestate p) -> bool {
126
+ fn set_prestate ( ts_ann a, & prestate p) -> bool {
127
127
ret bitv:: copy ( a. states . prestate , p) ;
128
128
}
129
129
130
130
// Sets all the bits in a's postcondition to equal the
131
131
// corresponding bit in p's postcondition.
132
- fn set_poststate ( @ ts_ann a , & poststate p) -> bool {
132
+ fn set_poststate ( ts_ann a, & poststate p) -> bool {
133
133
ret bitv:: copy ( a. states . poststate , p) ;
134
134
}
135
135
@@ -150,6 +150,16 @@ fn relax_prestate(uint i, &prestate p) -> bool {
150
150
ret was_set;
151
151
}
152
152
153
+ // Clears all the bits in p
154
+ fn clear ( & precond p) -> ( ) {
155
+ bitv:: clear ( p) ;
156
+ }
157
+
158
+ // Sets all the bits in p
159
+ fn set ( & precond p) -> ( ) {
160
+ bitv:: set_all ( p) ;
161
+ }
162
+
153
163
fn ann_precond ( & ts_ann a) -> precond {
154
164
ret a. conditions . precondition ;
155
165
}
@@ -163,8 +173,8 @@ fn ann_poststate(&ts_ann a) -> poststate {
163
173
}
164
174
165
175
fn pp_clone ( & pre_and_post p) -> pre_and_post {
166
- ret rec ( precondition=clone ( p. precondition ) ,
167
- postcondition=clone ( p. postcondition ) ) ;
176
+ ret @ rec( precondition=clone ( p. precondition ) ,
177
+ postcondition=clone ( p. postcondition ) ) ;
168
178
}
169
179
170
180
fn clone ( prestate p) -> prestate {
0 commit comments