[C++ VERIFICATION] Improved cpp new and delete

[XLiZHI]

Fixed C++ dangling pointer checking.

Fixed C++ double delete.

Next PR todo: move the adjustment of cpp new and delete into symex.

still wait for #1644

[lucasccordeiro]

I have two comments here.

[lucasccordeiro]

There is a memory leak in this program.

Can you please create another test case that enables --memory-leak-leak?

[lucasccordeiro]

Can you also create another test case that adds the delete to mark it as VERIFICATION SUCCESSFUL?

[fbrausse]

You can unify both branches by casting *code2 to the common base class const code_expression_data &. Otherwise LGTM.

[XLiZHI]

You can unify both branches by casting *code2 to the common base class const code_expression_data &. Otherwise LGTM.

Hi @fbrausse,

Thanks for your advice, I tried this, but cmake complained about it.

const code_expression_data &deref_code = is_code_cpp_delete2t(code2)? to_code_cpp_delete2t(code2)
                                                                    : to_code_cpp_del_array2t(code2);

different types ‘code_cpp_delete2t’ and ‘code_cpp_del_array2t’. Or do we have a general type cast function?

[fbrausse]

const auto &code_expr = static_cast<const code_expression_data &>(*code2); should work.

[XLiZHI]

const auto &code_expr = static_cast<const code_expression_data &>(*code2);

Great, thanks

[lucasccordeiro]

Thanks for submitting this PR, @XLiZHI.