Disable default pointer check (replaced by java_bytecode_instrument)

Also amend tests that are perturbed by this.

They used to require a specific goal marked as success, but when they become
simple enough that the simplifier solves the problem by itself the goal list is
not printed. Therefore just look for VERIFICATION SUCCESSFUL.

Also modify a test that was looking for a null pointer failure, since the
phrasing of them has changed.

Author: smowton

regression/cbmc-java/stack_var4/test.desc

@@ -3,8 +3,6 @@ stack_test.class
 
 ^EXIT=0$
 ^SIGNAL=0$
-^.*assertion at file stack_test.java line 5 function.*: SUCCESS
-$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc-java/stack_var5/test.desc

@@ -3,8 +3,6 @@ stack_test.class
 
 ^EXIT=0$
 ^SIGNAL=0$
-^.*assertion at file stack_test.java line 5 function.*: SUCCESS
-$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc-java/stack_var6/test.desc

@@ -3,8 +3,6 @@ stack_test.class
 
 ^EXIT=0$
 ^SIGNAL=0$
-^.*assertion at file stack_test.java line 5 function.*: SUCCESS
-$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc-java/stack_var7/test.desc

@@ -3,8 +3,6 @@ stack_test.class
 
 ^EXIT=0$
 ^SIGNAL=0$
-^.*assertion at file stack_test.java line 5 function.*: SUCCESS
-$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/strings/StaticCharMethods05/test.desc

@@ -3,7 +3,7 @@ StaticCharMethods05.class
 --refine-strings
 ^EXIT=10$
 ^SIGNAL=0$
-^\[pointer_dereference\.2\] reference is null in \*this->data: FAILURE$
+null-pointer-exception\.14\] Throw null: FAILURE
 ^\[.*assertion\.1\] .* line 12 .* FAILURE$
 ^\[.*assertion\.2\] .* line 22 .* FAILURE$
 ^VERIFICATION FAILED$

src/analyses/goto_check.cpp

@@ -909,7 +909,7 @@ void goto_checkt::pointer_validity_check(
   const exprt &access_ub,
   const irep_idt &mode)
 {
-  if(mode!=ID_java && !enable_pointer_check)
+  if(!enable_pointer_check)
     return;
 
   const exprt &pointer=expr.op0();