@@ -31,15 +31,15 @@ type poststate = t;
31
31
*/
32
32
33
33
/* named thus so as not to confuse with prestate and poststate */
34
- type pre_and_post = @ { precondition : precond , postcondition : postcond } ;
34
+ type pre_and_post = { precondition : precond , postcondition : postcond } ;
35
35
36
36
37
37
/* FIXME: once it's implemented: */
38
38
39
39
// : ((*.precondition).nbits == (*.postcondition).nbits);
40
40
type pre_and_post_state = { prestate : prestate , poststate : poststate } ;
41
41
42
- type ts_ann = @ { conditions : pre_and_post , states : pre_and_post_state } ;
42
+ type ts_ann = { conditions : pre_and_post , states : pre_and_post_state } ;
43
43
44
44
fn true_precond ( num_vars : uint ) -> precond { ret create_tritv ( num_vars) ; }
45
45
@@ -58,8 +58,8 @@ fn false_postcond(num_vars: uint) -> postcond {
58
58
}
59
59
60
60
fn empty_pre_post ( num_vars : uint ) -> pre_and_post {
61
- ret @ { precondition : empty_prestate ( num_vars) ,
62
- postcondition : empty_poststate ( num_vars) } ;
61
+ ret { precondition : empty_prestate ( num_vars) ,
62
+ postcondition : empty_poststate ( num_vars) } ;
63
63
}
64
64
65
65
fn empty_states ( num_vars : uint ) -> pre_and_post_state {
@@ -68,8 +68,8 @@ fn empty_states(num_vars: uint) -> pre_and_post_state {
68
68
}
69
69
70
70
fn empty_ann ( num_vars : uint ) -> ts_ann {
71
- ret @ { conditions : empty_pre_post ( num_vars) ,
72
- states : empty_states ( num_vars) } ;
71
+ ret { conditions : empty_pre_post ( num_vars) ,
72
+ states : empty_states ( num_vars) } ;
73
73
}
74
74
75
75
fn get_pre ( & & p: pre_and_post ) -> precond { ret p. precondition ; }
@@ -224,8 +224,8 @@ fn ann_prestate(a: ts_ann) -> prestate { ret a.states.prestate; }
224
224
fn ann_poststate ( a : ts_ann ) -> poststate { ret a. states . poststate ; }
225
225
226
226
fn pp_clone ( p : pre_and_post ) -> pre_and_post {
227
- ret @ { precondition : clone ( p. precondition ) ,
228
- postcondition : clone ( p. postcondition ) } ;
227
+ ret { precondition : clone ( p. precondition ) ,
228
+ postcondition : clone ( p. postcondition ) } ;
229
229
}
230
230
231
231
fn clone ( p : prestate ) -> prestate { ret tritv_clone ( p) ; }
0 commit comments