/* This header file contains the function prototypes for 
 * pointer operations.
 */

#ifndef _POINTER_
#define _POINTER_
#pragma CIVL ACSL
#include<civlc.cvh>
#include<op.h>

/* ******************************* Functions ******************************* */

/* updates the leaf nodes of a status variable to the default value 0 */
/*@ depends_on \access(obj);
  @ executes_when \true;
  @*/
$system void $set_default(void *obj);

/* applies the operation op on obj1 and obj2 and stores the result */
/*@ depends_on \access(obj1, obj2, result);
  @ executes_when \true;
  @*/
$system void $apply(void *obj1, $operation op, void *obj2, void *result);

/* are the object pointed to equal? */
/*@ depends_on \access(x, y);
  @ executes_when \true;
  @*/
$system _Bool $equals(void *x, void *y);

/* Assert that the two objects pointed are equal */
/*@ depends_on \access(x, y);
  @ executes_when \true;
  @*/
$system void $assert_equals(void *x, void *y, ...);

/* Semantics: Does the object pointed to by obj1 contain that
pointed to by obj1? */
/*@ depends_on \access(obj1, obj2);
  @ executes_when \true;
  @*/
$system _Bool $contains(void *obj1, void *obj2);

/* Translates a pointer into one object to a pointer
 * into a different object with similar structure. */
/*@ depends_on \nothing;
  @ executes_when \true;
  @*/
$system void * $translate_ptr(void *ptr, void *obj);

/* Copies the value pointed to by the right operand to the memory 
 * location specified by the left operand. */
/*@ depends_on \access(ptr, value);
  @ executes_when \true;
  @*/
$system void $copy(void *ptr, void *value);

/*
  copy the references to the leaf nodes of obj to the given array
  obj: pointer to type T' whose leaf node types are all type T
  array: pointer to array of pointer to type T
*/
/*@ depends_on \access(array);
  @ executes_when \true;
  @*/
$system void $leaf_node_ptrs(void *array, void *obj);

/*
  returns true if the given pointer is referencing to 
  an object by identity reference
*/
/*@ depends_on \nothing;
  @ executes_when \true;
  @*/
$system _Bool $is_identity_ref(void *obj);

/*
  updates the leaf nodes of the given objects to with
  the given integer value
*/
/*@ depends_on \access(obj);
  @ executes_when \true;
  @*/
$system void $set_leaf_nodes(void *obj, int value);

/*
  returns true iff all leaf nodes of the given
  object equal to the given value
*/
/*@ depends_on \access(obj);
  @ executes_when \true;
  @*/
$system _Bool $leaf_nodes_equal_to(void *obj, int value);

/*
  returns true iff at least one leaf nodes of the given
  object equal to the given value
 */
/*@ depends_on \access(obj);
  @ executes_when \true;
  @*/
$system _Bool $has_leaf_node_equal_to(void *obj, int value);

/*
  can the given pointer be safely referenced?
  A derefable pointer is not NULL
  and is referring to a memory location of some dyscope.
*/
/*@ depends_on \nothing;
  @ executes_when \true;
  @*/
$system _Bool $is_derefable_pointer(void *ptr);

/* 
   Gives a pointer addition operation. Note that the input pointer will always be
   casted to the form of a pointer to a primitive data type.
 */
/*@ depends_on \nothing;
  @ executes_when \true;
  @*/
$system void * $pointer_add(const void *ptr,  int offset, int type_size);


#endif