diff options
Diffstat (limited to 'FreeRTOS/Test/VeriFast/list/vListInsert.c')
| -rw-r--r-- | FreeRTOS/Test/VeriFast/list/vListInsert.c | 439 |
1 files changed, 220 insertions, 219 deletions
diff --git a/FreeRTOS/Test/VeriFast/list/vListInsert.c b/FreeRTOS/Test/VeriFast/list/vListInsert.c index 8e8886523..9a0278a84 100644 --- a/FreeRTOS/Test/VeriFast/list/vListInsert.c +++ b/FreeRTOS/Test/VeriFast/list/vListInsert.c @@ -1,6 +1,6 @@ /* * FreeRTOS V202112.00 - * Copyright (C) Amazon.com, Inc. or its affiliates. All Rights Reserved. + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. * * Permission is hereby granted, free of charge, to any person obtaining a copy of * this software and associated documentation files (the "Software"), to deal in @@ -24,24 +24,23 @@ * */ +/* *INDENT-OFF* */ + #include "proof/list.h" -ListItem_t * choose( List_t * list ); +ListItem_t * choose(List_t * list); /*@ requires DLS(&(list->xListEnd), ?endprev, &(list->xListEnd), endprev, ?cells, ?vals, ?container);@*/ - /*@ ensures DLS(&(list->xListEnd), endprev, &(list->xListEnd), endprev, cells, vals, container) &*& - * mem(result, cells) == true;@*/ + mem(result, cells) == true;@*/ void vListInsert( List_t * const pxList, ListItem_t * const pxNewListItem ) - /*@requires xLIST(pxList, ?len, ?idx, ?end, ?cells, ?vals) &*& - * xLIST_ITEM(pxNewListItem, ?val, _, _, _);@*/ - + xLIST_ITEM(pxNewListItem, ?val, _, _, _);@*/ /*@ensures xLIST(pxList, len+1, idx, end, ?new_cells, ?new_vals) &*& - * remove(pxNewListItem, new_cells) == cells - * ;@*/ + remove(pxNewListItem, new_cells) == cells +;@*/ { /*@xLIST_star_item(pxList, pxNewListItem);@*/ /*@open xLIST_ITEM(pxNewListItem, _, _, _, _);@*/ @@ -68,24 +67,23 @@ void vListInsert( List_t * const pxList, { /*@open DLS(end, endprev, end, endprev, cells, vals, pxList);@*/ /*@open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, pxList);@*/ - /*@ - * if (end != endprev) - * { - * assert DLS(endnext, end, end, endprev, tail(cells), tail(vals), pxList); - * if (endnext == endprev) - * { - * // done - * } - * else - * { - * dls_last_mem(endnext, end, end, endprev, tail(cells)); - * split(endnext, end, end, endprev, tail(cells), tail(vals), endprev, index_of(endprev, tail(cells))); - * } - * open DLS(endprev, _, _, _, _, _, _); - * open xLIST_ITEM(endprev, _, _, _, _); - * } - * @*/ + if (end != endprev) + { + assert DLS(endnext, end, end, endprev, tail(cells), tail(vals), pxList); + if (endnext == endprev) + { + // done + } + else + { + dls_last_mem(endnext, end, end, endprev, tail(cells)); + split(endnext, end, end, endprev, tail(cells), tail(vals), endprev, index_of(endprev, tail(cells))); + } + open DLS(endprev, _, _, _, _, _, _); + open xLIST_ITEM(endprev, _, _, _, _); + } + @*/ pxIterator = pxList->xListEnd.pxPrevious; } else @@ -110,55 +108,57 @@ void vListInsert( List_t * const pxList, * 4) Using a queue or semaphore before it has been initialised or * before the scheduler has been started (are interrupts firing * before vTaskStartScheduler() has been called?). + * 5) If the FreeRTOS port supports interrupt nesting then ensure that + * the priority of the tick interrupt is at or below + * configMAX_SYSCALL_INTERRUPT_PRIORITY. **********************************************************************/ - #ifdef VERIFAST /*< ***over-approximate list insert loop*** */ - pxIterator = choose( pxList ); - #else - for( pxIterator = ( ListItem_t * ) &( pxList->xListEnd ); pxIterator->pxNext->xItemValue <= xValueOfInsertion; pxIterator = pxIterator->pxNext ) /*lint !e826 !e740 !e9087 The mini list structure is used as the list end to save RAM. This is checked and valid. *//*lint !e440 The iterator moves to a different value, not xValueOfInsertion. */ - { - /* There is nothing to do here, just iterating to the wanted - * insertion position. */ - } - #endif +#ifdef VERIFAST /*< ***over-approximate list insert loop*** */ + pxIterator = choose(pxList); +#else + for( pxIterator = ( ListItem_t * ) &( pxList->xListEnd ); pxIterator->pxNext->xItemValue <= xValueOfInsertion; pxIterator = pxIterator->pxNext ) /*lint !e826 !e740 !e9087 The mini list structure is used as the list end to save RAM. This is checked and valid. *//*lint !e440 The iterator moves to a different value, not xValueOfInsertion. */ + { + /* There is nothing to do here, just iterating to the wanted + * insertion position. */ + } +#endif /*@int i = index_of(pxIterator, cells);@*/ - /*@ - * if (pxIterator == end) - * { - * open DLS(end, endprev, end, endprev, cells, vals, pxList); - * open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, pxList); - * if (end != endprev) - * { - * assert DLS(endnext, end, end, endprev, tail(cells), tail(vals), pxList); - * open DLS(endnext, _, _, _, _, _, _); - * open xLIST_ITEM(endnext, _, _, _, _); - * } - * } - * else - * { - * assert DLS(end, endprev, end, endprev, cells, vals, pxList); - * dls_first_mem(end, endprev, end, endprev, cells); - * assert pxIterator != end; - * assert index_of(end, cells) == 0; - * split(end, endprev, end, endprev, cells, vals, pxIterator, i); - * assert DLS(end, endprev, pxIterator, ?iterprev, take(i, cells), take(i, vals), pxList); - * assert DLS(pxIterator, iterprev, end, endprev, drop(i, cells), drop(i, vals), pxList); - * open DLS(pxIterator, iterprev, end, endprev, drop(i, cells), drop(i, vals), pxList); - * open xLIST_ITEM(pxIterator, _, ?iternext, iterprev, pxList); - * if (pxIterator == endprev) - * { - * open DLS(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals), pxList); - * take_take(1, i, vals); - * assert xLIST_ITEM(end, portMAX_DELAY, _, _, _); - * open xLIST_ITEM(iternext, _, _, pxIterator, _); - * } - * else - * { - * open DLS(iternext, pxIterator, end, endprev, _, _, _); - * open xLIST_ITEM(iternext, _, _, pxIterator, _); - * } - * }@*/ + if (pxIterator == end) + { + open DLS(end, endprev, end, endprev, cells, vals, pxList); + open xLIST_ITEM(end, portMAX_DELAY, ?endnext, endprev, pxList); + if (end != endprev) + { + assert DLS(endnext, end, end, endprev, tail(cells), tail(vals), pxList); + open DLS(endnext, _, _, _, _, _, _); + open xLIST_ITEM(endnext, _, _, _, _); + } + } + else + { + assert DLS(end, endprev, end, endprev, cells, vals, pxList); + dls_first_mem(end, endprev, end, endprev, cells); + assert pxIterator != end; + assert index_of(end, cells) == 0; + split(end, endprev, end, endprev, cells, vals, pxIterator, i); + assert DLS(end, endprev, pxIterator, ?iterprev, take(i, cells), take(i, vals), pxList); + assert DLS(pxIterator, iterprev, end, endprev, drop(i, cells), drop(i, vals), pxList); + open DLS(pxIterator, iterprev, end, endprev, drop(i, cells), drop(i, vals), pxList); + open xLIST_ITEM(pxIterator, _, ?iternext, iterprev, pxList); + if (pxIterator == endprev) + { + open DLS(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals), pxList); + take_take(1, i, vals); + assert xLIST_ITEM(end, portMAX_DELAY, _, _, _); + open xLIST_ITEM(iternext, _, _, pxIterator, _); + } + else + { + open DLS(iternext, pxIterator, end, endprev, _, _, _); + open xLIST_ITEM(iternext, _, _, pxIterator, _); + } + }@*/ } pxNewListItem->pxNext = pxIterator->pxNext; @@ -174,153 +174,154 @@ void vListInsert( List_t * const pxList, /*@close xLIST_ITEM(pxNewListItem, val, ?iternext, pxIterator, pxList);@*/ /*@close xLIST_ITEM(pxIterator, ?iterval, pxNewListItem, ?iterprev, pxList);@*/ - /*@ - * if( xValueOfInsertion == portMAX_DELAY ) - * { - * assert iternext == end; - * assert pxIterator == endprev; - * if (end == endprev) - * { - * close DLS(end, pxNewListItem, pxNewListItem, end, cells, vals, pxList); - * close DLS(pxNewListItem, end, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList); - * join(end, pxNewListItem, pxNewListItem, end, cells, vals, - * pxNewListItem, end, end, pxNewListItem, singleton(pxNewListItem), singleton(val)); - * close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val))); - * } - * else - * { - * close xLIST_ITEM(end, portMAX_DELAY, ?endnext, pxNewListItem, pxList); - * close DLS(pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList); - * if (endnext == endprev) - * { - * assert xLIST_ITEM(endnext, ?endnextval, pxNewListItem, end, pxList); - * close DLS(end, pxNewListItem, endnext, end, singleton(end), singleton(portMAX_DELAY), pxList); - * close DLS(endnext, end, pxNewListItem, endnext, singleton(endnext), singleton(endnextval), pxList); - * join(end, pxNewListItem, endnext, end, singleton(end), singleton(portMAX_DELAY), - * endnext, end, pxNewListItem, endnext, singleton(endnext), singleton(endnextval)); - * assert DLS(end, pxNewListItem, pxNewListItem, endnext, cells, vals, pxList); - * } - * else - * { - * assert DLS(endnext, end, endprev, ?endprevprev, ?cells_endnext_to_endprevprev, ?vals_endnext_to_endprevprev, pxList); - * assert cells_endnext_to_endprevprev == take(index_of(endprev, tail(cells)), tail(cells)); - * assert index_of(endprev, tail(cells)) == length(tail(cells)) - 1; - * assert cells_endnext_to_endprevprev == take(length(tail(cells)) - 1, tail(cells)); - * assert xLIST_ITEM(endprev, ?endprevval, pxNewListItem, endprevprev, pxList); - * close DLS(endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval), pxList); - * dls_last_mem(endnext, end, endprev, endprevprev, cells_endnext_to_endprevprev); - * dls_star_item(endnext, endprevprev, end); - * close DLS(end, pxNewListItem, endprev, endprevprev, cons(end, cells_endnext_to_endprevprev), cons(portMAX_DELAY, vals_endnext_to_endprevprev), pxList); - * join(end, pxNewListItem, endprev, endprevprev, cons(end, cells_endnext_to_endprevprev), cons(portMAX_DELAY, vals_endnext_to_endprevprev), - * endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval)); - * assert DLS(end, pxNewListItem, pxNewListItem, endprev, cells, vals, pxList); - * - * } - * join(end, pxNewListItem, pxNewListItem, endprev, cells, vals, - * pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val)); - * remove_append(pxNewListItem, cells, singleton(pxNewListItem)); - * close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val))); - * } - * } - * else - * { - * if (pxIterator == end) - * { - * if (iternext == end) - * { - * close DLS(end, pxNewListItem, pxNewListItem, end, cells, vals, pxList); - * close DLS(pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList); - * join(end, pxNewListItem, pxNewListItem, end, cells, vals, - * pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val)); - * close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val))); - * } - * else - * { - * close xLIST_ITEM(iternext, ?iternextval, _, pxNewListItem, pxList); - * if (iternext == endprev) - * { - * close DLS(iternext, pxNewListItem, end, endprev, singleton(iternext), singleton(iternextval), pxList); - * dls_last_mem(iternext, pxNewListItem, end, endprev, singleton(iternext)); - * } - * else - * { - * assert DLS(?iternextnext, iternext, end, endprev, ?cells_iternextnext_to_endprev, ?vals_iternextnext_to_endprev, pxList); - * close DLS(iternext, pxNewListItem, end, endprev, cons(iternext, cells_iternextnext_to_endprev), cons(iternextval, vals_iternextnext_to_endprev), pxList); - * dls_last_mem(iternext, pxNewListItem, end, endprev, cons(iternext, cells_iternextnext_to_endprev)); - * } - * close DLS(end, endprev, pxNewListItem, end, singleton(end), singleton(portMAX_DELAY), pxList); - * assert DLS(iternext, pxNewListItem, end, endprev, ?cells_iternext_to_endprev, ?vals_iternext_to_endprev, pxList); - * dls_star_item(iternext, endprev, pxNewListItem); - * close DLS(pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, cells_iternext_to_endprev), cons(val, vals_iternext_to_endprev), pxList); - * join(end, endprev, pxNewListItem, end, singleton(end), singleton(portMAX_DELAY), - * pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, cells_iternext_to_endprev), cons(val, vals_iternext_to_endprev)); - * close xLIST(pxList, len+1, idx, end, cons(end, cons(pxNewListItem, cells_iternext_to_endprev)), cons(portMAX_DELAY, cons(val, vals_iternext_to_endprev))); - * } - * } - * else - * { - * close xLIST_ITEM(iternext, ?iternextval, _, pxNewListItem, pxList); - * if (pxIterator == endprev) - * { - * if (iterprev == end) - * { - * close DLS(end, pxNewListItem, pxIterator, end, singleton(end), singleton(portMAX_DELAY), pxList); - * } - * else - * { - * assert DLS(_, iternext, pxIterator, iterprev, ?cells1, ?vals1, _); - * close DLS(end, pxNewListItem, pxIterator, iterprev, cons(end, cells1), cons(portMAX_DELAY, vals1), pxList); - * } - * int i = index_of(pxIterator, cells); - * assert DLS(end, pxNewListItem, pxIterator, iterprev, take(i, cells), take(i, vals), pxList); - * close DLS(pxIterator, iterprev, pxNewListItem, pxIterator, drop(i, cells), drop(i, vals), pxList); - * close DLS(pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList); - * join(end, pxNewListItem, pxIterator, iterprev, take(i, cells), take(i, vals), - * pxIterator, iterprev, pxNewListItem, pxIterator, drop(i, cells), drop(i, vals)); - * join(end, pxNewListItem, pxNewListItem, pxIterator, cells, vals, - * pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val)); - * close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val))); - * remove_append(pxNewListItem, cells, singleton(pxNewListItem)); - * } - * else - * { - * int i = index_of(pxIterator, cells); - * if (iternext == endprev) - * { - * close DLS(iternext, pxNewListItem, end, endprev, singleton(iternext), singleton(iternextval), pxList); - * } - * else - * { - * assert DLS(_, iternext, end, endprev, ?cells0, ?vals0, pxList); - * dls_star_item(end, iterprev, iternext); - * close DLS(iternext, pxNewListItem, end, endprev, tail(drop(i, cells)), tail(drop(i, vals)), pxList); - * } - * drop_drop(1, i, cells); - * drop_drop(1, i, vals); - * assert DLS(iternext, pxNewListItem, end, endprev, drop(i+1, cells), drop(i+1, vals), pxList); - * assert DLS(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals), pxList); - * dls_star_item(iternext, endprev, pxNewListItem); - * dls_last_mem(iternext, pxNewListItem, end, endprev, drop(i+1, cells)); - * close DLS(pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, drop(i+1, cells)), cons(val, drop(i+1, vals)), pxList); - * close DLS(pxIterator, iterprev, end, endprev, cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))), cons(iterval, cons(val, drop(i+1, vals))), pxList); - * join(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals), - * pxIterator, iterprev, end, endprev, cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))), cons(iterval, cons(val, drop(i+1, vals)))); - * list<struct xLIST_ITEM * >new_cells = append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells)))); - * list<TickType_t >new_vals = append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals)))); - * head_append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells)))); - * take_head(take(i, cells)); - * take_take(1, i, cells); - * assert( end == head(new_cells) ); - * head_append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals)))); - * take_head(take(i, vals)); - * take_take(1, i, vals); - * assert( portMAX_DELAY == head(new_vals) ); - * append_take_drop_n(cells, index_of(pxIterator, cells)); - * close xLIST(pxList, len+1, idx, end, append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells)))), append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals))))); - * mem_take_false(pxNewListItem, i, cells); - * remove_append(pxNewListItem, take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells)))); - * } - * } - * }@*/ + if( xValueOfInsertion == portMAX_DELAY ) + { + assert iternext == end; + assert pxIterator == endprev; + if (end == endprev) + { + close DLS(end, pxNewListItem, pxNewListItem, end, cells, vals, pxList); + close DLS(pxNewListItem, end, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList); + join(end, pxNewListItem, pxNewListItem, end, cells, vals, + pxNewListItem, end, end, pxNewListItem, singleton(pxNewListItem), singleton(val)); + close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val))); + } + else + { + close xLIST_ITEM(end, portMAX_DELAY, ?endnext, pxNewListItem, pxList); + close DLS(pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList); + if (endnext == endprev) + { + assert xLIST_ITEM(endnext, ?endnextval, pxNewListItem, end, pxList); + close DLS(end, pxNewListItem, endnext, end, singleton(end), singleton(portMAX_DELAY), pxList); + close DLS(endnext, end, pxNewListItem, endnext, singleton(endnext), singleton(endnextval), pxList); + join(end, pxNewListItem, endnext, end, singleton(end), singleton(portMAX_DELAY), + endnext, end, pxNewListItem, endnext, singleton(endnext), singleton(endnextval)); + assert DLS(end, pxNewListItem, pxNewListItem, endnext, cells, vals, pxList); + } + else + { + assert DLS(endnext, end, endprev, ?endprevprev, ?cells_endnext_to_endprevprev, ?vals_endnext_to_endprevprev, pxList); + assert cells_endnext_to_endprevprev == take(index_of(endprev, tail(cells)), tail(cells)); + assert index_of(endprev, tail(cells)) == length(tail(cells)) - 1; + assert cells_endnext_to_endprevprev == take(length(tail(cells)) - 1, tail(cells)); + assert xLIST_ITEM(endprev, ?endprevval, pxNewListItem, endprevprev, pxList); + close DLS(endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval), pxList); + dls_last_mem(endnext, end, endprev, endprevprev, cells_endnext_to_endprevprev); + dls_star_item(endnext, endprevprev, end); + close DLS(end, pxNewListItem, endprev, endprevprev, cons(end, cells_endnext_to_endprevprev), cons(portMAX_DELAY, vals_endnext_to_endprevprev), pxList); + join(end, pxNewListItem, endprev, endprevprev, cons(end, cells_endnext_to_endprevprev), cons(portMAX_DELAY, vals_endnext_to_endprevprev), + endprev, endprevprev, pxNewListItem, endprev, singleton(endprev), singleton(endprevval)); + assert DLS(end, pxNewListItem, pxNewListItem, endprev, cells, vals, pxList); + + } + join(end, pxNewListItem, pxNewListItem, endprev, cells, vals, + pxNewListItem, endprev, end, pxNewListItem, singleton(pxNewListItem), singleton(val)); + remove_append(pxNewListItem, cells, singleton(pxNewListItem)); + close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val))); + } + } + else + { + if (pxIterator == end) + { + if (iternext == end) + { + close DLS(end, pxNewListItem, pxNewListItem, end, cells, vals, pxList); + close DLS(pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList); + join(end, pxNewListItem, pxNewListItem, end, cells, vals, + pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val)); + close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val))); + } + else + { + close xLIST_ITEM(iternext, ?iternextval, _, pxNewListItem, pxList); + if (iternext == endprev) + { + close DLS(iternext, pxNewListItem, end, endprev, singleton(iternext), singleton(iternextval), pxList); + dls_last_mem(iternext, pxNewListItem, end, endprev, singleton(iternext)); + } + else + { + assert DLS(?iternextnext, iternext, end, endprev, ?cells_iternextnext_to_endprev, ?vals_iternextnext_to_endprev, pxList); + close DLS(iternext, pxNewListItem, end, endprev, cons(iternext, cells_iternextnext_to_endprev), cons(iternextval, vals_iternextnext_to_endprev), pxList); + dls_last_mem(iternext, pxNewListItem, end, endprev, cons(iternext, cells_iternextnext_to_endprev)); + } + close DLS(end, endprev, pxNewListItem, end, singleton(end), singleton(portMAX_DELAY), pxList); + assert DLS(iternext, pxNewListItem, end, endprev, ?cells_iternext_to_endprev, ?vals_iternext_to_endprev, pxList); + dls_star_item(iternext, endprev, pxNewListItem); + close DLS(pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, cells_iternext_to_endprev), cons(val, vals_iternext_to_endprev), pxList); + join(end, endprev, pxNewListItem, end, singleton(end), singleton(portMAX_DELAY), + pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, cells_iternext_to_endprev), cons(val, vals_iternext_to_endprev)); + close xLIST(pxList, len+1, idx, end, cons(end, cons(pxNewListItem, cells_iternext_to_endprev)), cons(portMAX_DELAY, cons(val, vals_iternext_to_endprev))); + } + } + else + { + close xLIST_ITEM(iternext, ?iternextval, _, pxNewListItem, pxList); + if (pxIterator == endprev) + { + if (iterprev == end) + { + close DLS(end, pxNewListItem, pxIterator, end, singleton(end), singleton(portMAX_DELAY), pxList); + } + else + { + assert DLS(_, iternext, pxIterator, iterprev, ?cells1, ?vals1, _); + close DLS(end, pxNewListItem, pxIterator, iterprev, cons(end, cells1), cons(portMAX_DELAY, vals1), pxList); + } + int i = index_of(pxIterator, cells); + assert DLS(end, pxNewListItem, pxIterator, iterprev, take(i, cells), take(i, vals), pxList); + close DLS(pxIterator, iterprev, pxNewListItem, pxIterator, drop(i, cells), drop(i, vals), pxList); + close DLS(pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val), pxList); + join(end, pxNewListItem, pxIterator, iterprev, take(i, cells), take(i, vals), + pxIterator, iterprev, pxNewListItem, pxIterator, drop(i, cells), drop(i, vals)); + join(end, pxNewListItem, pxNewListItem, pxIterator, cells, vals, + pxNewListItem, pxIterator, end, pxNewListItem, singleton(pxNewListItem), singleton(val)); + close xLIST(pxList, len+1, idx, end, append(cells, singleton(pxNewListItem)), append(vals, singleton(val))); + remove_append(pxNewListItem, cells, singleton(pxNewListItem)); + } + else + { + int i = index_of(pxIterator, cells); + if (iternext == endprev) + { + close DLS(iternext, pxNewListItem, end, endprev, singleton(iternext), singleton(iternextval), pxList); + } + else + { + assert DLS(_, iternext, end, endprev, ?cells0, ?vals0, pxList); + dls_star_item(end, iterprev, iternext); + close DLS(iternext, pxNewListItem, end, endprev, tail(drop(i, cells)), tail(drop(i, vals)), pxList); + } + drop_drop(1, i, cells); + drop_drop(1, i, vals); + assert DLS(iternext, pxNewListItem, end, endprev, drop(i+1, cells), drop(i+1, vals), pxList); + assert DLS(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals), pxList); + dls_star_item(iternext, endprev, pxNewListItem); + dls_last_mem(iternext, pxNewListItem, end, endprev, drop(i+1, cells)); + close DLS(pxNewListItem, pxIterator, end, endprev, cons(pxNewListItem, drop(i+1, cells)), cons(val, drop(i+1, vals)), pxList); + close DLS(pxIterator, iterprev, end, endprev, cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))), cons(iterval, cons(val, drop(i+1, vals))), pxList); + join(end, endprev, pxIterator, iterprev, take(i, cells), take(i, vals), + pxIterator, iterprev, end, endprev, cons(pxIterator, cons(pxNewListItem, drop(i+1, cells))), cons(iterval, cons(val, drop(i+1, vals)))); + list<struct xLIST_ITEM * >new_cells = append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells)))); + list<TickType_t >new_vals = append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals)))); + head_append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells)))); + take_head(take(i, cells)); + take_take(1, i, cells); + assert( end == head(new_cells) ); + head_append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals)))); + take_head(take(i, vals)); + take_take(1, i, vals); + assert( portMAX_DELAY == head(new_vals) ); + append_take_drop_n(cells, index_of(pxIterator, cells)); + close xLIST(pxList, len+1, idx, end, append(take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells)))), append(take(i, vals), cons(iterval, cons(val, drop(i+1, vals))))); + mem_take_false(pxNewListItem, i, cells); + remove_append(pxNewListItem, take(i, cells), cons(pxIterator, cons(pxNewListItem, drop(i+1, cells)))); + } + } + }@*/ } + +/* *INDENT-ON* */ |