unit tests for verilog_typename(...)

Author: kroening

unit/Makefile

@@ -11,6 +11,7 @@ SRC += smvlang/expr2smv.cpp \
        temporal-logic/sva_to_ltl.cpp \
        temporal-logic/nnf.cpp \
        temporal-logic/trivial_sva.cpp \
+       verilog/typename.cpp \
        # Empty last line
 
 INCLUDES= -I ../src/ -I . -I $(CPROVER_DIR)/unit -I $(CPROVER_DIR)/src

unit/verilog/typename.cpp

@@ -0,0 +1,23 @@
+/*******************************************************************\
+
+Module: $typename Unit Tests
+
+Author: Daniel Kroening, Amazon, dkr@amazon.com
+
+\*******************************************************************/
+
+#include <testing-utils/use_catch.h>
+#include <verilog/typename.h>
+#include <verilog/verilog_types.h>
+
+SCENARIO("$typename(...)")
+{
+  GIVEN("various Verilog types")
+  {
+    REQUIRE(verilog_typename(verilog_chandle_typet{}) == "chandle");
+    REQUIRE(verilog_typename(verilog_real_typet{}) == "real");
+    REQUIRE(
+      verilog_typename(verilog_signedbv_typet{10}) == "logic signed[9:0]");
+    REQUIRE(verilog_typename(verilog_shortreal_typet{}) == "shortreal");
+  }
+}