Merge pull request #49 from tautschnig/readme

Include a README in the zip archive

Author: peterschrammel

Makefile

@@ -20,52 +20,55 @@ 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 README.cbmc-path.txt
+cbmc-path.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC)/src/goto-cc/goto-cc sv-comp-readme.sh
 	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
+	./sv-comp-readme.sh $(basename $@) > $(basename $@)/README
 	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 README.txt
+	cd $(basename $@) && rm cbmc cbmc-binary goto-cc LICENSE README
 	rmdir $(basename $@)
 
-cbmc.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC)/src/goto-cc/goto-cc
+cbmc.zip: cbmc.inc tool-wrapper.inc $(CBMC)/LICENSE $(CBMC)/src/cbmc/cbmc $(CBMC)/src/goto-cc/goto-cc sv-comp-readme.sh
 	mkdir -p $(basename $@)
 	$(MAKE) cbmc-wrapper
 	mv cbmc-wrapper $(basename $@)/cbmc
+	./sv-comp-readme.sh $(basename $@) > $(basename $@)/README
 	cp -L $(CBMC)/LICENSE $(basename $@)/
 	cp -L $(CBMC)/src/cbmc/cbmc $(basename $@)/cbmc-binary
 	cp -L $(CBMC)/src/goto-cc/goto-cc $(basename $@)/
 	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
 	rmdir $(basename $@)
 
-2ls.zip: 2ls.inc tool-wrapper.inc $(2LS)/LICENSE $(2LS)/src/2ls/2ls $(2LS)/cbmc/src/goto-cc/goto-cc
+2ls.zip: 2ls.inc tool-wrapper.inc $(2LS)/LICENSE $(2LS)/src/2ls/2ls $(2LS)/cbmc/src/goto-cc/goto-cc sv-comp-readme.sh
 	mkdir -p $(basename $@)
 	$(MAKE) 2ls-wrapper
 	mv 2ls-wrapper $(basename $@)/2ls
+	./sv-comp-readme.sh $(basename $@) > $(basename $@)/README
 	cp -L $(2LS)/LICENSE $(basename $@)/
 	cp -L $(2LS)/src/2ls/2ls $(basename $@)/2ls-binary
 	cp -L $(2LS)/cbmc/src/goto-cc/goto-cc $(basename $@)/
 	chmod a+rX $(basename $@)/*
 	zip -r $@ $(basename $@)
-	cd $(basename $@) && rm 2ls 2ls-binary goto-cc LICENSE
+	cd $(basename $@) && rm 2ls 2ls-binary goto-cc LICENSE README
 	rmdir $(basename $@)
 
-jbmc.zip: jbmc.inc tool-wrapper.inc $(JBMC)/LICENSE $(JBMC)/jbmc/src/jbmc/jbmc $(JBMC)/jbmc/lib/java-models-library/target/core-models.jar
+jbmc.zip: jbmc.inc tool-wrapper.inc $(JBMC)/LICENSE $(JBMC)/jbmc/src/jbmc/jbmc $(JBMC)/jbmc/lib/java-models-library/target/core-models.jar sv-comp-readme.sh
 	mkdir -p $(basename $@)
 	$(MAKE) jbmc-wrapper
 	mv jbmc-wrapper $(basename $@)/jbmc
+	./sv-comp-readme.sh $(basename $@) > $(basename $@)/README
 	cp -L $(JBMC)/LICENSE $(basename $@)/
 	cp -L $(JBMC)/jbmc/src/jbmc/jbmc $(basename $@)/jbmc-binary
 	cp -L $(JBMC)/jbmc/lib/java-models-library/target/core-models.jar $(basename $@)/
 	chmod a+rX $(basename $@)/*
 	zip -r $@ $(basename $@)
-	cd $(basename $@) && rm jbmc jbmc-binary core-models.jar LICENSE
+	cd $(basename $@) && rm jbmc jbmc-binary core-models.jar LICENSE README
 	rmdir $(basename $@)

sv-comp-readme.sh

@@ -0,0 +1,96 @@
+#!/bin/bash
+
+CONFIG=$1
+
+case $CONFIG in
+  2ls)
+    TOOL=2ls
+    REPO=2ls
+    ;;
+  cbmc|cbmc-path)
+    TOOL=cbmc
+    REPO=cbmc
+    ;;
+  jbmc)
+    TOOL=jbmc
+    REPO=cbmc
+    ;;
+  *)
+    echo "Unknown configuration $CONFIG" 1>&2
+    exit 1
+    ;;
+esac
+
+cat <<EOF
+CPROVER is a framework of software analysis tools. See https://www.cprover.org/
+for further information about the tools, publications, and the pointers to
+source code.
+
+This archive contains the following files:
+
+EOF
+
+if [ x$TOOL != xjbmc ]
+then
+  cat <<EOF
+- goto-cc: this C compiler transforms input files into so-called
+  "goto-binaries," which are encoded in CBMC's intermediate representation.
+
+- $TOOL-binary: this is the actual verification tool. It takes a goto-binary or
+  source code as input and checks the properties specified by command-line
+  flags.
+
+- $TOOL: this wrapper script invokes $TOOL-binary and goto-cc, parsing the
+  property file to pass the correct flags to $TOOL-binary and returning the
+  correct return codes for SV-COMP.
+EOF
+else
+  cat <<EOF
+- jbmc-binary: this is the actual verification tool. It takes Java bytecode
+  (class files) as input and checks the properties specified by command-line
+  flags.
+
+- jbmc: this wrapper script invokes jbmc-binary, parsing the property file to
+  pass the correct flags to jbmc-binary and returning the correct return codes
+  for SV-COMP.
+EOF
+fi
+
+cat <<EOF
+
+The binaries were compiled on $(lsb_release -d -s); 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/$REPO
+EOF
+
+if [ x$CONFIG = xcbmc-path ]
+then
+  cat <<EOF
+
+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`.
+
+EOF
+else
+  cat <<EOF
+
+To use the tool, run the tool passing a source file as argument. For C source
+code, and as only installation requirement, make sure a C compiler (such as GCC)
+is installed.
+EOF
+fi
+
+cat <<EOF
+
+For SV-COMP, use the wrapper script provided in this distribution, which takes
+the following options:
+
+  --32 or --64: set the bit width
+  --propertyfile <file>: read SV-COMP property specification from <file>
+  --graphml-witness <file>: write SV-COMP witness to <file>
+EOF