Replies: 1 comment
-
In our latest ESBMC prefixed: __ESBMC_get_thread_id, it starts at 0. esbmc/src/cpp/library/CUDA/device_launch_parameters.h Lines 49 to 50 in 083f5af I think in OM we might get a negative index. Also, if we used another thread to run the program, would the values for I observe that the approach we use is: It uses a thread to call a method, but in OM will our define and values be re-run in a new thread? |
Beta Was this translation helpful? Give feedback.
0 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
On the ESBMC-GPU website, it gives the following example code:
I think something is wrong with this code. First, N (the number of threads) is 2, so tid ranges from 0 to 1.
int size = N*sizeof(int);
array A also ranges from 0 to 1, which would cause an out-of-bounds problem if we used an offset of 2.
This example code I think needs to be changed?
Beta Was this translation helpful? Give feedback.
All reactions