The program below gives an error message that begins with "irep(...".
The programs compiles with g++. If replace the template type with `bool`, the program passes cbmc.
I'm using cbmc 6.8.0 on ubuntu 22.04.
Program:
```
template <typename T>
class vector {
private:
T* _data;
public:
vector( unsigned short num ) {
_data = new T[ num ];
}
};
template <typename T>
void buggy_rot( vector<T> xv )
{
}
int main()
{
vector<bool> xv0 = vector<bool>( 10 );
buggy_rot( xv0);
return 0;
}
```
Error message:
```
CBMC version 6.8.0 (cbmc-6.8.0) 64-bit x86_64 linux
Type-checking tmp
file tmp.cpp line 21 function main: function call expects function or function pointer as argument, but got 'irep("(\"cpp_declaration\" \"\" (\"cpp_declarator\" \"type\" (\"function_type\" \"\" (\"nil\") \"parameters\" (\"\" \"\" (\"cpp_declaration\" \"\" (\"cpp_declarator\" \"type\" (\"nil\") \"#source_location\" (\"nil\") \"value\" (\"nil\") \"name\" (\"cpp_name\" \"\" (\"name\" \"#source_location\" (\"\" \"file\" (\"tmp.cpp\") \"line\" (\"14\")) \"identifier\" (\"xv\")) \"#source_location\" (\"\" \"file\" (\"tmp.cpp\") \"line\" (\"14\"))) \"is_parameter\" (\"1\")) \"type\" (\"cpp_name\" \"\" (\"name\" \"#source_location\" (\"\" \"file\" (\"tmp.cpp\") \"line\" (\"14\")) \"identifier\" (\"vector\")) \"\" (\"template_args\" \"arguments\" (\"\" \"\" (\"ambiguous\" \"type\" (\"cpp_name\" \"\" (\"name\" \"#source_location\" (\"\" \"file\" (\"tmp.cpp\") \"line\" (\"14\")) \"identifier\" (\"T\")) \"#source_location\" (\"\" \"file\" (\"tmp.cpp\") \"line\" (\"14\"))) \"#source_location\" (\"\" \"file\" (\"tmp.cpp\") \"line\" (\"14\"))) \"#source_location\" (\"\" \"file\" (\"tmp.cpp\") \"line\" (\"14\")))) \"#source_location\" (\"\" \"file\" (\"tmp.cpp\") \"line\" (\"14\")))))) \"#source_location\" (\"nil\") \"value\" (\"code\" \"type\" (\"empty\") \"#source_location\" (\"\" \"file\" (\"tmp.cpp\") \"line\" (\"15\") \"function\" (\"buggy_rot\")) \"statement\" (\"block\")) \"name\" (\"cpp_name\" \"\" (\"name\" \"#source_location\" (\"\" \"file\" (\"tmp.cpp\") \"line\" (\"14\")) \"identifier\" (\"buggy_rot\")) \"#source_location\" (\"\" \"file\" (\"tmp.cpp\") \"line\" (\"14\")))) \"type\" (\"void\" \"#source_location\" (\"\" \"file\" (\"tmp.cpp\") \"line\" (\"14\"))) \"is_template\" (\"1\") \"template_type\" (\"template\" \"#source_location\" (\"\" \"file\" (\"tmp.cpp\") \"line\" (\"13\")) \"template_parameters\" (\"\" \"\" (\"type\" \"type\" (\"template_parameter_symbol_type\" \"#source_location\" (\"\" \"file\" (\"tmp.cpp\") \"line\" (\"13\")) \"identifier\" (\"template::1::T\"))))) \"storage_spec\" (\"cpp_storage_spec\") \"member_spec\" (\"\"))")'
CONVERSION ERROR
```
-mark