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;
}
}
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:
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: