diff --git a/jbmc/regression/jbmc/generic_static_field/test.desc b/jbmc/regression/jbmc/generic_static_field/check_static_field_use.desc similarity index 75% rename from jbmc/regression/jbmc/generic_static_field/test.desc rename to jbmc/regression/jbmc/generic_static_field/check_static_field_use.desc index f341a759e93..656e5c342f3 100644 --- a/jbmc/regression/jbmc/generic_static_field/test.desc +++ b/jbmc/regression/jbmc/generic_static_field/check_static_field_use.desc @@ -1,6 +1,6 @@ CORE Test.class ---function Test.test --validate-goto-model --show-goto-functions +--function Test.test --show-goto-functions ^EXIT=0$ ^SIGNAL=0$ Test\.test:\(\)LTest;#return_value = static_field; @@ -8,8 +8,8 @@ Test\.test:\(\)LTest;#return_value = static_field; ^warning: ignoring -- This checks that the return value type matches the static field -- if it didn't, -either --validate-goto-model would throw because of a mismatching assignment, or -a cast would be used to adjust the type. +either --validate-goto-model would throw because of a mismatching assignment (checked +in ensure_runs.desc), or a cast would be used to adjust the type. The original motivation for this test was that generic field references could accidentally omit generic arguments that were present in function types. diff --git a/jbmc/regression/jbmc/generic_static_field/ensure_runs.desc b/jbmc/regression/jbmc/generic_static_field/ensure_runs.desc new file mode 100644 index 00000000000..d39f620ddc2 --- /dev/null +++ b/jbmc/regression/jbmc/generic_static_field/ensure_runs.desc @@ -0,0 +1,10 @@ +CORE +Test.class +--function Test.test --validate-goto-model +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +This just checks the generated GOTO passes validation; the main test is in check_static_field_use.desc