[C++ Verification] Segfault verifying program containing `new`

[fbrausse]

I'm getting a segmentation fault when running ESBMC on

#include <memory>

int main()
{
	int *p = new int;
}

[lucasccordeiro]

@kunjsong01: @brcfarias will work on this issue. Is that okay for you?

[kunjsong01]

@lucasccordeiro sure, thanks

[lucasccordeiro]

I have assigned this issue to @brcfarias.

[brcfarias]

I have submitted a first part of the fix in #1045.

[lucasccordeiro]

Closed via https://github.com/esbmc/esbmc/pull/1045.

[brcfarias]

@kunjsong01, After merging #1045 we are crashing due to the abort() on this line It is possible to reproduce with the following snippet:

struct Foo {
  virtual void bar();
};

int main(void) {
    return 0;
}

If we don't declare the method as virtual the problem doesn't occur. Could you confirm wheter declaring as virtual should make difference considering that the definition is not avaiable?

[lucasccordeiro]

We could relax our constraints here.

GCC and Clang do not abort or give a warning message because The virtual method isn't pure virtual and hasn't a method implementation.

@kunjsong01: what do you think?

[kunjsong01]

We could relax our constraints here.

GCC and Clang do not abort or give a warning message because The virtual method isn't pure virtual and hasn't a method implementation.

@kunjsong01: what do you think?

sounds like the way to go, and worth a try.

BTW, @brcfarias just a quick confirmation regarding #include <memory> --- did you include the ESBMC's C++ operational models in the command? something like "-I <path_to_library>/library" where library refers to https://github.com/esbmc/esbmc/tree/master/src/cpp/library.

[brcfarias]

Did you include the ESBMC's C++ operational models in the command? something like "-I <path_to_library>/library"

I was not using this parameter.

[kunjsong01]

@brcfarias for C++ verification we usually use "-I <path_to_library>/library" so that we can use the ESBMC's C++ OMs instead of the original libraries

[fbrausse]

Reopening since the test case still doesn't pass. See also #1060.

[lucasccordeiro]

@brcfarias: can I ask you for the status of this issue?

[lucasccordeiro]

There is no segmentation fault now for this issue after integrating https://github.com/esbmc/esbmc/pull/1636.

@XLiZHI: can I ask you to check this issue? We might be missing the memory OM here.

[XLiZHI]

@XLiZHI: can I ask you to check this issue? We might be missing the memory OM here.

The issue is now in OM memory (PARSING ERROR) and I think we have two ways to resolve it, maintain it or use the standard library after improving the frontend.

[lucasccordeiro]

Many thanks, @XLiZHI.

We have a common agreement that we must improve our Clang C++ front end first. Let's focus on the issues that will enhance our Clang C++ frontend.

[XLiZHI]

fixed by #1685