Fixing inheritance issue for java programs.

CBMC was incorrectly stubbing inherited methods. This leads to such methods
being treated as non-det. The fix simply prevents CBMC from stubbing methods
that are inherited.

Author: Degiorgio

regression/Makefile

@@ -3,6 +3,7 @@ DIRS = ansi-c \
        cbmc \
        cpp \
        cbmc-java \
+       cbmc-java-inheritance \
        goto-analyzer \
        goto-instrument \
        goto-instrument-typedef \

regression/cbmc-java-inheritance/Makefile

@@ -0,0 +1,38 @@
+default: tests.log
+
+test:
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+tests.log: ../test.pl
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.java" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log
+
+%.class: %.java ../../src/org.cprover.jar
+	javac -g -cp ../../src/org.cprover.jar:. $<
+
+nondet_java_files := $(shell find . -name "Nondet*.java")
+nondet_class_files := $(patsubst %.java, %.class, $(nondet_java_files))
+
+.PHONY: nondet-class-files
+nondet-class-files: $(nondet_class_files)
+
+.PHONY: clean-nondet-class-files
+clean-nondet-class-files:
+	-rm $(nondet_class_files)

regression/cbmc-java-inheritance/inheritance01/A.class

@@ -0,0 +1,5 @@
+CORE
+test.class
+--function test.check
+^EXIT=0$
+^SIGNAL=0$

regression/cbmc-java-inheritance/inheritance01/B.class

@@ -0,0 +1,20 @@
+class A
+{
+  public int toInt()
+  {
+    return 12345;
+  }
+}
+
+class B extends A
+{
+}
+
+class test
+{
+  void check()
+  {
+    B b=new B();
+    assert(b.toInt()==12345);
+  }
+}