diffblue / cbmc

C Bounded Model Checker
https://diffblue.github.io/cbmc
Other
816 stars 258 forks source link

CodeQL reports potential double free in XML parser #8262

Open tautschnig opened 4 months ago

tautschnig commented 4 months ago

https://github.com/diffblue/cbmc/security/code-scanning/4 reports a double free without giving a detailed example or trace. Trying to reproduce a free at source line 1235 on Ubuntu 22.04 (Bison 3.8.2) is failing for me for that line is just blank. It is still possible that CodeQL is right for the XML parser does use free in a couple of places. Likely requires setting up CodeQL CLI to reproduce with local source code.

kroening commented 4 months ago

It's in this rule: attribute : NAME EQ VALUE { xml_parser.current().set_attribute( xmlt::unescape($1), xmlt::unescape($3)); free($1); free($3);} ; xmlt::unescape takes an std::string, so copies. Tough to see where the double-free happens. It may well be the case that CodeQL can't distinguish $1 from $3.