ESBMC does not detect race conditions with floating points #1657
Replies: 4 comments 2 replies
-
|
It also does not work for int numbers |
Beta Was this translation helpful? Give feedback.
-
|
Thanks for this report, @SanjanaSai94. @XLiZHI: could you please check this issue? |
Beta Was this translation helpful? Give feedback.
-
|
Hi @SanjanaSai94 , Thanks for this issue. After my detailed investigation, the key point should be here: It returns when
Maybe you could try commenting
|
Beta Was this translation helpful? Give feedback.
-
|
@XLiZHI: It looks like ESBMC is facing some issues with guards for the Reachability Tree (RT) exploration. We should be able to detect this data-race because nondet_int can also return a @Anthonysdu: could you please check this issue? I'm almost sure that we've some issues with the guard generation for the RT exploration. |
Beta Was this translation helpful? Give feedback.
-
|
Hi @lucasccordeiro, But when seed_imput < 50, the assignment OUTPUT won't happen. I think ESBMC is working as expected. |
Beta Was this translation helpful? Give feedback.
-
|
Oh, I see. Then, I agree with your assessment here. |
Beta Was this translation helpful? Give feedback.
Uh oh!
There was an error while loading. Please reload this page.
-
I run ESBMC version 7.4.0 64-bit x86_64 windows and it was not able to detect race conditions for the attached code. also I added some assert(0) statements (line 215 and 228) in order to check that is possible to access the shared variable and it also cannot detect these assert(0). the code is a little simple, only two threads and does not have loops.
Please can you check.
Many thanks for the support.
main_float.txt
Beta Was this translation helpful? Give feedback.
All reactions