diff --git a/regression/cbmc-java/invalid_classpath/test-jar.desc b/regression/cbmc-java/invalid_classpath/test-jar.desc index ad17341c1003..ad0200548564 100644 --- a/regression/cbmc-java/invalid_classpath/test-jar.desc +++ b/regression/cbmc-java/invalid_classpath/test-jar.desc @@ -1,7 +1,10 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure Test.class --classpath ./NotHere.jar ^EXIT=6$ ^SIGNAL=0$ ^the program has no entry point$ ^failed to load class `Test'$ +-- +-- +symex-driven lazy loading should emit "the program has no entry point" but currently doesn't diff --git a/regression/cbmc-java/invalid_classpath/test-path.desc b/regression/cbmc-java/invalid_classpath/test-path.desc index a9de00701264..282ae0209f87 100644 --- a/regression/cbmc-java/invalid_classpath/test-path.desc +++ b/regression/cbmc-java/invalid_classpath/test-path.desc @@ -1,7 +1,10 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure Test.class --classpath ./NotHere ^EXIT=6$ ^SIGNAL=0$ ^the program has no entry point$ ^failed to load class `Test'$ +-- +-- +symex-driven lazy loading should emit "the program has no entry point" but currently doesn't diff --git a/regression/cbmc-java/provide_object_implementation/test.desc b/regression/cbmc-java/provide_object_implementation/test.desc index 2edcd31244ec..381ae109d1e7 100644 --- a/regression/cbmc-java/provide_object_implementation/test.desc +++ b/regression/cbmc-java/provide_object_implementation/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure java/lang/Object.class ^EXIT=6$ @@ -6,3 +6,5 @@ java/lang/Object.class ^the program has no entry point$ -- ^failed to add class symbol java::java\.lang\.Object$ +-- +symex-driven lazy loading should emit "the program has no entry point" but currently doesn't