#ifndef X_LIST_JOINT_H
#include <vcc.h>

/* +-----------------------------------------------------------------------------------------------------------+
   | MISCELLANEOUS FLAGS                                                                                       |
   +-----------------------------------------------------------------------------------------------------------+
*/
/* UnCOmment SANITY_CHECK to make prover to prove FALSE at the end of function calls.  This will allow us to make
	sure that none of our assumption in the function body leads to false. On enabling this flag all the function 
	should fail with '_(ensures \false)' fails at the post-condition
	"Post condition '\false' did not verify"
*/
//#define SANITY_CHECK() _(ensures \false)
//OR IN CASE YOU DO NOT WANT A SANITY CHECK COMMENT ABOVE AND UNCOMMENT BELOW
#define SANITY_CHECK() 



/* Uncomment the following to make sure that the pre-conditions are reachable in other words !pre-condition ==> false
	On enabling this flag all the function should fail with error assertion failed _(assert PRE_CONDITION_SANITY_CHECK) in the function
	body
*/
//#define CHECK_PRECONDITION(); _(assert \false)
 // OR IN CASE YOU DONT WANT TO CHECK FOR PRE-CONDITION SANITY UNCOMMENT THE BELOW DECLARATION
#define CHECK_PRECONDITION(); 


#define NULL 0

#define ZERO (0u)

struct xLIST_ITEM;
struct xListMap;

_(ghost enum xListType {FIFO,PQ,UNORDERED} )

/*	Following variable represents the 
	maximum numeric value allowed by the type
*/
unsigned maxNumVal;
/*	Following variable represents the 
	maximum priority of a task
*/
ghost unsigned maxPrio;



_(dynamic_owns)
typedef struct tskTCB{
	struct xLIST_ITEM *pvGenericListItem;		
	/*  List item used to place the owner 
		task in ready or delayed/suspended lists. 
	*/
	struct xLIST_ITEM *pvEventListItem;		
	/*	List item used to place the owner task in 
		event lists. 
	*/
	unsigned uxPriority;			
	/*	The priority of the task where 0 is the 
		lowest priority. 
	*/

	_(invariant pvGenericListItem != pvEventListItem )
	/*	List items are distinct. */
}TCB;


/* +-----------------------------------------------------------------------------------------------------------+
   | The struct xListItem. This item is unchnaged with the exception of 'ownersPriority' which is included to  |
   | easify the model and invariant. The field 'pvOwner' is specified to be type 'TCB' ( void used in original |
   | code, this is done because VCC handles strongly typed code well. This is a safe assumption and a nice way |
   | to filter out any wrong assignment to this field.                                                          |
   +-----------------------------------------------------------------------------------------------------------+
*/

_(dynamic_owns)
typedef struct xLIST_ITEM{
	
	/* Can be the priority of the task or time to awake in delayed lists */
	unsigned xItemValue;	
	
	/*	Pointer to the next xListItem in the list. */
	struct xLIST_ITEM * pxNext;	
	
	/*  Pointer to the previous xListItem in the list.*/ 
	struct xLIST_ITEM * pxPrevious;
	
	/*	Pointer to the object (normally a TCB) that owns the list item */
	TCB * pvOwner;							
	
	/*	pointer to the list in which it is present*/
	struct xListMap *pvContainer;   
	
	/* Extra field to represent the priority of the owner.
	   Without this, invariants on this field is not possible 
	   in the list because of ownership issue, note that at 
	   the same time two list items of a task can be 
	   in two different lists and hence neither can own the 
	   owner task 
	*/
	unsigned ownersPriority;	
	
	/*	+----------------------------------------------------------------------------+
		| INVARIANTS ON xLIST_ITEM                                                   |
		| These invariants should hold for each object of type xListItem in valid    |
		| state                                                                      |
		+----------------------------------------------------------------------------+

	/*  INV-ITEM-01	:	The value of xItemValue should not exeed the BOUND. The BOUND variable define the limit of integer in FreeRTOS
						This is the maximum amount of time a task can be made to sleep. In ideal conditions this is set according to the
						width of integer for the system. The priority value of 'xItemValue' is within the bound
	*/
	_(invariant xItemValue<=maxNumVal )
	

	/* --- END OF STRUCT xListItem --- */
} xListItem;


/*	+--------------------------------------------------------------------------------------------------------------------+
	|	xListMap : A version for xList based on integer maps. This maps is contrained to simulate an array of xListItems |
	|	Map provides a very easy interface to verify 'xList as array of xListItems'. It provides bulk update to all map- |
	|	pings using 'lambda' statement which otherwise will be very hard to prove in array implementation which would	 |
	|	require 'hard-to-prove' loops and memory access. The map is treated as a primitive variable so VCC does not imp- |
	|	ose any contraint on map like memory access, updation of mappings etc.                                           |
	+--------------------------------------------------------------------------------------------------------------------+
*/

_(dynamic_owns)
typedef struct xListMap{

	
	/*	Following map models a sequence of nodes (each node represent a task in the system), 
		the value for a given unsigned int 'i' gives the address of the node modelling the ith 
		task in the sequence 
	*/
	_(ghost xListItem *list[unsigned] )

	/*	EXAMPLE INSTANCE OF 'list'
		pointer 	-->			|	&item_1	|	&item_2	|	$item_3	|	....	|	...		|	$items_length	|
		---------------------------------------------------------------------------------------------------------
		index		-->			|	   0	|	    1   |	   2    |	....	|	....	|	    length - 1	|
	
		It means that at index '0' the value stored is pointer to an item (say 'item1'), at index '1' the value stored
		is pointer to another 'item' and so on upto index 'length - 1' Thus all total 'length' number of pointers.

		We extract the requirements from the Z Model and port them to here in VCC on top of this structure. The invariants
		are stated in the next section. To make the life easy for Specifications and Developers we have added an additional
		reverse map which associate items with their position in the above list/array/map
	*/

	/*	+---------------------------------------------------------------------------------------------------------------+
		|	Housekeeping variables and addition added to provide correct model for xListMap. These variable are used to |
		|	specify model correctly.																				    |
		+---------------------------------------------------------------------------------------------------------------+
	*/

	/*	The following map support easy specification of some of the function contract.
		The value of the following map for a given pointer (p) to xListItem gives the index 
		(0<=index<length) of p in the list, when p is present in list. If p is not in list, 
		the value should be 'length'. 
	*/
	_(ghost unsigned position[xListItem *] )
	
	/*	The following field shows the type (PQ or FIFO) of the list. We need to specify properties 
		which are true only on lists of a given 'type'
	*/
	_(ghost enum xListType type )

	/*	The following field models the length of the sequence 
	*/
	unsigned length;
	/*	Following ghost field models the priority 
		of tasks (unique) in ready queue. The value 
		is the priority of any task in this queue. 
		This enable easy specification.
	*/

	/*	
		+-----------------------------------------------------------------------------------------------+
	 	|	INVARIANTS ON XLISTMAP																		|
	 	|	Ownership Model: For VCC the ownership model is used to check for write access due to its   |
		|	multithread nature. The valid state of A can depend on state of object B only if B is in    |
		|	ownership domain of A. VCC constraint that an object can be modified only if it is owned by |
		|	current thread. Hence if we were to modify B then we have to first take it out of ownership |
		|	domain of A. For xListMap state of an instance of xListMap depends on all the items that are|
		|	contained in the list. So we define the 'ownership' domain of 'xListMap' as the set of the  |
		|	xListItem contained in the xListMap                                                         |
	 	+-----------------------------------------------------------------------------------------------+
	 */


	/* INV-1:	length never exceeds maxNumVal */
	_(ghost unsigned priority )
	
	/* INV-2:	priority of each task is within the bound */
	_(invariant length <= maxNumVal)
	
	/* INV-3:	item value of each node is within the bound */
	_(invariant \forall unsigned i; (i < length) ==> ( \mine(list[i]) && (list[i]->xItemValue <= maxNumVal) ) )

	/* INV-4:	Tasks in the list are distinct */
	_(invariant \forall unsigned i,j;( (i < length) && (j < length) && (i != j) && \mine(list[i])  && \mine(list[j]) ) 
						==> ( list[i]->pvOwner != list[j]->pvOwner) 
	)

	/* INV-5:	Valid list elements are owned by this : to support INV-2,INV-3 and INV-4 */
	_(invariant \forall unsigned i; (i < length) ==> ( (list[i] != NULL) && \mine(list[i]) ) )
	
	/* INV-6a:	position is consistent with list	*/
	_(invariant \forall xListItem *xli; (\mine(xli) && (xli != &xListEnd)) ==> ( (position[xli] < length) && (list[position[xli]] == xli) ) )
	
	/* INV-6b:	position is consistent with list. Follows from the above. But explicitly saying thhis helps the prover */
	_(invariant \forall unsigned i; (i < length) ==> ( \mine(list[i]) && (position[list[i]] == i) ))
	
	/* INV-6c:	For all invalid list item modes, value under the map position is maxNumVal */
	_(invariant \forall xListItem *xli; ( !\mine(xli) ) ==> (position[xli] == maxNumVal) ) 
	
	/* INV-7:	All invalid elements in the sequence contain null pointer */
	_(invariant \forall unsigned i; (i >= length) ==> (list[i] == NULL) )

	/* INV-FIFO:	All tasks in a FIFO list are of the same priority */
	_(invariant (type == FIFO) ==> 
			(
				\forall unsigned i; (i < length) ==> ( \mine(list[i])  && (list[i]->ownersPriority == priority) ) 
					
			)
	)
	
	/* INV-PQ:	All tasks in a PQ list are arranged in the nondecreasing order of priority values */
	_(invariant (type == PQ) ==>	
			(	
				\forall unsigned i , j; ((j < length) && \mine(list[i]) && \mine(list[j]) && (i < j) ) 
						==> ( list[i]->xItemValue <= list[j]->xItemValue ) 
			) 
	)

	/* INV-added:	All valid items are contained in the list */
	_(invariant \forall xListItem *xli; \mine(xli) ==> (xli->pvContainer == \this) )


	/* INV-added:	For all valid items, the value of ownersPriority is within the bound */
	_(invariant \forall xListItem *xli; \mine(xli) ==> (xli->ownersPriority <= maxPrio) )


	/*INV-added:For all valid list nodes 
				th eitem value is within the bound
	*/
	_(invariant \forall xListItem *xli; ( \mine(xli) ) ==> 
					( xli->xItemValue <= maxNumVal ) 
	 )

	/*INV-added: This structure owns 'maxNumVal' */
	_( invariant \mine( \embedding( &maxNumVal ) ) )

	/*INV-added: This structure owns 'maxPrio' */
	_( invariant \mine( \embedding( &maxPrio ) ) )

	 /* --- END OF STRUCT xListMap --- */







	/*-------------------------------------------------------------------------------------------------------------*/
	/*	ORIGINAL XLIST DEFINITIONS	*/
	/*-------------------------------------------------------------------------------------------------------------*/
	/*NOTE : The type has been changed for verification purpose ONLY*/
	unsigned uxNumberOfItems;
	xListItem *pxIndex;
	xListItem xListEnd;


	/* VERIFICATION DEFINITIONS */
	/*********************************************************************************************************************/
	/*	DEFINING THE OWNERSHIP MODEL FOR VCC. WE WOULD MAKE THE XLIST OWN ALL THE XLIST ITEMS. THIS WAAY XLIST IS FREE TO 
		STATE THE DESIRED PROPERTIES OVER THEM. 
	*/
	/*********************************************************************************************************************/
	/*	MODEL FOR XLIST. MAP INDEX WILL MAKE SURE THAT THE XLIST STRUCTURE IS INDEED A DOUBLY LINKED xList STRUCTURE. THE 
		MAP WILL SERVE AS A INDEXER FOR ALL THE xList ITEMS
	*  Invariants for ensuring a valid xList as a Doubly Linked List.These invariants are over 
	*  xListItems as well as index. Using index is the simplest way to convey the order of 
	*  the items to be synchronous.
	*
	*  'owns' set is the set of objects about which a xList struct can say something about.
	*  If we want to say something about any xListItem then the item must be owned by xList
	*
	*
	*  NOTE: Hereafter we consider 'I' as the 'instance' of the xList that we are talking 
	*  about.
	*  
	*  These invariants will define what node to be included into the owns set. In simple 
	*  words we define that any node reachable from xListEnd OR pxIndex is in owns set. First
	*  we say that 'xListEnd and pxIndex are explicitly in owns set' then secondly we say
	*  that whichever node we can get by following pxNext or pxPrevious is in owns set. 
	*  Thus,
	*  \forall xListItem *p ; 
			(p is reachable through xListEnd or pxIndex) ==> (p in \this->\owns)
	*  
	   INVARIANTS TO STATE OWNS SET (DLL-OD)[Owns Definition]:
	*/
	/********************************************************************************************************************/

	/*INV-LI-01		'pxIndex' always points to something */
	_(invariant ( pxIndex != NULL))
	
	/*INV-LI-02		pxIndex is always owned */
	_(invariant   \mine(pxIndex) && \mine(&xListEnd))

	/*INV-LI-03		If a node 'N' is owned then every node that can be reached through 'pxNext' is owned */
	_(invariant \forall xListItem *p; \mine(p) ==> ( \mine(p->pxNext) && ( p->pxNext->pxPrevious == p) ) )

	/*INV-LI-04		If a node 'N' is owned then every node that can be reached through 'pxPrevious' is owned */
	_(invariant \forall xListItem *p; \mine(p) ==> ( \mine(p->pxPrevious) && ( p->pxPrevious->pxNext == p) ))

	/*INV-LI-05		If I own a node 'N' then 'N->pvContainer' is me */
	_(invariant \forall xListItem *p ; \mine(p) ==> ( p->pvContainer == \this) )

	/*INV-LI-06		For all item except xListEnd the type matches the list node type */
	_(invariant \forall xListItem *p ; ( \mine(p) && ( p != (&xListEnd))) ==> (  p->pvOwner != NULL ) )
	
	/*INV-LI-07		uxNumberOfItems is always >= 0 and less than MACHINE_OVERFLOW */
	_(invariant (uxNumberOfItems >= 0) && (uxNumberOfItems <= maxNumVal))

	/*INV-LI-09		xListEnd Has only one item value */
	_(invariant xListEnd.xItemValue == maxNumVal)
	
	/*INV-LI-09		The elements values are in order  for a PQ */
	_(invariant (type == PQ) ==>
			(\forall xListItem *p ; ( \mine(p) && \mine(p->pxNext) && ( p != (&xListEnd))) ==> 
					( p->xItemValue <= p->pxNext->xItemValue )
			)
	)

	/*	The definition for the owns set and all the fields for xList as a Doubly Linked List
		are done by here 
	*/
	/*------------------------------------------------------------------------------------*/
	/*	CONCRETE MODEL FOR XLIST USING MAP 'index'

		This map 'index' will correctly specify the DLL structure of xList. Hence this map 
		represent the linked model of DLL with xListEnd. It is required for VCC to correctly interpret 
		xList as a DLL.

		If the invariants of the 'index' map hold then that will mean that the xList is a a 
		valid DLL. Hence, this will verify the xList as DLL.

		Example: Lets consider a xList instance 
			A->B->C->D->.....->X->Y->Z->xListEnd->(points to A)

		We define index as 
			|0 | 1| 2| 3|...|...|L-3|L-2|L-1| L		  |
			-------------------------------------------
			|&A|&B|&C|&D|...|...|&X |&Y |&Z |&xListEnd|


		For any item 'A' if index is 'i' then for item 'A->pxNext' the index will be 'i+1'
		This goes on till xListEnd. Hence 'xListEnd.pxNext' will always have index '0' and
		xListEnd will have index 'uxNumberOfItems'. This make sure that there is only one 
		cycle in Linked List. Notable point is that this 'index' map is not present in the
		contracts of the 'xList'. We treat this index map as 'ghost' variable in concrete
		xList implementation.
	*/
	/*------------------------------------------------------------------------------------*/
	
	_(ghost unsigned index[struct xListItem *])
	/*
		This map is used to map a unique index to evry node. The index has a range
		[0,uxNumberOfItems]. This ensures that the number of items in the xList is 
		valid and the order is preserved on checking.
	*/

	/*INV-LI-10		xListEnd is at last only */
	_(invariant index[&xListEnd] == uxNumberOfItems)
	
	/*INV-LI-11		Node Next to xListEnd is at ZERO */
	_(invariant index[(&xListEnd)->pxNext] == 0 )

	/*INV-LI-12		The indices are consecutive wrt to pxNext 
					NOTE : This invariant will ensure that there are no cycles in the 'owned node set' */
	_(invariant \forall xListItem *p;
			( \mine(p) && \mine(p->pxNext) && ( index[p] != uxNumberOfItems ) ) ==> ( (index[p] + 1) == index[p->pxNext] )
	) 
	
	/*INV-LI-13		The indices are consecutive wrt to pxPrevious
	*				NOTE : This invariant will ensure that there are no cycles in the 'owned node set'. */
	_(invariant \forall xListItem *p;
			( \mine(p) && \mine(p->pxPrevious)&& (index[p] != 0)) ==> ( (index[p]- 1) == (index[p->pxPrevious]))
	) 

	/*INV-LI-14		There are no index greater than size */
    //_(invariant \forall xListItem *p ; \mine(p) ==> ( index[p] >= 0 ) )

	/*INV-LI-15		There are no index greater than size */
	_(invariant \forall xListItem *p ; \mine(p) ==> ( index[p] <= uxNumberOfItems))

	/*INV-LI-16		Each element in the list is only contained once */
    _(invariant \forall xListItem *p1 , *p2 ; ( \mine(p1) && \mine(p2) && (p1 != p2) ) ==> ( index[p1] != index[p2]) )

	/*
	*
	* # DEFINITION OF 'index' ENDS HERE. #
	*
	*/




	/*-------------------------------------------------------------------------------------------------------------*/
	/*	GLUING INVARIANTS STARTS HERE	
		These invariants combine the two data structures 'list' map and 'xList' dll. 
	*/
	/*-------------------------------------------------------------------------------------------------------------*/

	/*INV-GI-01	'length' of map and 'uxNumberOfItems' of xlist are always same */
	_(invariant length == uxNumberOfItems)

	/*INV-GI-02	'xListEnd is a "dormant" item for 'xListMap'. Due to which we assign the last unused position (BOUND)
				to it
	*/
	_(invariant position[&xListEnd] == maxNumVal)

	/*INV-GI-03	None of the valid locations points to xListEnd */
	_(invariant \forall unsigned i; (i < length) ==> (list[ i ] != &xListEnd ))

	/*INV-GI-04 [FIFO] pxIndex is at last only if its not xListEnd */
	_(invariant ((type == FIFO) && (length > ZERO) && (pxIndex != (&xListEnd)) && \mine(pxIndex)) ==> ( list[length - 1] == pxIndex))


	/*INV-GI-05 [FIFO] If pxIndex = xListEnd then we require that the sequence end at previous of xListEnd */
	_(invariant ((type == FIFO) && (length > ZERO) && (pxIndex == (&xListEnd))) ==> list[length - 1] == xListEnd.pxPrevious)


	/*INV-GI-06	[FIFO] If pxNext of pxIndex is NOT xListEnd then pxNExt is at index 0 */
	_(invariant ((type == FIFO) && (length > ZERO ) && (pxIndex->pxNext != (&xListEnd) ) ==> (list[ZERO] == pxIndex->pxNext )))

	
	/*INV-GI-07	[FIFO] If pxIndex is pxPrevious to xListEnd then we say that xListEnd.pxNext is at 0 */
	_(invariant ((type == FIFO) && (length > ZERO ) && (pxIndex->pxNext == (&xListEnd)) ==> (list[ZERO] == xListEnd.pxNext)))

	
	/*INV-GI-08	[FIFO] If for any item if the pxNext is not xListEnd then index of pxNext is plus ONE */
	_(invariant (type == FIFO) ==> ( \forall unsigned i ; 
		( (i < (length -1)) && (list[i]->pxNext != (&xListEnd)) && \mine(list[i]) && \mine(list[i]->pxNext))
			==> (list[i + 1] == list[i]->pxNext))
	)

	/*INV-GI-09	[FIFO] If for any item if the pxNext is xListEnd then index of xListEnd.pxNext is plus ONE */
	_(invariant (type == FIFO) ==> ( \forall unsigned i ; 
		( (i < (length - 1)) && (list[i]->pxNext == (&xListEnd)) && \mine(list[i]) && \mine((&xListEnd)->pxNext))
			==> (list[i+1] == (&xListEnd)->pxNext))
	)

	/*INV-GI-10	[FIFO] If for any item if the pxPrevious is xListEnd then its index of pxPrevious is minus ONE */
	_(invariant (type == FIFO) ==> (\forall unsigned i ; 
		( (i > ZERO) && (i < length) && (list[i]->pxPrevious != (&xListEnd)) && \mine(list[i]) && \mine(list[i]->pxPrevious))
			==> (list[i]->pxPrevious == list[i-1]))
	)

	/*INV-GI-11	[FIFO] If for any item if the pxPrevious is xListEnd then its index of xListEnd.pxPrevious is minus ONE */
	_(invariant (type == FIFO) ==> (\forall unsigned i ; 
		( (i > ZERO) && (i < length) && (length > ZERO) && (list[i]->pxPrevious == (&xListEnd))	&& \mine(list[i]) && \mine((&xListEnd)->pxPrevious))
			==> ((&xListEnd)->pxPrevious == list[i-1]))
	)
	
	/*-----------------------------------------------------------------------------------
	* Invariants for list when xList is used as a PQ
	-------------------------------------------------------------------------------------*/

	/*INV-GI-12  [PQ] If list is not empty then last item is previous to the xListEnd */
	_(invariant ((type == PQ) && (length > ZERO) ) ==> list[length - 1] == ((&xListEnd)->pxPrevious))
	
	/*INV-GI-12 [PQ] If list is not empty then last item is next to the xListEnd */
	_(invariant ((type == PQ) && (length > ZERO) ) ==> list[ZERO] == ((&xListEnd)->pxNext))

	/*INV-GI-13 [PQ] Every element and its next is synchronous in the array */
	_(invariant (type == PQ) ==> 
			(\forall unsigned i ; (((i < (length - 1)) && \mine(list[i]) && \mine(list[i]->pxNext) )
					==> (list[i + 1] == list[i]->pxNext))
			)
	)
	/*-----------------------------------------------------------------------------------------------------------------------------*/
	/* Gluing Invariants for list END here */
	/*-----------------------------------------------------------------------------------------------------------------------------*/
	

	/* All items in 'owns' are xListItem or TCB */
	_(invariant \forall \object o ; (o \in \this->\owns) ==> (o \is xListItem))

} xMap;



void listInitialiseItem(xListItem *li)
	_(requires \wrapped(li) )
	_(writes li )
	_(ensures li->pvContainer==NULL )
//////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli != li ) ==>
					( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////
	SANITY_CHECK()
	;


void setItemOwner(xListItem *li, TCB *task)
	_(requires \wrapped(li) )
	_(requires li->pvContainer==NULL )
	_(requires li->pvOwner==NULL )
	_(requires \wrapped(task) )
	_(writes li )
	_(writes task)
	_(ensures \wrapped(li) )
	_(ensures li->pvOwner==task )
	_(ensures li->ownersPriority == task->uxPriority )
//////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; ( xli != li ) ==>
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; ( xli != li ) ==>
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; ( xli != li ) ==>
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////
	SANITY_CHECK()
	;

void setItemValue(xListItem *li, unsigned value)
	_(requires \wrapped(li) )
	_(requires li->pvContainer==NULL )
	_(requires value<=maxNumVal )
	_(writes li )
	_(ensures \wrapped(li) )
	_(ensures li->xItemValue==value )
///////////////////////////////////////////////////////
	//_(ensures \forall xListItem *xli; 
	//			( xli == \old(xli) ) 
	 //) #ANIRUDH: USELESS CLAUSE DELETE IT
	_(ensures \forall xListItem *xli; ( xli != li ) ==>
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
///////////////////////////////////////////////////////
	SANITY_CHECK()
	;

unsigned getItemValue(xListItem *li)
	_(requires \wrapped(li) )
	_(ensures \result==li->xItemValue )
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; ( xli != li ) ==>
				( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////( xList != L ) ==> ( task != tcb ) ==>
	SANITY_CHECK()
	;


unsigned listIsEmpty(xMap *xList)
	_(requires \wrapped(xList) )
	_(ensures \result <==> xList->length==0 )
	_(ensures \wrapped(xList) )
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////( xList != L ) ==> ( task != tcb ) ==>
	SANITY_CHECK()
	;

unsigned currentLength(xMap *xList)
	_(requires \wrapped(xList) )
	_(ensures \result == xList->length )
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////( xList != L ) ==> ( task != tcb ) ==>
	SANITY_CHECK()
	;



TCB *getOwnerOfFirstEntry(xMap *xList)
	_(requires \wrapped(xList) )
	_(requires xList->type!=PQ )
	/*	Because this function is only for the FIFO queue*/
	_(requires xList->length>0 )
	_(ensures \result==xList->list[0]->pvOwner )
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////
	SANITY_CHECK()
	;


void rotateLeft(xMap *xList)
	_(requires \wrapped(xList) )
	_(requires xList->type!=PQ )
	/*	Because this function is only for the FIFO queue
		and it cannot restore the order of elements for PQ 
	*/
	_(requires ( xList->type==FIFO ) ==> 
		(\forall unsigned i; (i<xList->length) ==> 
					(	xList->list[i]->pvOwner->uxPriority	==	
						xList->priority 
					) 
		) 		
	 )
	_(requires xList->length>0 )
	_(writes xList)
	_(ensures \wrapped(xList) )
	_(ensures	xList->list[xList->length-1] ==
				\old(xList->list[0]) 
	 )
	_(ensures \forall  unsigned i; 
		( i < xList->length-1 ) ==> 
			( xList->list[i] == \old(xList->list[i+1]) ) 
	 ) 
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; ( xList != L ) ==> 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
		( xList != L ) ==> 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////
	SANITY_CHECK()
	;


TCB* getOwnerOfNextEntry(xMap *xList)
	_(requires \wrapped(xList) )
	_(requires xList->type!=PQ )
	/*	Because this function is only for the FIFO queue and it cannot restore the order of elements for PQ */
	_(requires ( xList->type==FIFO ) ==> 
		(\forall unsigned i; (i<xList->length) ==> 
					(	xList->list[i]->pvOwner->uxPriority	==	
						xList->priority 
					) 
		) 		
	 )
	_(requires xList->length > ZERO)
	_(writes xList)
	_(ensures \wrapped(xList) )
	_(ensures \result==\old(xList->list[1]->pvOwner) )
	_(ensures	xList->list[xList->length-1] ==
				\old(xList->list[0]) 
	 )
	_(ensures \forall  unsigned i; 
		( i < xList->length-1 ) ==> 
			( xList->list[i] == \old(xList->list[i+1]) ) 
	 ) 
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	//_(ensures \forall xListItem *xli; 
	//			( xli->pxNext == \old(xli->pxNext) ) 
	 //)
	//_(ensures \forall xListItem *xli; 
	//			( xli->pxPrevious == \old(xli->pxPrevious) ) 
	// ) #ANIRUDH NOT REQUIRED FOR xMap
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; ( xList != L ) ==> 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
		( xList != L ) ==> 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////
	SANITY_CHECK()
	;


TCB *getOwnerOfHeadEntry(xMap *xList)
	_(requires \wrapped(xList) )
	_(requires xList->length>0 )
	_(requires xList->list[0]->pvOwner->pvGenericListItem->
				ownersPriority <= maxPrio )
	_(ensures \result==xList->list[0]->pvOwner )
	_(ensures 
		\result->pvGenericListItem->ownersPriority <= maxPrio 
	 )
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; L->type==\old(L->type) )
	_(ensures \forall xMap  *L ; 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
//////////////////////////////////////////////////////( xList != L ) ==> ( task != tcb ) ==>
	SANITY_CHECK()
	;

_(pure) unsigned containedWithin( xMap *xList, xListItem *li )
	_(requires \wrapped(xList) )
	_(requires \thread_local(li) ) 
	_(reads xList,li )

	_(ensures \result == (li \in xList->\owns))

	SANITY_CHECK()
	;

void listInitialise(xMap *xList _(ghost enum xListType type) )
	_(requires \mutable(xList) )
	_(requires \wrapped(&(xList->xListEnd)) )

	_(requires xList->length == 0 )
	
	_(writes \span(xList) )
	_(writes \span(&(xList->xListEnd)))

	_(ensures \wrapped(xList) )
	_(ensures xList->length == 0) 
	
	//_(ensures xList->\owns=={} ) #ANIRUDH: NOT REQUIRED!!
	///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxNext == \old(xli->pxNext) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pxPrevious == \old(xli->pxPrevious) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; 
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; ( xList != L ) ==> 
								L->type==\old(L->type) 
	 )
	_(ensures \forall xMap  *L ; ( xList != L ) ==>
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
		( xList != L ) ==>
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
///////////////////////////////////////////////////////
	SANITY_CHECK()
	;

void listInsertEnd(xMap *xList, xListItem *li)
	_(requires \wrapped(xList))
	_(requires xList->type != PQ ) ///* This function cannot restore the order of elements for PQ */	
	_(requires ( xList->type == FIFO ) ==> (li->ownersPriority == xList->priority) )
	_(requires \wrapped(li))
	_(requires li->ownersPriority <= maxPrio )
	_(requires \forall unsigned i; (i < xList->length) ==> (xList->list[i]->pvOwner != li->pvOwner))
	_(requires (xList->type == FIFO) ==>
		(\forall unsigned i; (i < xList->length) ==> 
				(xList->list[i]->pvOwner->uxPriority == li->pvOwner->uxPriority) 
		) 
	 )
	_(requires xList->length < maxNumVal )
	_(requires li->pvOwner != NULL) //#ANIRUDH: Please add to the model

	_(writes xList )
	_(writes li )
	
	_(ensures li->pvContainer == xList)
	_(ensures \forall unsigned i; (i < \old(xList->length)) ==> (xList->list[i] == \old(xList->list[i])) )
	_(ensures xList->list[\old(xList->length)] == li)
	_(ensures xList->length == \old(xList->length+1))
	_(ensures li \in xList->\owns )
	_(ensures \wrapped(xList) )
	
	
	_(ensures \forall xListItem *xli; xli->xItemValue == \old(xli->xItemValue))
	_(ensures \forall xListItem *xli; xli->pvOwner==\old(xli->pvOwner)) 
	_(ensures \forall xListItem *xli; (xli != li) ==> (xli->pvContainer == \old(xli->pvContainer)) )
	//_(ensures \forall xListItem *xli; xli->pxNext == \old(xli->pxNext)) #ANIRUDH
	//WRONG! NOT REQUIRED FOR XMAP AS WE ARE NOT MODELLING pxNext or pxPrevious in the XMAP; Are we????
	//_(ensures \forall xListItem *xli; xli->pxPrevious == \old(xli->pxPrevious)) #ANIRUDH
	//WRONG! NOT REQUIRED FOR XMAP AS WE ARE NOT MODELLING pxNext or pxPrevious in the XMAP; Are we????

	_(ensures \forall xListItem *xli; xli->ownersPriority == \old(xli->ownersPriority))
	_(ensures \forall xListItem *xli; xli->pvOwner->uxPriority == \old(xli->pvOwner->uxPriority)) 
	
	_(ensures \forall TCB *tcb; tcb->pvGenericListItem == \old(tcb->pvGenericListItem))
	_(ensures \forall TCB *tcb;	tcb->pvEventListItem == \old(tcb->pvEventListItem))
	_(ensures \forall TCB *tcb; tcb->uxPriority == \old(tcb->uxPriority))
	
	_(ensures \forall xMap  *L; L->type==\old(L->type))
	_(ensures \forall xMap  *L; (xList != L) ==> (L->length  == \old(L->length)))
	_(ensures \forall xMap  *L; (L->priority  == \old(L->priority)))
	_(ensures \forall xMap  *L; (xList != L) ==>
			(
				\forall unsigned i; ( i<L->length ) ==> (L->list[i] == \old(L->list[i]))
			)
	 )
	_(ensures \forall xMap  *L;
			(
				\forall  xListItem *xli; (xList != L) ==> (L->position[xli] == \old(L->position[xli])) 
			)
	)
	_(ensures \forall xMap  *L;
			(
				\forall  xListItem *xli; (xList != L) ==> (L->position[xli] == \old(L->position[xli])) 
			)
	)
	//#ANIRUDH: Alternative is _(ensures xList->position[li] == \old(xList->length))
	_(ensures xList->position[li] == xList->length -1)
	
	_(ensures \forall xListItem *xli; (	(xli != li) && (xli \in xList->\owns) ) ==> 
			(xList->position[ xli ] == \old(xList->position[xli]))
	 )
	
	SANITY_CHECK();


void listInsert(xMap *xList, xListItem *li)

	_(requires li->pvOwner != NULL) //#ANIRUDH: NEEDS TO BE ADDED

	_(requires \wrapped(xList) )
	_(requires \wrapped(li) )
	_(requires li->ownersPriority <= maxPrio )
	_(requires \forall unsigned i; 
		( i<xList->length ) ==> 
			 (xList->list[i]->pvOwner!=li->pvOwner ) 
	 )
	// This operation is only for priority queues
	_(requires ( xList->type== PQ ) )
	_(requires xList->length<maxNumVal )
	_(writes xList )
	_(writes li )
	_(ensures xList->length==\old(xList->length+1) )
	_(ensures xList->list[xList->position[li]] == li )
	_(ensures \forall unsigned i;
		(	( i < xList->length ) &&
			( i < xList->position[li] )
		) ==> ( xList->list[i] == \old(xList->list[i]) )
	 )
	_(ensures ( xList->list[xList->position[li]] == li ) )
	_(ensures \forall unsigned i;
		(	( i < xList->length ) &&
			( i > xList->position[li] )
		) ==> ( xList->list[i] == \old(xList->list[i-1]) )
	 )
	_(ensures li->pvContainer==xList )
	_(ensures li \in xList->\owns )
	_(ensures \wrapped(xList) )
///////////////////////////////////////////////////////
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	//_(ensures \forall xListItem *xli; 
	//			( xli->pxNext == \old(xli->pxNext) ) 
	// )
	//_(ensures \forall xListItem *xli; 
	//			( xli->pxPrevious == \old(xli->pxPrevious) ) 
	// )
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; ( xli != li ) ==>
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; 
								L->type==\old(L->type) 
	 )
	_(ensures \forall xMap  *L ; ( xList != L ) ==> 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; ( xList != L ) ==> 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
		( xList != L ) ==> 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
	_(ensures xList->position[li] < xList->length )
	_(ensures \forall xListItem *xli; 
		(	( xli != li ) &&
			( xli \in xList->\owns ) &&
			( xList->position[xli] < xList->position[li] )
		) ==> ( xList->position[ xli ] == \old(xList->position[ xli ]) )
	 )
	_(ensures \forall xListItem *xli; 
		(	( xli != li ) &&
			( xli \in xList->\owns ) &&
			( xList->position[xli] > xList->position[li] ) &&
			( xList->position[xli] < xList->length )
		) ==> ( xList->position[ xli ] == ( \old(xList->position[ xli ]) + 1 ) )
	 )

	SANITY_CHECK()
	;

void listRemove(xMap *xList, xListItem *li)
	_(requires \wrapped(xList) )
	//_(requires li \in xList->\owns ) #ANIRUDH: This should be changed to position OR index
	_(requires xList->position[ li ] < xList->length)
	_(writes xList )
	_(ensures \wrapped(xList) )
	_(ensures xList->length == \old(xList->length-1) )
	_(ensures \forall unsigned i; 
		( i < \old(xList->position[\old(li)]) ) ==> 
			( xList->list[i]==\old(xList->list[i]) ) 
	 )
	_(ensures \forall unsigned i; 
		(	( i >= \old(xList->position[\old(li)]) ) && 
			( i < xList->length ) 
		) ==> ( xList->list[i] == \old(xList->list[i+1]) ) 
	 ) 
	_(ensures li->pvContainer == NULL )
	_(ensures \forall unsigned i; 
		( i<xList->length ) ==> ( xList->list[i] != li ) )
	_(ensures !(li \in xList->\owns) )
	_(ensures \wrapped(li) )
	_(ensures xList->\owns == \old(xList->\owns) - li )
	_(ensures \fresh(li) )	
	/*	To say explicitely that li's ownership is transferred 
		to the current thread. Because in VCC the ownership 
		transfer will be effected only when the 
		owner is closed.
	*/
	_(ensures ( xList->type == FIFO ) ==> 
			( xList->priority == \old(xList->priority) ) 
	 )
	_(ensures li->ownersPriority <= maxPrio )
	_(ensures \forall unsigned i;	
		(	( i < xList->length ) && 
			( xList->list[i] \in xList->\owns ) 
		) ==> ( (xList->list[i]->pvOwner != li->pvOwner ) ) 
	 )
	_(ensures xList->length < maxNumVal )  
	/*	The above is required to prove that there is a space 
		for insertion after every deletion
	*/
	_(ensures xList->position[li]== maxNumVal )
//////////////////////////////////////////////////////( li != li ) ==>
	_(ensures \forall xListItem *xli; 
			( xli->xItemValue == \old(xli->xItemValue) ) 
	 )
	//_(ensures \forall xListItem *xli; 
	//			( xli->pxNext == \old(xli->pxNext) ) 
	// )
	//_(ensures \forall xListItem *xli; 
	//			( xli->pxPrevious == \old(xli->pxPrevious) ) 
	// ) #ANIRUDH: SHOULD NOT BE INCLUDED AS pxNext and pxPrevious are not a part of xListMap
	_(ensures \forall xListItem *xli; 
				( xli->pvOwner==\old(xli->pvOwner) ) 
	 )
	_(ensures \forall xListItem *xli; ( xli != li ) ==>
				( xli->pvContainer==\old(xli->pvContainer) ) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->ownersPriority == 
					\old(xli->ownersPriority) 
				) 
	 )
	_(ensures \forall xListItem *xli; 
				(	xli->pvOwner->uxPriority == 
					\old(xli->pvOwner->uxPriority) 
				) 
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvGenericListItem == 
			\old(tcb->pvGenericListItem) 
		)
	 )
	_(ensures \forall TCB *tcb;
		(	tcb->pvEventListItem == 
			\old(tcb->pvEventListItem) 
		)
	 )
	_(ensures \forall TCB *tcb; 
				tcb->uxPriority == 
				\old(tcb->uxPriority) 
	 )
	_(ensures \forall xMap  *L; 
								L->type==\old(L->type) 
	 )
	_(ensures \forall xMap  *L ; ( xList != L ) ==> 
		( L->length  == \old(L->length) )
	 )
	_(ensures \forall xMap  *L ; 
		( L->priority  == \old(L->priority) )
	 )
	_(ensures \forall xMap  *L ; ( xList != L ) ==> 
		(
			\forall unsigned i; ( i<L->length ) ==> 
						( L->list[i] == \old(L->list[i]) )
		)
	 )
	_(ensures \forall xMap  *L;\forall  xListItem *xli; 
		( xList != L ) ==> 
				(	L->position[xli] == 
					\old(L->position[xli])
				) 
	 )
///////////////////////////////////////////////////////
	SANITY_CHECK()
	;

#define X_LIST_JOINT_H
#endif