jbmc-strings/ConstantEvaluationTrim: avoid null dereference

String refinement may or may not be successful (resulting in "ERROR"
results rather than "FAILURE") when working on an unconstrained string
(which the null dereference yields), depending on the models returned by
the SAT solver.

Author: tautschnig

jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.class

@@ -24,8 +24,10 @@ public void trimRight() {
     }
 
     public void noprop(String str) {
-        str = str.trim();
-        assert str.equals("abc");
+        if(str != null) {
+          str = str.trim();
+          assert str.equals("abc");
+        }
     }
 
     public void empty() {

jbmc/regression/jbmc-strings/ConstantEvaluationTrim/Main.java

@@ -2,6 +2,8 @@ CORE
 Main
 --function Main.noprop --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^Generated [1-9]\d* VCC\(s\), [1-9]\d* remaining after simplification$
+line 29 assertion at file Main.java line 29 .*: FAILURE$
+^\*\* 1 of \d+ failed
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$