facebook / infer

A static analyzer for Java, C, C++, and Objective-C

http://fbinfer.com/

MIT License

14.8k stars 2k forks source link

[pulse] More normalization in BaseDomain and Formula #1751

Closed danielmercier closed 3 months ago

danielmercier commented 1 year ago

Normalize the conditions field from the path_condition according to the formula when normalizing it.

When canonicalizing the abductive state, also use var_repr for the pre state.

1750

jvillard commented 3 months ago

Thanks! The rest of pulse wasn't ready for this change at the time but now pulse normalises all abstract values on the fly, which in particular includes changes like this PR. Apologies for not incorporating this PR itself, that would have been tricky in the middle of all the changes. The particular false positive was fixed in 5d2d0c48aa9121a47c296d15da313c49404dc846. I believe we can close this.