Skip to content

Commit 35f69f0

Browse files
Remove GOTO_CHECK options from JBMC
1 parent 86d4fec commit 35f69f0

File tree

8 files changed

+6
-8
lines changed

8 files changed

+6
-8
lines changed

jbmc/regression/jbmc/NullPointer1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
NullPointer1.class
3-
--pointer-check --stop-on-fail
3+
--stop-on-fail
44
^EXIT=10$
55
^SIGNAL=0$
66
^ file NullPointer1.java line 16 function java::NullPointer1.main:\(\[Ljava/lang/String;\)V bytecode-index 9$

jbmc/regression/jbmc/NullPointer2/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
NullPointer2.class
3-
--pointer-check --stop-on-fail
3+
--stop-on-fail
44
^EXIT=10$
55
^SIGNAL=0$
66
^ file NullPointer2.java line 9 function java::NullPointer2.main:\(\[Ljava/lang/String;\)V

jbmc/regression/jbmc/NullPointer3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
NullPointer3.class
3-
--pointer-check
3+
44
^EXIT=10$
55
^SIGNAL=0$
66
^.*Null pointer check: FAILURE$

jbmc/regression/jbmc/NullPointer4/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
NullPointer4.class
3-
--pointer-check --stop-on-fail
3+
--stop-on-fail
44
^EXIT=10$
55
^SIGNAL=0$
66
^ file NullPointer4.java line 6 function java::NullPointer4.main:\(\[Ljava/lang/String;\)V bytecode-index 4$

jbmc/regression/jbmc/pointer_check1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
pointer_check1.class
3-
--pointer-check
3+
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

jbmc/regression/jbmc/static_method1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
static_method1.class
3-
--function 'static_method1.f' --div-by-zero-check
3+
--function 'static_method1.f'
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

jbmc/src/jbmc/jbmc_parse_options.cpp

-1
Original file line numberDiff line numberDiff line change
@@ -1098,7 +1098,6 @@ void jbmc_parse_optionst::help()
10981098
HELP_SHOW_CLASS_HIERARCHY
10991099
"\n"
11001100
"Program instrumentation options:\n"
1101-
HELP_GOTO_CHECK
11021101
" --no-assertions ignore user assertions\n"
11031102
" --no-assumptions ignore user assumptions\n"
11041103
" --error-label label check that label is unreachable\n"

jbmc/src/jbmc/jbmc_parse_options.h

-1
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,6 @@ class optionst;
4747
"(document-subgoals)(outfile):" \
4848
"(object-bits):" \
4949
"(classpath):(cp):(main-class):" \
50-
OPT_GOTO_CHECK \
5150
"(no-assertions)(no-assumptions)" \
5251
"(no-built-in-assertions)" \
5352
"(xml-ui)(json-ui)" \

0 commit comments

Comments
 (0)