C++ front-end is broken since ESBMC v3.0

[lucasccordeiro]

If we run ~/esbmc-private/src/esbmc/esbmc double-linked-list.cpp double-linked-list_app.cpp -I ~/esbmc-private/src/cpp/library/, ESBMC reports:

Generating GOTO Program
GOTO program creation time: 0.953s
GOTO program processing time: 0.053s
No solver specified; defaulting to Boolector
Starting Bounded Model Checking
Symbolic type id in type_byte_size
symbol
- symbol_name : cpp::tag.node
  Aborted (core dumped)

The C++ front-end seems to be completely broken since ESBMC v3.0. Is it related to some refactoring about structs/unions?

Here are the files:

//double-linked-list.cpp
# include <iostream>
# include <cassert>
# include "double-linked-list.h"

using namespace std;

mlist::mlist(node\* h) : head(h)
{
    cout << "List is being created" << endl;
    head=NULL;
}

node\* mlist::search_node(int k)
{
    node\* l = new node();
    l=head;
    while(l!=NULL && l->key!=k)
    {
        l = l->next;
    }
    return l;
}

int mlist::delete_node(node *l)
{
    if (l->previous!=NULL)
        l->previous->next = l->next;
    else
        head = l->next;


if (l->next!=NULL)
    l->next->previous=l->previous;

return 0;


}

int mlist::insert_node(int k)
{
    node\* tmp = new node();
    tmp->key = k;
    tmp->next = head;
    if (head!=NULL)
        head->previous =tmp;
    head = tmp;
    tmp->previous = NULL;


return 0;


}

node\* mlist::get_head()
{
    return head;
}

//double-linked-list_app.cpp
# include <iostream>
# include <cassert>
# include "double-linked-list.h"

using namespace std;

int main(void){

mlist *mylist = new mlist(NULL);

mylist->insert_node(2);
mylist->insert_node(5);
mylist->insert_node(1);
mylist->insert_node(3);

node *temp = mylist->get_head();

cout << "list all elements: " << endl;

while(temp)
{
    cout << temp->key << endl;
    temp = temp->next;
}

temp = mylist->search_node(2);
cout << "search for element 2: " << (temp->key == 2 ? "found" : "not found") << endl;
assert(temp->key == 2);

mylist->delete_node(temp);

temp = mylist->get_head();

cout << "list all elements except 2: " << endl;
while(temp)
{
    cout << temp->key << endl;
    temp = temp->next;
}
}

[jmorse]

I haven't touched the C++ frontend in a year, and not seriously in two; would you mind giving this an eyeball first Mikhail?

[github-actions]

Stale issue message

[github-actions]

Stale issue message