source: CIVL/examples/translation/opencl/setup/openCL.cvl@ aef8b11

#include "cl.cvl"
#include<string.h>
#include<stdlib.h>
#include <stdio.h>

$input int DEVICE_ID;
$input int DEVICE_ID_BOUND;

$assume 0 < DEVICE_ID && DEVICE_ID < DEVICE_ID_BOUND;


/*  
 Gives back an int for the error code, fills devices with ids of devices
 See cl.cvl for files
 platform - The platform, can be NULL
 device_type - Has the device type
 num_entries - Is the max number of devices that can be filled
 devices - A pointer that will contain the IDs
 num_devices - Says how many devices were added, can be NULL
*/
int clGetDeviceIDs(cl_platform_id platform, 
  cl_device_type device_type, 
  cl_uint num_entries, 
  cl_device_id *devices, 
  cl_uint *num_devices)
  {
  //$assume device_type == CL_DEVICE_TYPE_DEFAULT;
  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;
  }
  
  //CIVL cannot pass this if block if not commented out
  /*
  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)
      {
        devices[0] = (cl_device_id)(&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;

}

/*
  Creates the cl_context that will be used in later types to be made
  properties - Context property names
  num_devices - Number of devices
  devices - Pointer to the devices from clGetDeviceIDs
  pfn_notify - Callback function to report errors. Can be NULL
  user_data - Part of pfn_notify. Can be NULL
  errcode_ret - Returns proper error code.
*/

cl_context clCreateContext(const cl_context_properties  *properties,
                 cl_uint                       num_devices,
                 const cl_device_id *          devices,
                 void (CL_CALLBACK *pfn_notify)(const char *, const void *, size_t, void *),
                 void *                        user_data,
                 cl_int *                      errcode_ret)
{
  cl_int default_errcode_ret;
  cl_context ctx;
  
  if(!errcode_ret)
  {
    errcode_ret = &default_errcode_ret;
  }
    
  if (!devices || !num_devices || (!pfn_notify && user_data))
  {
    *errcode_ret = CL_INVALID_VALUE;
    return 0;
  }
    
  *errcode_ret = CL_SUCCESS;
  
  ctx = (cl_context)malloc(sizeof(_cl_context));

  
  ctx->properties = properties;
  ctx->num_devices = num_devices;
  ctx->devices = devices;
  ctx->pfn_notify = pfn_notify;
  ctx->user_data = user_data;
  ctx->errcode_ret = errcode_ret;
  
    
  if(*errcode_ret != CL_SUCCESS)
  {
    //delete ctx;
    return 0;
  }
  
  return(cl_context) ctx;
   
}

/* Creates a cl_command_queue
  context - The context created from clCreateContext
  device - The pointer to IDs from clGetDeviceIDs
  properties - Bitfield for properties, see cl.cvl
  errcode_ret - Returns proper error code.
*/
cl_command_queue clCreateCommandQueue(cl_context context,
  cl_device_id device,
  cl_command_queue_properties properties,
  cl_int* errcode_ret)
{
  cl_int default_errcode_ret;
  cl_command_queue cmd;
  
     // No errcode_ret ?
  if (!errcode_ret)
  {
    errcode_ret = &default_errcode_ret;
  }
  
  cmd = (cl_command_queue)malloc(sizeof(_cl_command_queue));
  
  cmd->context = context;
  cmd->device = device;
  cmd->properties = properties;
  cmd->errcode_ret = errcode_ret;
  
  return cmd;
}

/*Makes a program from context. Not quite like the original implementation
  context - From clCreateContext
  count - number of source codes for strings
  strings - Array of chars that makes up code
  lengths - string length, if NULL nulls the strings
  errcode_ret - Returns proper error code
*/
cl_program clCreateProgramWithSource(cl_context context,
  cl_uint count,
  const char** strings,
  const size_t * lengths,
  cl_int * errcode_ret)
{
  cl_int default_errcode_ret;
  cl_program program;
  
  program = (cl_program)malloc(sizeof(_cl_program));
  
  if(!errcode_ret)
  {
    errcode_ret = &default_errcode_ret;
  }
  
  *errcode_ret = CL_SUCCESS;
  //*errcode_ret = program->loadSources(count, strings, lengths);

  //corrects lengths
  
  for (cl_uint i = 0; i < count; i++)
  {
    size_t len = 0;
    const char *data = strings[i];
    
    if (lengths && lengths[i])
    {
      len = lengths[i];
    }
    else
    {
      len = strlen(data);
    }
    
    
    //remove trailing \0's, or null characters at EOF
    //remember that '' is char, "" is string
    while (len > 0 && (data[len-1] == '\0'))
    {
      len--;
    }
    
  }
  
  program->context = context;
  program->count = count;
  program->strings = strings;
  program->lengths = lengths;
  $assert (*errcode_ret == CL_SUCCESS);
  //the original for loop can make *errcode_ret not CL_SUCCESS, this is a placeholder
  
  return (cl_program) program;
}

/*Makes a program from context. Not quite like the original implementation
  Still looks almost like clCreateProgramWithSource, change
  context - From clCreateContext
  num_devices - Number of devices in device_list
  device_list - Pointer to list of devices associated with a program
  lengths - Array of size in bytes the program binaries are
  binaries - Array of pointers to program binaries
  binary_status - Returns whether each device was loaded, an array of num_devices
  errcode_ret - Returns proper error code
*/

cl_program clCreateProgramWithBinaries(cl_context context,
  cl_uint num_devices,
  const cl_device_id *device_list,
  const size_t *lengths,
  const unsigned char **binaries,
  cl_int *binary_status,
  cl_int *errcode_ret)
{
  cl_int default_errcode_ret;
  cl_program program;
  cl_uint context_num_devices = 0;
  cl_device_id *context_devices;
  
  program = (cl_program)malloc(sizeof(_cl_program));
  
  if(!errcode_ret)
  {
    errcode_ret = &default_errcode_ret;
  }
  
  *errcode_ret = CL_SUCCESS;
  //*errcode_ret = program->loadBinaries(count, strings, lengths);

  
  for (cl_uint i = 0; i < num_devices; i++)
  {
    bool found = false;
    
    if (!lengths[i] || !binaries[i])
    {
      if(binary_status)
      {
        binary_status[i] = CL_INVALID_VALUE;
        break;
      }
      
      *errcode_ret = CL_INVALID_VALUE;
    }
    
    for (cl_uint j = 0; j < context_num_devices; j++)
    {
      if(device_list[i] == context_devices[j])
      {
        found = true;
        return 0;
      }
    }
    
    if(!found)
    {
      *errcode_ret = CL_INVALID_DEVICE;
      break;
    }
  }
  
  program->context = context;
  program->lengths = lengths;
  $assert (*errcode_ret == CL_SUCCESS);
  
  return (cl_program) program;
}


/* "Builds" a program executable from the source/binary
  program - The program, from clCreateProgramWithBinary or clCreateProgramWithContext
  num_devices - Number of devices in device_list, can be 0
  device_list - List of devices, can be NULL
  options - Pointer describing build options, can be NULL
  pfn_notify - Function pointer to notification routine, can be NULL and won't return until build is completed
  user_data - argument for pfn_notify, can be NULL
*/
/*
void clBuildProgram(cl_program program,
  cl_uint num_devices,
  const cl_device_id *device_list,
  const char *options,
  void (CL_CALLBACK *pfn_notify)(cl_program program, void *user_data),
  void *user_data)
{
  
  if (num_devices)
  {
    cl_uint context_num_devices = 0;
    cl_device_id *context_devices;
    cl_context *context = (cl_context *) program->context;
    cl_int result;
    
    context_devices = (cl_device_id *) 
  }
}
*/