[clang-cpp-14] Support variable template specialization

esbmc · Mar 18, 2024 · 9a5f374 · 9a5f374
1 parent 68a0dc9
commit 9a5f374
Show file tree

Hide file tree

Showing 6 changed files with 41 additions and 0 deletions.
diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
@@ -114,6 +114,9 @@ set(REGRESSIONS_CPP11 esbmc-cpp11/cpp
                       esbmc-cpp11/template
                       )
 
+# list of C++14 test suites
+set(REGRESSIONS_CPP14 esbmc-cpp14/template)
+
 # NOTE: In order to make the best of the concurrency set sort the tests from the slowest to fastest.
 if(APPLE)
     set(REGRESSIONS esbmc-unix
@@ -180,6 +183,7 @@ else()
                     ${REGRESSIONS_SMTLIB}
                     ${REGRESSIONS_Z3}
                     incremental-smt
+                    ${REGRESSIONS_CPP14}
                     ${REGRESSIONS_CPP11}
                     ${REGRESSIONS_CPP03}
                     ${REGRESSIONS_GOTO_CONTRACTOR}

diff --git a/regression/esbmc-cpp14/template/var-template-specialization-fail/main.cpp b/regression/esbmc-cpp14/template/var-template-specialization-fail/main.cpp
@@ -0,0 +1,12 @@
+#include <assert.h>
+
+template <typename>
+int a;
+
+int main()
+{
+  a<int> = 2;
+  a<double> = 3;
+  assert(a<int> == 3);
+  assert(a<double> == 4);
+}
diff --git a/regression/esbmc-cpp14/template/var-template-specialization-fail/test.desc b/regression/esbmc-cpp14/template/var-template-specialization-fail/test.desc
@@ -0,0 +1,5 @@
+CORE
+main.cpp
+--cppstd 14
+
+^VERIFICATION FAILED$
diff --git a/regression/esbmc-cpp14/template/var-template-specialization/main.cpp b/regression/esbmc-cpp14/template/var-template-specialization/main.cpp
@@ -0,0 +1,14 @@
+#include <assert.h>
+
+template <typename>
+int a;
+
+int main()
+{
+  a<int> = 2;
+  a<double> = 42;
+  assert(a<int> == 2);
+  assert(a<int> != 42);
+  assert(a<double> == 42);
+  assert(a<double> != 2);
+}
diff --git a/regression/esbmc-cpp14/template/var-template-specialization/test.desc b/regression/esbmc-cpp14/template/var-template-specialization/test.desc
@@ -0,0 +1,5 @@
+CORE
+main.cpp
+--cppstd 14
+
+^VERIFICATION SUCCESSFUL$
diff --git a/src/clang-c-frontend/clang_c_convert.cpp b/src/clang-c-frontend/clang_c_convert.cpp
@@ -116,6 +116,7 @@ bool clang_c_convertert::get_decl(const clang::Decl &decl, exprt &new_expr)
 
   // Declaration of variables
   case clang::Decl::Var:
+  case clang::Decl::VarTemplateSpecialization:
   {
     const clang::VarDecl &vd = static_cast<const clang::VarDecl &>(decl);
     return get_var(vd, new_expr);