error message with "irep(...)" for function with template type arg

1 view
Skip to first unread message

Mark Aagaard

unread,
Feb 13, 2026, 1:47:42 PM (10 days ago) Feb 13
to CProver Support
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

Reply all
Reply to author
Forward
0 new messages