Merge pull request #48 from karkhaz/kk-cbmc-path-readme

Add README for CBMC Path

Author: tautschnig

Makefile

@@ -20,17 +20,18 @@ jbmc: jbmc.zip
 	cat $*.inc tool-wrapper.inc >> $@
 	chmod 755 $@
 
-cbmc-path.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC)/src/goto-cc/goto-cc
+cbmc-path.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC)/src/goto-cc/goto-cc README.cbmc-path.txt
 	mkdir -p $(basename $@)
 	$(MAKE) cbmc-wrapper
 	mv cbmc-wrapper $(basename $@)/cbmc
 	sed -i 's/^.\/cbmc-binary --graphml-witness/.\/cbmc-binary --paths fifo --graphml-witness/' $(basename $@)/cbmc
 	cp -L $(CBMC)/LICENSE $(basename $@)/
 	cp -L $(CBMC)/src/cbmc/cbmc $(basename $@)/cbmc-binary
 	cp -L $(CBMC)/src/goto-cc/goto-cc $(basename $@)/
+	cp -L README.cbmc-path.txt $(basename $@)/README.txt
 	chmod a+rX $(basename $@)/*
 	zip -r $@ $(basename $@)
-	cd $(basename $@) && rm cbmc cbmc-binary goto-cc LICENSE
+	cd $(basename $@) && rm cbmc cbmc-binary goto-cc LICENSE README.txt
 	rmdir $(basename $@)
 
 cbmc.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC)/src/goto-cc/goto-cc

README.cbmc-path.txt

@@ -0,0 +1,26 @@
+                           CBMC Path
+                           =========
+
+This archive contains the following files:
+
+- goto-cc: this C compiler transforms input files into so-called
+  `goto-binaries,' which are encoded in CBMC's intermediate representation.
+
+- cbmc-binary: this is the actual verification tool. It takes a goto-binary
+  as input and checks the properties specified by command-line flags.
+
+- cbmc: this wrapper script invokes cbmc-binary and goto-cc, parsing the
+  property file to pass the correct flags to cbmc-binary and returning the
+  correct return codes for SV-COMP.
+
+goto-cc and cbmc-binary were compiled on Debian 9 (stretch); the binaries
+should be self-hosting on similar operating systems.  The upstream URL, if
+you wish to compile it yourself, is https://github.com/diffblue/cbmc
+
+To run CBMC Path manually, you need to invoke the tool as
+
+    cbmc-binary --paths fifo ...
+
+which activates CBMC's path-exploration mode. Note that the tool will not
+terminate for input programs that contain loops unless you specify an
+unwinding limit using --unwind N. For other flags, see `cbmc-binary -h`.