Merge pull request #57 from peterschrammel/improve-jbmc-readme

Improve JBMC readme

Author: peterschrammel

Makefile

@@ -1,7 +1,6 @@
 CBMC=../cbmc
 2LS=../2ls
 JBMC=../cbmc
-YEAR=2019
 
 all: cbmc 2ls jbmc
 
@@ -65,10 +64,11 @@ jbmc.zip: jbmc.inc tool-wrapper.inc $(JBMC)/LICENSE $(JBMC)/jbmc/src/jbmc/jbmc $
 	$(MAKE) jbmc-wrapper
 	mv jbmc-wrapper $(basename $@)/jbmc
 	./sv-comp-readme.sh $(basename $@) > $(basename $@)/README
-	cp -L $(JBMC)/LICENSE $(basename $@)/
+	cp -L $(JBMC)/LICENSE $(basename $@)/LICENSE-for-JBMC
+	cp -L $(JBMC)/jbmc/lib/java-models-library/OpenJDK\ \ GPLv2\ +\ Classpath\ Exception.txt $(basename $@)/LICENSE-for-core-models
 	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 README
+	cd $(basename $@) && rm jbmc jbmc-binary core-models.jar LICENSE-for-core-models LICENSE-for-JBMC README
 	rmdir $(basename $@)

sv-comp-readme.sh

@@ -76,20 +76,28 @@ 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
+elif [ x$TOOL != xjbmc ]
+then
   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
+else
+  cat <<EOF
+
+To use the tool, run the tool passing a class or jar file as argument.
+Compile sources with Java 8. Using -g is recommended to obtain more
+readable counterexample traces.
+EOF
 fi
 
 cat <<EOF
 
 For SV-COMP, use the wrapper script provided in this distribution, which takes
 the following options:
-
+  <path(s)> to sources
   --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>