Skip to content

Commit 151da10

Browse files
committed
Remove "WARNING: no body for function" regexes
These lines appear in the output for methods whose body is empty/nil. For excluded methods, we now have "return nondet" bodies as we do for stubs, so the warnings are no longer printed.
1 parent 3476187 commit 151da10

File tree

4 files changed

+0
-16
lines changed

4 files changed

+0
-16
lines changed

jbmc/regression/jbmc/context-include-exclude/test_exclude_from_all.desc

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,6 @@ Main.class
66
.* line 10 assertion at file Main.java line 10 .*: SUCCESS
77
.* line 11 assertion at file Main.java line 11 .*: SUCCESS
88
.* line 12 assertion at file Main.java line 12 .*: FAILURE
9-
WARNING: no body for function java::org\.cprover\.MyClass\$Inner\.doIt:\(I\)I
109
--
11-
WARNING: no body for function .*clinit_wrapper
12-
WARNING: no body for function java::org\.cprover\.MyClass\.<init>:\(I\)V
13-
WARNING: no body for function java::org\.cprover\.MyClass\.get:\(\)I
14-
WARNING: no body for function java::Main\.myMethod:\(I\)I
1510
--
1611
Tests that no methods except those in the specified class are excluded.

jbmc/regression/jbmc/context-include-exclude/test_exclude_from_include.desc

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -6,12 +6,7 @@ Main.class
66
.* line 10 assertion at file Main.java line 10 .*: FAILURE
77
.* line 11 assertion at file Main.java line 11 .*: SUCCESS
88
.* line 12 assertion at file Main.java line 12 .*: FAILURE
9-
WARNING: no body for function java::Main\.myMethod:\(I\)I
10-
WARNING: no body for function java::org\.cprover\.MyClass\$Inner\.doIt:\(I\)I
119
--
12-
WARNING: no body for function .*clinit_wrapper
13-
WARNING: no body for function java::org\.cprover\.MyClass\.<init>:\(I\)V
14-
WARNING: no body for function java::org\.cprover\.MyClass\.get:\(\)I
1510
--
1611
Tests that only the specified methods and classes are included, while
1712
the inner class from MyClass is excluded.

jbmc/regression/jbmc/context-include-exclude/test_include.desc

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,6 @@ Main.class
66
.* line 10 assertion at file Main.java line 10 .*: SUCCESS
77
.* line 11 assertion at file Main.java line 11 .*: FAILURE
88
.* line 12 assertion at file Main.java line 12 .*: FAILURE
9-
WARNING: no body for function java::org\.cprover\.MyClass\.<init>:\(I\)V
10-
WARNING: no body for function java::org\.cprover\.MyClass\.get:\(\)I
11-
WARNING: no body for function java::org\.cprover\.MyClass\$Inner\.doIt:\(I\)I
129
--
13-
WARNING: no body for function .*clinit_wrapper
14-
WARNING: no body for function java::Main\.myMethod:\(I\)I
1510
--
1611
Tests that only methods from the specified class are included.

jbmc/regression/jbmc/context-include-exclude/test_include_all.desc

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,5 @@ Main.class
77
.* line 11 assertion at file Main.java line 11 .*: SUCCESS
88
.* line 12 assertion at file Main.java line 12 .*: SUCCESS
99
--
10-
WARNING: no body for function .*
1110
--
1211
Tests that no methods are excluded.

0 commit comments

Comments
 (0)