Skip to content
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

Symbol::as_z3_symbol can return Null Pointer #235

Open
Pat-Lafon opened this issue Apr 12, 2023 · 1 comment
Open

Symbol::as_z3_symbol can return Null Pointer #235

Pat-Lafon opened this issue Apr 12, 2023 · 1 comment

Comments

@Pat-Lafon
Copy link
Contributor

It seem like the integer conversion for Symbol does not check that the integer is within the valid bounds that Z3_mk_int_symbol expects(0 <= 2^30 -1). If you try to create a symbol with u32::MAX for example then any of the functions that use a symbol via as_z3_symbol will be using a null pointer.

I'm not sure what bad things can happen because of this, I think some of the usual cases do get caught or just have other operations return null as well.

#[test]
fn test() {
    let cfg = crate::Config::new();
    let ctx = Context::new(&cfg);
    println!("{}", crate::ast::Bool::new_const(&ctx, u32::MAX).to_string());
}
@Pat-Lafon
Copy link
Contributor Author

In doing some more digging, I see that Z3 tries to warn the user about this but in #92 we disabled the error handler and don't otherwise try to detect this situation.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant