CBMC front-end support on C++ template instantiation

[Sepideh Asadi]

Dear CBMC team,
I'm interested in verifying C++ with STL Containers via Predicate Abstraction, in particular the SATABS project in the earlier version of Cprover with tutorial C++ examples in http://www.cprover.org/stl/ .

I am wondering if SATABS functionalities are included in the new version of CBMC? Or is there any recent development to have support for C++ template specialization?

 According to the above link, it seems SATABS would give a concrete counterexample violating an assertion in the header file vector once "it" is dereferenced. That would be cool to identify such undefined behaviors in CBMC as well. 

I ran cbmc-5.52.0 on the following example from the SATABS webpage and got parsing errors:
#include <vector>
using namespace std;
int main()
{
  vector<int>::iterator it;
  {
        vector<int> vec;
        vec.push_back(0);
        it = vec.begin();
  }
  *it = 1;   // undefined behavior
}


Logs:
CBMC version 5.52.0 (cbmc-5.52.0-dirty) 64-bit x86_64 macos
line 0: parse error before '( ( ) )'
file /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/time.h line 172: parse error before '; __attribute__ ( ('
file /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/time.h line 202: parse error before '} typedef __darwin_wint_t wint_t'
file /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/c++/v1/type_traits line 466: parse error before 'class ... _Args >'
file /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/c++/v1/type_traits line 484: parse error before 'template < class ...'
file /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/c++/v1/type_traits line 513: parse error before 'class ... > false_type'
file /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/c++/v1/type_traits line 2664: parse error before ') ( _Param ...'
file /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/c++/v1/type_traits line 2680: parse error before ') ( _Param ...'
file /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/c++/v1/type_traits line 2684: parse error before '... ) ; }'
file /Library/Developer/CommandLineTools/SDKs/MacOSX.sdk/usr/include/c++/v1/type_traits line 2685: parse error before '} ; template <'
PARSING ERROR

Best regards,

Sepideh