#include "openCLtypes.cvl"

$input int DEVICE_ID;
$input int DEVICE_ID_BOUND;

$assume 0 < DEVICE_ID && DEVICE_ID < DEVICE_ID_BOUND;

int clGetDEVICE_IDs(cl_platform_id platform,
  cl_device_type device_type,
  cl_uint num_entries,
  cl_device_id *devices,
  cl_uint *num_devices)
  {
  int i = 0;
  //cl_platform_id int value can be null

  //num_entries number of devices that can be added
  
  if(num_entries == 0 && devices != 0)
  {
    return CL_INVALID_VALUE;
  }
 	
  if(num_entries == 0 && devices == 0)
  {
    return CL_INVALID_VALUE;
  }
 	
  //device_type type a bitfield that somehow gets type of OpenCL device
  //use the device types, look in openCLtypes and look for CL_DEVICE_TYPE
  //-> CPU, GPU, ACCELERATOR, DEFAULT, ALL
  
  if(device_type & (CL_DEVICE_TYPE_DEFAULT | CL_DEVICE_TYPE_CPU | 
    CL_DEVICE_TYPE_GPU | CL_DEVICE_TYPE_ACCELERATOR | 
    CL_DEVICE_TYPE_CUSTOM | CL_DEVICE_TYPE_ALL)
  {
    while (i < num_entries)
    {
    //if devices not null/0? What does that even mean?
    //If there isn't anything there, you can't add in?
      if(devices)
      {
        devices[i] = DEVICE_ID;
        //how to say "use anything"?
        i++;
      }
      else
      {
        break;
      }
      
    }
    if (num_devices)
    {
      *num_devices = i;
    }
  }
  
  else
  {
    return CL_DEVICE_NOT_FOUND;
  }
 	

  //*devices list of devices found, use
  //cl_device_id device_id;
  //&device_id
 	
 
 	
  return CL_SUCCESS;

 		
  }