Verilog: introduce the Verilog indexer

This adds a recusive decent parser for quicky indexing large quantities of
Verilog, tolerating parsing errors, for the purpose of creating overview
data very quickly.  A new executable, vlindex, is added to output it.

regression/verilog/case/nested_case1.desc

@@ -0,0 +1,8 @@
+CORE
+nested_case1.v
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+^\[main.property.p1\] .* PROVED up to bound 0$
+--
+^warning: ignoring

regression/verilog/case/nested_case1.v

@@ -0,0 +1,17 @@
+module main(input x, input y);
+
+  reg result;
+
+  always @(x, y)
+    case(x)
+      0: result = 0;
+      1:
+        case(y)
+          1: result = 1;
+          0: result = 0;
+        endcase
+    endcase
+
+  always assert p1: result == (x && y);
+
+endmodule

src/Makefile

@@ -1,10 +1,10 @@
 DIRS = ebmc hw-cbmc temporal-logic trans-word-level trans-netlist \
-       verilog vhdl smvlang ic3 aiger
+       verilog vhdl smvlang ic3 aiger vlindex
 
 EBMC_DIR:=$(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
 CPROVER_DIR:=../lib/cbmc/src
 
-all: hw-cbmc.dir ebmc.dir
+all: hw-cbmc.dir ebmc.dir vlindex.dir
 
 .PHONY: $(patsubst %, %.dir, $(DIRS))
 $(patsubst %, %.dir, $(DIRS)):
@@ -21,6 +21,8 @@ ebmc.dir: trans-word-level.dir trans-netlist.dir verilog.dir vhdl.dir \
 hw-cbmc.dir: trans-word-level.dir trans-netlist.dir verilog.dir \
          vhdl.dir smvlang.dir cprover.dir temporal-logic.dir
 
+vlindex.dir: cprover.dir verilog.dir
+
 # building cbmc proper
 .PHONY: cprover.dir
 cprover.dir:

src/vlindex/Makefile

@@ -0,0 +1,26 @@
+SRC = \
+      verilog_indexer.cpp \
+      vlindex_main.cpp \
+      vlindex_parse_options.cpp \
+      #empty line
+
+OBJ+= $(CPROVER_DIR)/util/util$(LIBEXT) \
+      $(CPROVER_DIR)/langapi/langapi$(LIBEXT) \
+      $(CPROVER_DIR)/big-int/big-int$(LIBEXT) \
+      ../verilog/verilog$(LIBEXT)
+
+include ../config.inc
+include ../common
+
+CLEANFILES = vlindex$(EXEEXT)
+
+all: vlindex$(EXEEXT)
+
+ifdef DEBUG
+CXXFLAGS += -DDEBUG
+endif
+
+###############################################################################
+
+vlindex$(EXEEXT): $(OBJ)
+	$(LINKBIN)