Skip to content

Conversation

Snezhkko
Copy link

Reason: Formatting function calls in counterexamples could dereference a null parameter pointer when a parameter is absent and no concrete value is available, leading to undefined behavior.

Change: Guard against null params.at(i) and use a safe fallback: prefer the parameter’s actual name when available, otherwise use the placeholder param_. The existing “counterexample incomplete” note remains unchanged.

Goal: Eliminate potential UB and make counterexample formatting robust. This aligns with existing null checks in nearby code (e.g., CHC.cpp, RenameSymbol.cpp) and follows existing placeholder naming (param_) used elsewhere. Tests pass.

Copy link

Thank you for your contribution to the Solidity compiler! A team member will follow up shortly.

If you haven't read our contributing guidelines and our review checklist before, please do it now, this makes the reviewing process and accepting your contribution smoother.

If you have any questions or need our help, feel free to post them in the PR or talk to us directly on the #solidity-dev channel on Matrix.

Copy link
Member

@clonker clonker left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is subtle but the first if statement contains params.at(i). This throws if i is not in the map and exits from the control flow. Therefore subsequent uses of the operator[] on params are safe. For function calls the pointers contained in params can't be null by virtue of how they are constructed in the solidity parser. There is no type-level guarantee for this of course. Did you encounter a null pointer in this anywhere?

@cameel cameel added the smt label Aug 29, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants