unsigned int get_data(void *wrapper) {
return ((tag_elem_t*) wrapper)->data;
}
- @Happens_before:
- Enqueue -> Dequeue
+ @Happens_before: Enqueue -> Dequeue
@End
*/
@Interface: Enqueue
@Commit_point_set: Enqueue_Point
@ID: get_and_inc(tag)
- @Action:
- tag_elem_t *elem = new_tag_elem(__ID__, data);
- push_back(__queue, elem);
+ @Action: push_back(__queue, new_tag_elem(__ID__, data));
+ //tag_elem_t *elem = new_tag_elem(__ID__, data);
+ //push_back(__queue, elem);
@End
*/
void enqueue(T data)
@Action:
T _Old_Val = get_data(front(__queue));
pop_front(__queue);
- @Post_check:
- _Old_Val == __RET__
+ @Post_check: _Old_Val == __RET__
@End
*/
T dequeue()