Incrementing in OpenCL

Simple OpenCL kernel that increments a single element of a shared array. This verification example shows that VerCors is capable of verifying actual OpenCL kernel code.

General Information

  • Backend: Silicon
  • Language: Cuda
  • Features: GPU Kernels, Arrays
  • Path to Example File: opencl/opencl_incr.c
  • Should Verify: Yes
  • Date: 2017-06-20
  • Lines of Code: 14 (comments not included)
  • Lines of Specification: 3 (21.4% of total)
  • Computation Time: 14.4 seconds