Add the crangler tool

This is a command-line utility that makes changes to a preprocessed C file
that are prescribed in a JSON configuration file.

The initial set of transformations is as follows.
 * add a contract (pre/post/assigns) to a named C function
 * add a loop invariant to a loop identified by the name
   of the function its in and a loop number
 * remove the 'static' storage classifier from a function

The resulting source file is written to standard output or to file
specified in the JSON configuration.

Author: kroening

CMakeLists.txt

@@ -150,6 +150,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
               "$<TARGET_FILE:unit>"
               "$<TARGET_FILE:goto-harness>"
               "$<TARGET_FILE:cbmc>"
+              "$<TARGET_FILE:crangler>"
               "$<TARGET_FILE:driver>"
               "$<TARGET_FILE:goto-analyzer>"
               "$<TARGET_FILE:goto-cc>"
@@ -213,6 +214,8 @@ cprover_default_properties(
     cbmc
     cbmc-lib
     cpp
+    crangler
+    crangler-lib
     driver
     goto-analyzer
     goto-analyzer-lib

regression/CMakeLists.txt

@@ -83,3 +83,7 @@ if(WITH_MEMORY_ANALYZER)
   add_subdirectory(memory-analyzer)
   add_subdirectory(extract_type_header)
 endif()
+
+if(NOT WIN32)
+  add_subdirectory(crangler)
+endif()

regression/Makefile

@@ -3,6 +3,7 @@
 # listed with decreasing runtimes (i.e. longest running at the top)
 DIRS = cbmc \
        cbmc-library \
+       crangler \
        goto-analyzer \
        ansi-c \
        goto-instrument \

regression/crangler/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:crangler>"
+)

regression/crangler/Makefile

@@ -0,0 +1,27 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+ifeq ($(BUILD_ENV_),MSVC)
+test:
+
+tests.log:
+
+else
+test:
+	@../test.pl -e -p -c '../../../src/crangler/crangler'
+
+tests.log:
+	@../test.pl -e -p -c '../../../src/crangler/crangler'
+endif
+
+clean:
+	@for dir in *; do \
+		$(RM) tests.log; \
+		if [ -d "$$dir" ]; then \
+			cd "$$dir"; \
+			$(RM) *.out *.gb; \
+			cd ..; \
+		fi \
+	done

regression/crangler/remove-static/remove_static1.c

@@ -0,0 +1,14 @@
+int foo()
+{
+  return 0;
+}
+
+int bar();
+
+static void foobar1()
+{
+}
+
+void static foobar2()
+{
+}

regression/crangler/remove-static/remove_static1.desc

@@ -0,0 +1,8 @@
+CORE
+remove_static1.json
+
+^\s+void foobar1\(\)$
+^void\s+foobar2\(\)$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/crangler/remove-static/remove_static1.json

@@ -0,0 +1,18 @@
+{
+  "sources": [
+    "remove_static1.c"
+  ],
+  "functions": [
+    {
+      "foobar1": [
+        "remove static"
+      ]
+    },
+    {
+      "foobar2": [
+        "remove static"
+      ]
+    }
+  ],
+  "output": "stdout"
+}

src/CMakeLists.txt

@@ -106,6 +106,7 @@ add_subdirectory(statement-list)
 add_subdirectory(util)
 
 add_subdirectory(cbmc)
+add_subdirectory(crangler)
 add_subdirectory(goto-cc)
 add_subdirectory(goto-instrument)
 add_subdirectory(goto-analyzer)

src/Makefile

@@ -4,6 +4,7 @@ DIRS = analyses \
        big-int \
        cbmc \
        cpp \
+       crangler \
        goto-analyzer \
        goto-cc \
        goto-checker \
@@ -27,6 +28,7 @@ DIRS = analyses \
        # Empty last line
 
 all: cbmc.dir \
+     crangler.dir \
      goto-analyzer.dir \
      goto-cc.dir \
      goto-diff.dir \
@@ -59,6 +61,8 @@ $(patsubst %, %.dir, $(filter-out big-int util, $(DIRS))): util.dir
 
 cpp.dir: ansi-c.dir linking.dir
 
+crangler.dir: util.dir json.dir
+
 languages: util.dir langapi.dir \
            cpp.dir ansi-c.dir xmllang.dir assembler.dir \
            jsil.dir json.dir json-symtab-language.dir statement-list.dir