-
Notifications
You must be signed in to change notification settings - Fork 92
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
UB not tracked data-flow-wise #64
Comments
Still happens with master. |
The root cause of this is that we don't track UB in the data-flow, only in control-flow. This is fine for translation validation, but not sufficient for standalone alive. |
would it be bad to change the default to root-only, and make the other thing available as an option? |
I find that better UB printing will be very helpful for correctly understanding counter examples; when an input program is too large, what I can do is to just guess which operation raised UB from the values of registers... |
I don't know what the overhead would be; didn't try it out. |
If it is related with creation of a unique variable name, would it be helpful if the creation is done by alive2 rather than by Z3_mk_fresh_const? |
True, vcgen can take some time. The cost is basically track another expression per statement. Instead of just value & poison, we would need store UB as well. |
The text was updated successfully, but these errors were encountered: