call_kernel.h File Reference

#include <stddef.h>
#include <cstdlib>
#include <string.h>
#include <pthread.h>
#include <assert.h>
#include "vector_types.h"
#include "device_launch_parameters.h"
#include <new>

Include dependency graph for call_kernel.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	arg_struct_no_params
struct	arg_struct
struct	arg_struct1
struct	arg_struct2
struct	arg_struct2_i
struct	arg_struct_u1
struct	arg_struct_u2
struct	arg_struct_u3
struct	arg_struct_float
struct	arg_struct_ffloat
struct	arg_struct_f5i2
struct	arg_struct_d1
struct	arg_struct_d2
struct	arg_struct_c3
struct	arg_struct_intt
struct	arg_struct_fuintt
struct	arg_struct_fuint
struct	arg_struct_fuintint
struct	arg_struct_fint
struct	arg_struct_iuull
struct	arg_struct_i_ui_ull_f
struct	arg_struct1_ui

Macros
#define	GPU_threads   2

Typedefs
typedef void *(*	voidFunction_no_params) ()
typedef void *(*	voidFunction_one) (int *arg)
typedef void *(*	voidFunction_two) (int *arg, int *arg2)
typedef void *(*	voidFunction_three) (int *arg, int *arg2, int *arg3)
typedef void *(*	voidFunction_two_i) (int arg, int arg2)
typedef void *(*	voidFunction_one_u) (uint4 *arg)
typedef void *(*	voidFunction_two_u) (unsigned int *arg, int *arg2)
typedef void *(*	voidFunction_three_u) (unsigned arg, unsigned arg2, unsigned arg3)
typedef void *(*	voidFunction_float) (float *arg1)
typedef void *(*	voidFunction_ffloat) (float *arg1, float arg2)
typedef void *(*	voidFunction_f5i2) (float *arg1, float *arg2, float *arg3, float *arg4, float *arg5, int arg6, int arg7)
typedef void *(*	voidFunction_d1) (double *arg1)
typedef void *(*	voidFunction_d2) (double arg1, int arg2)
typedef void *(*	voidFunction_c3) (char *arg1, char *arg2, char *arg3)
typedef void *(*	voidFunction_intt) (int *arg1, int arg2)
typedef void *(*	voidFunction_fuintt) (float *arg1, unsigned int arg2, unsigned int arg3)
typedef void *(*	voidFunction_fuint) (float *arg1, unsigned int arg2)
typedef void *(*	voidFunction_fuintint) (float *arg1, unsigned int arg2, int arg3)
typedef void *(*	voidFunction_fint) (float *arg1, int arg2)
typedef void *(*	voidFunction_iuull) (int *arg1, unsigned int *arg2, unsigned long long int *arg3)
typedef void *(*	voidFunction_i_ui_ull_f) (int *arg1, unsigned int *arg2, unsigned long long int *arg3, float *arg4)
typedef void *(*	voidFunction_one_ui) (unsigned int *arg)
typedef void *(*	voidFunction_ui) (unsigned int *arg)
typedef struct arg_struct_no_params	Targ_no_params
typedef struct arg_struct	Targ
typedef struct arg_struct1	Targ1
typedef struct arg_struct2	Targ2
typedef struct arg_struct2_i	Targ2_i
typedef struct arg_struct_u1	Targ_u1
typedef struct arg_struct_u2	Targ_u2
typedef struct arg_struct_u3	Targ_u3
typedef struct arg_struct_intt	Targ_intt
typedef struct arg_struct_float	Targ_float
typedef struct arg_struct_ffloat	Targ_ffloat
typedef struct arg_struct_f5i2	Targ_f5i2
typedef struct arg_struct_d1	Targ_d1
typedef struct arg_struct_d2	Targ_d2
typedef struct arg_struct_c3	Targ_c3
typedef struct arg_struct_fuintt	Targ_fuintt
typedef struct arg_struct_fuint	Targ_fuint
typedef struct arg_struct_fuintint	Targ_fuintint
typedef struct arg_struct_fint	Targ_fint
typedef struct arg_struct_iuull	Targ_iuull
typedef struct arg_struct_i_ui_ull_f	Targ_i_ui_ull_f
typedef struct arg_struct1_ui	Targ1_ui

Functions
int	__cudaChooseDeviceCount ()
	__attribute__ ((annotate("__ESBMC_inf_size"))) int __cudaDeviceOf[1]
unsigned int	__cudaPeerIndex (int device, int peer)
template<class T>
void	__cudaCheckKernelArg (T)
template<class T>
void	__cudaCheckKernelArg (T *p)
template<class... Ts>
void	__cudaCheckKernelArgs (Ts... args)
void *	ESBMC_execute_kernel_no_params (void *args)
void *	ESBMC_execute_kernel_one (void *args)
void *	ESBMC_execute_kernel_two (void *args)
void *	ESBMC_execute_kernel_three (void *args)
void *	ESBMC_execute_kernel_two_i (void *args)
void *	ESBMC_execute_kernel_one_u (void *args)
void *	ESBMC_execute_kernel_two_u (void *args)
void *	ESBMC_execute_kernel_three_u (void *args)
void *	ESBMC_execute_kernel_float (void *args)
void *	ESBMC_execute_kernel_ffloat (void *args)
void *	ESBMC_execute_kernel_f5i2 (void *args)
void *	ESBMC_execute_kernel_d1 (void *args)
void *	ESBMC_execute_kernel_d2 (void *args)
void *	ESBMC_execute_kernel_c3 (void *args)
void *	ESBMC_execute_kernel_intt (void *args)
void *	ESBMC_execute_kernel_fuintt (void *args)
void *	ESBMC_execute_kernel_fuint (void *args)
void *	ESBMC_execute_kernel_fuintint (void *args)
void *	ESBMC_execute_kernel_fint (void *args)
void *	ESBMC_execute_kernel_three_iuull (void *args)
void *	ESBMC_execute_kernel_four_i_ui_ull_f (void *args)
void *	ESBMC_execute_kernel_ui (void *args)
void	ESBMC_verify_kernel_no_params (void *(*kernel)(), int blocks, int threads)
void	ESBMC_verify_kernel_with_one_arg (void *(*kernel)(int *), int blocks, int threads, void *arg1)
void	ESBMC_verify_kernel_with_two_args (void *(*kernel)(int *, int *), int blocks, int threads, void *arg1, void *arg2)
void	ESBMC_verify_kernel_with_three_args (void *(*kernel)(int *, int *, int *), int blocks, int threads, void *arg1, void *arg2, void *arg3)
void	ESBMC_verify_kernel_with_two_args_i (void *(*kernel)(int, int), int blocks, int threads, int arg1, int arg2)
void	ESBMC_verify_kernel_with_one_args_u (void *(*kernel)(uint4 *), int blocks, int threads, void *arg1)
void	ESBMC_verify_kernel_with_two_args_u (void *(*kernel)(unsigned int *, int *), int blocks, int threads, void *arg1, void *arg2)
void	ESBMC_verify_kernel_with_three_args_u (void *(*kernel)(unsigned, unsigned, unsigned), int blocks, int threads, unsigned arg1, unsigned arg2, unsigned arg3)
void	ESBMC_verify_kernel_float (void *(*kernel)(float *), int blocks, int threads, void *arg1)
void	ESBMC_verify_kernel_ffloat (void *(*kernel)(float *, float), int blocks, int threads, void *arg1, float arg2)
void	ESBMC_verify_kernel_f5i2 (void *(*kernel)(float *, float *, float *, float *, float *, int, int), int blocks, int threads, void *arg1, void *arg2, void *arg3, void *arg4, void *arg5, int arg6, int arg7)
void	ESBMC_verify_kernel_d1 (void *(*kernel)(double *), int blocks, int threads, void *arg1)
void	ESBMC_verify_kernel_d2 (void *(*kernel)(double, int), int blocks, int threads, double arg1, int arg2)
void	ESBMC_verify_kernel_c3 (void *(*kernel)(char *, char *, char *), int blocks, int threads, void *arg1, void *arg2, void *arg3)
void	ESBMC_verify_kernel__intt (void *(*kernel)(int *, int), int blocks, int threads, void *arg1, int arg2)
void	ESBMC_verify_kernel__fuintt (void *(*kernel)(float *, unsigned int, unsigned int), int blocks, int threads, void *arg1, unsigned int arg2, unsigned int arg3)
void	ESBMC_verify_kernel__fuint (void *(*kernel)(float *, unsigned int), int blocks, int threads, void *arg1, unsigned int arg2)
void	ESBMC_verify_kernel__fuintint (void *(*kernel)(float *, unsigned int, int), int blocks, int threads, void *arg1, unsigned int arg2, int arg3)
void	ESBMC_verify_kernel__fint (void *(*kernel)(float *, int), int blocks, int threads, void *arg1, int arg2)
void	ESBMC_verify_kernel_with_three_args_iuull (void *(*kernel)(int *, unsigned int *, unsigned long long int *), int blocks, int threads, void *arg1, void *arg2, void *arg3)
void	ESBMC_verify_kernel_with_four__args_i_ui_ull_f (void *(*kernel)(int *, unsigned int *, unsigned long long int *, float *), int blocks, int threads, void *arg1, void *arg2, void *arg3, void *arg4)
void	ESBMC_verify_kernel_one_ui (void *(*kernel)(unsigned int *), int blocks, int threads, void *arg1)
template<class RET, class BLOCK, class THREAD>
void	ESBMC_verify_kernel (RET *kernel, BLOCK blocks, THREAD threads)
template<class RET, class BLOCK, class THREAD, class T1>
void	ESBMC_verify_kernel (RET *kernel, BLOCK blocks, THREAD threads, T1 arg)
template<class RET, class BLOCK, class THREAD, class T1, class T2>
void	ESBMC_verify_kernel (RET *kernel, BLOCK blocks, THREAD threads, T1 arg, T2 arg2)
template<class RET, class BLOCK, class THREAD, class T1, class T2, class T3>
void	ESBMC_verify_kernel (RET *kernel, BLOCK blocks, THREAD threads, T1 arg, T2 arg2, T3 arg3)
template<class RET, class BLOCK, class THREAD, class T1, class T2>
void	ESBMC_verify_kernel_i (RET *kernel, BLOCK blocks, THREAD threads, T1 arg, T2 arg2)
template<class RET, class BLOCK, class THREAD, class T1>
void	ESBMC_verify_kernel_u (RET *kernel, BLOCK blocks, THREAD threads, T1 arg)
template<class RET, class BLOCK, class THREAD, class T1, class T2>
void	ESBMC_verify_kernel_u (RET *kernel, BLOCK blocks, THREAD threads, T1 arg, T2 arg2)
template<class RET, class BLOCK, class THREAD, class T1, class T2, class T3>
void	ESBMC_verify_kernel_u (RET *kernel, BLOCK blocks, THREAD threads, T1 arg, T2 arg2, T3 arg3)
template<class RET, class BLOCK, class THREAD, class T1, class T2>
void	ESBMC_verify_kernel_f (RET *kernel, BLOCK blocks, THREAD threads, T1 arg, T2 arg2)
template<class RET, class BLOCK, class THREAD, class T1>
void	ESBMC_verify_kernel_f (RET *kernel, BLOCK blocks, THREAD threads, T1 arg)
template<class RET, class BLOCK, class THREAD, class T1, class T2, class T3, class T4, class T5, class T6, class T7>
void	ESBMC_verify_kernel_f (RET *kernel, BLOCK blocks, THREAD threads, T1 arg, T2 arg2, T3 arg3, T4 arg4, T5 arg5, T6 arg6, T7 arg7)
template<class RET, class BLOCK, class THREAD, class T1, class T2, class T3>
void	ESBMC_verify_kernel_c (RET *kernel, BLOCK blocks, THREAD threads, T1 arg, T2 arg2, T3 arg3)
template<class RET, class BLOCK, class THREAD, class T1>
void	ESBMC_verify_kernel_c (RET *kernel, BLOCK blocks, THREAD threads, T1 arg)
template<class RET, class BLOCK, class THREAD, class T1, class T2>
void	ESBMC_verify_kernel_c (RET *kernel, BLOCK blocks, THREAD threads, T1 arg, T2 arg2)
template<class RET, class BLOCK, class THREAD, class T1, class T2>
void	ESBMC_verify_kernel_intt (RET *kernel, BLOCK blocks, THREAD threads, T1 arg, T2 arg2)
template<class RET, class BLOCK, class THREAD, class T1, class T2, class T3>
void	ESBMC_verify_kernel_fuintt (RET *kernel, BLOCK blocks, THREAD threads, T1 arg, T2 arg2, T3 arg3)
template<class RET, class BLOCK, class THREAD, class T1, class T2>
void	ESBMC_verify_kernel_fuintt (RET *kernel, BLOCK blocks, THREAD threads, T1 arg, T2 arg2)
template<class RET, class BLOCK, class THREAD, class T1, class T2, class T3>
void	ESBMC_verify_kernel_fuintint (RET *kernel, BLOCK blocks, THREAD threads, T1 arg, T2 arg2, T3 arg3)
template<class RET, class BLOCK, class THREAD, class T1, class T2>
void	ESBMC_verify_kernel_fuintint (RET *kernel, BLOCK blocks, THREAD threads, T1 arg, T2 arg2)
template<class RET, class BLOCK, class THREAD, class T1, class T2, class T3>
void	ESBMC_verify_kernel_three_args_iuull (RET *kernel, BLOCK blocks, THREAD threads, T1 arg, T2 arg2, T3 arg3)
template<class RET, class BLOCK, class THREAD, class T1, class T2, class T3, class T4>
void	ESBMC_verify_kernel_four (RET *kernel, BLOCK blocks, THREAD threads, T1 arg, T2 arg2, T3 arg3, T4 arg4)
template<class RET, class BLOCK, class THREAD, class T1>
void	ESBMC_verify_kernel_ui (RET *kernel, BLOCK blocks, THREAD threads, T1 arg)

Variables
int	blockGlobal
int	threadGlobal
int	__cudaDeviceCount = __cudaChooseDeviceCount()
__thread int	__cudaCurrentDevice = 0
unsigned int	n_threads
Targ_no_params	dev_no_params
Targ	dev_three
Targ1	dev_one
Targ2	dev_two
Targ2_i	dev_two_i
Targ_u1	dev_one_u
Targ_u2	dev_two_u
Targ_u3	dev_three_u
Targ_intt	dev_intt
Targ_float	dev_float
Targ_ffloat	dev_ffloat
Targ_f5i2	dev_f5i2
Targ_d1	dev_d1
Targ_d2	dev_d2
Targ_c3	dev_c3
Targ_fuintt	dev_fuintt
Targ_fuint	dev_fuint
Targ_fuintint	dev_fuintint
Targ_fint	dev_fint
Targ_iuull	dev_three_iuull
Targ_i_ui_ull_f	dev_four_i_ui_ull_f
Targ1_ui	dev_ui

Macro Definition Documentation

GPU_threads

#define GPU_threads   2

Typedef Documentation

Targ

typedef struct arg_struct Targ

Targ1

typedef struct arg_struct1 Targ1

Targ1_ui

typedef struct arg_struct1_ui Targ1_ui

Targ2

typedef struct arg_struct2 Targ2

Targ2_i

typedef struct arg_struct2_i Targ2_i

Targ_c3

typedef struct arg_struct_c3 Targ_c3

Targ_d1

typedef struct arg_struct_d1 Targ_d1

Targ_d2

typedef struct arg_struct_d2 Targ_d2

Targ_f5i2

typedef struct arg_struct_f5i2 Targ_f5i2

Targ_ffloat

typedef struct arg_struct_ffloat Targ_ffloat

Targ_fint

typedef struct arg_struct_fint Targ_fint

Targ_float

typedef struct arg_struct_float Targ_float

Targ_fuint

typedef struct arg_struct_fuint Targ_fuint

Targ_fuintint

typedef struct arg_struct_fuintint Targ_fuintint

Targ_fuintt

typedef struct arg_struct_fuintt Targ_fuintt

Targ_i_ui_ull_f

typedef struct arg_struct_i_ui_ull_f Targ_i_ui_ull_f

Targ_intt

typedef struct arg_struct_intt Targ_intt

Targ_iuull

typedef struct arg_struct_iuull Targ_iuull

Targ_no_params

typedef struct arg_struct_no_params Targ_no_params

Targ_u1

typedef struct arg_struct_u1 Targ_u1

Targ_u2

typedef struct arg_struct_u2 Targ_u2

Targ_u3

typedef struct arg_struct_u3 Targ_u3

voidFunction_c3

typedef void *(* voidFunction_c3) (char *arg1, char *arg2, char *arg3)

voidFunction_d1

typedef void *(* voidFunction_d1) (double *arg1)

voidFunction_d2

typedef void *(* voidFunction_d2) (double arg1, int arg2)

voidFunction_f5i2

typedef void *(* voidFunction_f5i2) (float *arg1, float *arg2, float *arg3, float *arg4, float *arg5, int arg6, int arg7)

voidFunction_ffloat

typedef void *(* voidFunction_ffloat) (float *arg1, float arg2)

voidFunction_fint

typedef void *(* voidFunction_fint) (float *arg1, int arg2)

voidFunction_float

typedef void *(* voidFunction_float) (float *arg1)

voidFunction_fuint

typedef void *(* voidFunction_fuint) (float *arg1, unsigned int arg2)

voidFunction_fuintint

typedef void *( * voidFunction_fuintint) (float *arg1, unsigned int arg2, int arg3)

voidFunction_fuintt

typedef void *( * voidFunction_fuintt) (float *arg1, unsigned int arg2, unsigned int arg3)

voidFunction_i_ui_ull_f

typedef void *(* voidFunction_i_ui_ull_f) (int *arg1, unsigned int *arg2, unsigned long long int *arg3, float *arg4)

voidFunction_intt

typedef void *(* voidFunction_intt) (int *arg1, int arg2)

voidFunction_iuull

typedef void *(* voidFunction_iuull) (int *arg1, unsigned int *arg2, unsigned long long int *arg3)

voidFunction_no_params

typedef void *(* voidFunction_no_params) ()

voidFunction_one

typedef void *(* voidFunction_one) (int *arg)

voidFunction_one_u

typedef void *(* voidFunction_one_u) (uint4 *arg)

voidFunction_one_ui

typedef void *(* voidFunction_one_ui) (unsigned int *arg)

voidFunction_three

typedef void *(* voidFunction_three) (int *arg, int *arg2, int *arg3)

voidFunction_three_u

typedef void *( * voidFunction_three_u) (unsigned arg, unsigned arg2, unsigned arg3)

voidFunction_two

typedef void *(* voidFunction_two) (int *arg, int *arg2)

voidFunction_two_i

typedef void *(* voidFunction_two_i) (int arg, int arg2)

voidFunction_two_u

typedef void *(* voidFunction_two_u) (unsigned int *arg, int *arg2)

voidFunction_ui

typedef void *(* voidFunction_ui) (unsigned int *arg)

Function Documentation

__attribute__()

__attribute__

(

(annotate("__ESBMC_inf_size"))

)

__cudaCheckKernelArg() [1/2]

template<class T>

void __cudaCheckKernelArg

(

T *

p

)

__cudaCheckKernelArg() [2/2]

template<class T>

void __cudaCheckKernelArg

(

T

)

__cudaCheckKernelArgs()

template<class... Ts>

void __cudaCheckKernelArgs

(

Ts...

args

)

__cudaChooseDeviceCount()

int __cudaChooseDeviceCount

(

)

__cudaPeerIndex()

unsigned int __cudaPeerIndex	(	int	device,
		int	peer )

ESBMC_execute_kernel_c3()

void * ESBMC_execute_kernel_c3

(

void *

args

)

ESBMC_execute_kernel_d1()

void * ESBMC_execute_kernel_d1

(

void *

args

)

ESBMC_execute_kernel_d2()

void * ESBMC_execute_kernel_d2

(

void *

args

)

ESBMC_execute_kernel_f5i2()

void * ESBMC_execute_kernel_f5i2

(

void *

args

)

ESBMC_execute_kernel_ffloat()

void * ESBMC_execute_kernel_ffloat

(

void *

args

)

ESBMC_execute_kernel_fint()

void * ESBMC_execute_kernel_fint

(

void *

args

)

ESBMC_execute_kernel_float()

void * ESBMC_execute_kernel_float

(

void *

args

)

ESBMC_execute_kernel_four_i_ui_ull_f()

void * ESBMC_execute_kernel_four_i_ui_ull_f

(

void *

args

)

ESBMC_execute_kernel_fuint()

void * ESBMC_execute_kernel_fuint

(

void *

args

)

ESBMC_execute_kernel_fuintint()

void * ESBMC_execute_kernel_fuintint

(

void *

args

)

ESBMC_execute_kernel_fuintt()

void * ESBMC_execute_kernel_fuintt

(

void *

args

)

ESBMC_execute_kernel_intt()

void * ESBMC_execute_kernel_intt

(

void *

args

)

ESBMC_execute_kernel_no_params()

void * ESBMC_execute_kernel_no_params

(

void *

args

)

ESBMC_execute_kernel_one()

void * ESBMC_execute_kernel_one

(

void *

args

)

ESBMC_execute_kernel_one_u()

void * ESBMC_execute_kernel_one_u

(

void *

args

)

ESBMC_execute_kernel_three()

void * ESBMC_execute_kernel_three

(

void *

args

)

ESBMC_execute_kernel_three_iuull()

void * ESBMC_execute_kernel_three_iuull

(

void *

args

)

ESBMC_execute_kernel_three_u()

void * ESBMC_execute_kernel_three_u

(

void *

args

)

ESBMC_execute_kernel_two()

void * ESBMC_execute_kernel_two

(

void *

args

)

ESBMC_execute_kernel_two_i()

void * ESBMC_execute_kernel_two_i

(

void *

args

)

ESBMC_execute_kernel_two_u()

void * ESBMC_execute_kernel_two_u

(

void *

args

)

ESBMC_execute_kernel_ui()

void * ESBMC_execute_kernel_ui

(

void *

args

)

ESBMC_verify_kernel() [1/4]

template<class RET, class BLOCK, class THREAD>

void ESBMC_verify_kernel	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads )

ESBMC_verify_kernel() [2/4]

template<class RET, class BLOCK, class THREAD, class T1>

void ESBMC_verify_kernel	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg )

ESBMC_verify_kernel() [3/4]

template<class RET, class BLOCK, class THREAD, class T1, class T2>

void ESBMC_verify_kernel	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg,
		T2	arg2 )

ESBMC_verify_kernel() [4/4]

template<class RET, class BLOCK, class THREAD, class T1, class T2, class T3>

void ESBMC_verify_kernel	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg,
		T2	arg2,
		T3	arg3 )

ESBMC_verify_kernel__fint()

void ESBMC_verify_kernel__fint	(	void *(*	kernel )(float *, int),
		int	blocks,
		int	threads,
		void *	arg1,
		int	arg2 )

ESBMC_verify_kernel__fuint()

void ESBMC_verify_kernel__fuint	(	void *(*	kernel )(float *, unsigned int),
		int	blocks,
		int	threads,
		void *	arg1,
		unsigned int	arg2 )

ESBMC_verify_kernel__fuintint()

void ESBMC_verify_kernel__fuintint	(	void *(*	kernel )(float *, unsigned int, int),
		int	blocks,
		int	threads,
		void *	arg1,
		unsigned int	arg2,
		int	arg3 )

ESBMC_verify_kernel__fuintt()

void ESBMC_verify_kernel__fuintt	(	void *(*	kernel )(float *, unsigned int, unsigned int),
		int	blocks,
		int	threads,
		void *	arg1,
		unsigned int	arg2,
		unsigned int	arg3 )

ESBMC_verify_kernel__intt()

void ESBMC_verify_kernel__intt	(	void *(*	kernel )(int *, int),
		int	blocks,
		int	threads,
		void *	arg1,
		int	arg2 )

ESBMC_verify_kernel_c() [1/3]

template<class RET, class BLOCK, class THREAD, class T1>

void ESBMC_verify_kernel_c	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg )

ESBMC_verify_kernel_c() [2/3]

template<class RET, class BLOCK, class THREAD, class T1, class T2>

void ESBMC_verify_kernel_c	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg,
		T2	arg2 )

ESBMC_verify_kernel_c() [3/3]

template<class RET, class BLOCK, class THREAD, class T1, class T2, class T3>

void ESBMC_verify_kernel_c	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg,
		T2	arg2,
		T3	arg3 )

ESBMC_verify_kernel_c3()

void ESBMC_verify_kernel_c3	(	void *(*	kernel )(char *, char *, char *),
		int	blocks,
		int	threads,
		void *	arg1,
		void *	arg2,
		void *	arg3 )

ESBMC_verify_kernel_d1()

void ESBMC_verify_kernel_d1	(	void *(*	kernel )(double *),
		int	blocks,
		int	threads,
		void *	arg1 )

ESBMC_verify_kernel_d2()

void ESBMC_verify_kernel_d2	(	void *(*	kernel )(double, int),
		int	blocks,
		int	threads,
		double	arg1,
		int	arg2 )

ESBMC_verify_kernel_f() [1/3]

template<class RET, class BLOCK, class THREAD, class T1>

void ESBMC_verify_kernel_f	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg )

ESBMC_verify_kernel_f() [2/3]

template<class RET, class BLOCK, class THREAD, class T1, class T2>

void ESBMC_verify_kernel_f	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg,
		T2	arg2 )

ESBMC_verify_kernel_f() [3/3]

template<class RET, class BLOCK, class THREAD, class T1, class T2, class T3, class T4, class T5, class T6, class T7>

void ESBMC_verify_kernel_f	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg,
		T2	arg2,
		T3	arg3,
		T4	arg4,
		T5	arg5,
		T6	arg6,
		T7	arg7 )

ESBMC_verify_kernel_f5i2()

void ESBMC_verify_kernel_f5i2	(	void *(*	kernel )(float *, float *, float *, float *, float *, int, int),
		int	blocks,
		int	threads,
		void *	arg1,
		void *	arg2,
		void *	arg3,
		void *	arg4,
		void *	arg5,
		int	arg6,
		int	arg7 )

ESBMC_verify_kernel_ffloat()

void ESBMC_verify_kernel_ffloat	(	void *(*	kernel )(float *, float),
		int	blocks,
		int	threads,
		void *	arg1,
		float	arg2 )

ESBMC_verify_kernel_float()

void ESBMC_verify_kernel_float	(	void *(*	kernel )(float *),
		int	blocks,
		int	threads,
		void *	arg1 )

ESBMC_verify_kernel_four()

template<class RET, class BLOCK, class THREAD, class T1, class T2, class T3, class T4>

void ESBMC_verify_kernel_four	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg,
		T2	arg2,
		T3	arg3,
		T4	arg4 )

ESBMC_verify_kernel_fuintint() [1/2]

template<class RET, class BLOCK, class THREAD, class T1, class T2>

void ESBMC_verify_kernel_fuintint	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg,
		T2	arg2 )

ESBMC_verify_kernel_fuintint() [2/2]

template<class RET, class BLOCK, class THREAD, class T1, class T2, class T3>

void ESBMC_verify_kernel_fuintint	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg,
		T2	arg2,
		T3	arg3 )

ESBMC_verify_kernel_fuintt() [1/2]

template<class RET, class BLOCK, class THREAD, class T1, class T2>

void ESBMC_verify_kernel_fuintt	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg,
		T2	arg2 )

ESBMC_verify_kernel_fuintt() [2/2]

template<class RET, class BLOCK, class THREAD, class T1, class T2, class T3>

void ESBMC_verify_kernel_fuintt	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg,
		T2	arg2,
		T3	arg3 )

ESBMC_verify_kernel_i()

template<class RET, class BLOCK, class THREAD, class T1, class T2>

void ESBMC_verify_kernel_i	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg,
		T2	arg2 )

ESBMC_verify_kernel_intt()

template<class RET, class BLOCK, class THREAD, class T1, class T2>

void ESBMC_verify_kernel_intt	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg,
		T2	arg2 )

ESBMC_verify_kernel_no_params()

void ESBMC_verify_kernel_no_params	(	void *(*	kernel )(),
		int	blocks,
		int	threads )

ESBMC_verify_kernel_one_ui()

void ESBMC_verify_kernel_one_ui	(	void *(*	kernel )(unsigned int *),
		int	blocks,
		int	threads,
		void *	arg1 )

ESBMC_verify_kernel_three_args_iuull()

template<class RET, class BLOCK, class THREAD, class T1, class T2, class T3>

void ESBMC_verify_kernel_three_args_iuull	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg,
		T2	arg2,
		T3	arg3 )

ESBMC_verify_kernel_u() [1/3]

template<class RET, class BLOCK, class THREAD, class T1>

void ESBMC_verify_kernel_u	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg )

ESBMC_verify_kernel_u() [2/3]

template<class RET, class BLOCK, class THREAD, class T1, class T2>

void ESBMC_verify_kernel_u	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg,
		T2	arg2 )

ESBMC_verify_kernel_u() [3/3]

template<class RET, class BLOCK, class THREAD, class T1, class T2, class T3>

void ESBMC_verify_kernel_u	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg,
		T2	arg2,
		T3	arg3 )

ESBMC_verify_kernel_ui()

template<class RET, class BLOCK, class THREAD, class T1>

void ESBMC_verify_kernel_ui	(	RET *	kernel,
		BLOCK	blocks,
		THREAD	threads,
		T1	arg )

ESBMC_verify_kernel_with_four__args_i_ui_ull_f()

void ESBMC_verify_kernel_with_four__args_i_ui_ull_f	(	void *(*	kernel )(int *, unsigned int *, unsigned long long int *, float *),
		int	blocks,
		int	threads,
		void *	arg1,
		void *	arg2,
		void *	arg3,
		void *	arg4 )

ESBMC_verify_kernel_with_one_arg()

void ESBMC_verify_kernel_with_one_arg	(	void *(*	kernel )(int *),
		int	blocks,
		int	threads,
		void *	arg1 )

ESBMC_verify_kernel_with_one_args_u()

void ESBMC_verify_kernel_with_one_args_u	(	void *(*	kernel )(uint4 *),
		int	blocks,
		int	threads,
		void *	arg1 )

ESBMC_verify_kernel_with_three_args()

void ESBMC_verify_kernel_with_three_args	(	void *(*	kernel )(int *, int *, int *),
		int	blocks,
		int	threads,
		void *	arg1,
		void *	arg2,
		void *	arg3 )

ESBMC_verify_kernel_with_three_args_iuull()

void ESBMC_verify_kernel_with_three_args_iuull	(	void *(*	kernel )(int *, unsigned int *, unsigned long long int *),
		int	blocks,
		int	threads,
		void *	arg1,
		void *	arg2,
		void *	arg3 )

ESBMC_verify_kernel_with_three_args_u()

void ESBMC_verify_kernel_with_three_args_u	(	void *(*	kernel )(unsigned, unsigned, unsigned),
		int	blocks,
		int	threads,
		unsigned	arg1,
		unsigned	arg2,
		unsigned	arg3 )

ESBMC_verify_kernel_with_two_args()

void ESBMC_verify_kernel_with_two_args	(	void *(*	kernel )(int *, int *),
		int	blocks,
		int	threads,
		void *	arg1,
		void *	arg2 )

ESBMC_verify_kernel_with_two_args_i()

void ESBMC_verify_kernel_with_two_args_i	(	void *(*	kernel )(int, int),
		int	blocks,
		int	threads,
		int	arg1,
		int	arg2 )

ESBMC_verify_kernel_with_two_args_u()

void ESBMC_verify_kernel_with_two_args_u	(	void *(*	kernel )(unsigned int *, int *),
		int	blocks,
		int	threads,
		void *	arg1,
		void *	arg2 )

Variable Documentation

__cudaCurrentDevice

__thread int __cudaCurrentDevice = 0

__cudaDeviceCount

int __cudaDeviceCount = __cudaChooseDeviceCount()

blockGlobal

int blockGlobal

dev_c3

Targ_c3 dev_c3

dev_d1

Targ_d1 dev_d1

dev_d2

Targ_d2 dev_d2

dev_f5i2

Targ_f5i2 dev_f5i2

dev_ffloat

Targ_ffloat dev_ffloat

dev_fint

Targ_fint dev_fint

dev_float

Targ_float dev_float

dev_four_i_ui_ull_f

Targ_i_ui_ull_f dev_four_i_ui_ull_f

dev_fuint

Targ_fuint dev_fuint

dev_fuintint

Targ_fuintint dev_fuintint

dev_fuintt

Targ_fuintt dev_fuintt

dev_intt

Targ_intt dev_intt

dev_no_params

Targ_no_params dev_no_params

dev_one

Targ1 dev_one

dev_one_u

Targ_u1 dev_one_u

dev_three

Targ dev_three

dev_three_iuull

Targ_iuull dev_three_iuull

dev_three_u

Targ_u3 dev_three_u

dev_two

Targ2 dev_two

dev_two_i

Targ2_i dev_two_i

dev_two_u

Targ_u2 dev_two_u

dev_ui

Targ1_ui dev_ui

n_threads

unsigned int n_threads

threadGlobal

int threadGlobal