From 9078d1555fe120378a1575fd2a95133da7d86e9b Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 2 Aug 2017 18:14:42 +0100 Subject: [PATCH 1/2] Rename bytecode_index -> bytecodeIndex in JSON output JSON property names should use camelCase. --- regression/cbmc-java/NullPointer1/test.desc | 2 +- regression/cbmc-java/NullPointer4/test.desc | 2 +- regression/cbmc-java/enum1/test.desc | 2 +- .../putstatic_source_location/test.desc | 2 +- .../java_parseint_with_radix_knownbug/output | 8 ++++---- src/goto-instrument/cover.cpp | 16 ++++++++-------- src/util/json_expr.cpp | 2 +- src/util/source_location.cpp | 2 +- 8 files changed, 18 insertions(+), 18 deletions(-) diff --git a/regression/cbmc-java/NullPointer1/test.desc b/regression/cbmc-java/NullPointer1/test.desc index b11a57a56fd..64fd6a24f69 100644 --- a/regression/cbmc-java/NullPointer1/test.desc +++ b/regression/cbmc-java/NullPointer1/test.desc @@ -3,7 +3,7 @@ NullPointer1.class --pointer-check --stop-on-fail ^EXIT=10$ ^SIGNAL=0$ -^ file NullPointer1.java line 16 function java::NullPointer1.main:\(\[Ljava/lang/String;\)V bytecode_index 9$ +^ file NullPointer1.java line 16 function java::NullPointer1.main:\(\[Ljava/lang/String;\)V bytecode-index 9$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc-java/NullPointer4/test.desc b/regression/cbmc-java/NullPointer4/test.desc index 28c9e6f47fd..fbe3588bfff 100644 --- a/regression/cbmc-java/NullPointer4/test.desc +++ b/regression/cbmc-java/NullPointer4/test.desc @@ -3,7 +3,7 @@ NullPointer4.class --pointer-check --stop-on-fail ^EXIT=10$ ^SIGNAL=0$ -^ file NullPointer4.java line 6 function java::NullPointer4.main:\(\[Ljava/lang/String;\)V bytecode_index 4$ +^ file NullPointer4.java line 6 function java::NullPointer4.main:\(\[Ljava/lang/String;\)V bytecode-index 4$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/regression/cbmc-java/enum1/test.desc b/regression/cbmc-java/enum1/test.desc index 4c1fcafe076..eff2c2e6817 100644 --- a/regression/cbmc-java/enum1/test.desc +++ b/regression/cbmc-java/enum1/test.desc @@ -4,6 +4,6 @@ enum1.class ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ -^Unwinding loop java::enum1.:\(\)V.0 iteration 5 \(6 max\) file enum1.java line 6 function java::enum1.:\(\)V bytecode_index 78 thread 0$ +^Unwinding loop java::enum1.:\(\)V.0 iteration 5 \(6 max\) file enum1.java line 6 function java::enum1.:\(\)V bytecode-index 78 thread 0$ -- ^warning: ignoring diff --git a/regression/cbmc-java/putstatic_source_location/test.desc b/regression/cbmc-java/putstatic_source_location/test.desc index 131860ef72d..fdb85eb8ee7 100644 --- a/regression/cbmc-java/putstatic_source_location/test.desc +++ b/regression/cbmc-java/putstatic_source_location/test.desc @@ -3,4 +3,4 @@ test.class --show-goto-functions ^EXIT=0$ ^SIGNAL=0$ -test\.java line 5 function java::test.main:\(\)V bytecode_index 1 +test\.java line 5 function java::test.main:\(\)V bytecode-index 1 diff --git a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/output b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/output index e9cde4a8842..dfb2f48b2cf 100644 --- a/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/output +++ b/regression/strings-smoke-tests/java_parseint_with_radix_knownbug/output @@ -45,18 +45,18 @@ Runtime decision procedure: 0.386s [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.1] reference is null in *args: SUCCESS [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.2] reference is null in *new_tmp0: SUCCESS [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.3] reference is null in *new_tmp2: SUCCESS -[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.1] assertion at file test_parseint_with_radix.java line 9 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode_index 20: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.1] assertion at file test_parseint_with_radix.java line 9 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode-index 20: SUCCESS [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.null-pointer-exception.1] Throw null: SUCCESS [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.4] reference is null in *new_tmp3: SUCCESS -[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.2] assertion at file test_parseint_with_radix.java line 10 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode_index 29: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.2] assertion at file test_parseint_with_radix.java line 10 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode-index 29: SUCCESS [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.null-pointer-exception.2] Throw null: SUCCESS [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.5] reference is null in *args: SUCCESS [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.6] reference is null in *new_tmp4: SUCCESS [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.7] reference is null in *new_tmp6: SUCCESS -[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.3] assertion at file test_parseint_with_radix.java line 16 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode_index 52: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.3] assertion at file test_parseint_with_radix.java line 16 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode-index 52: SUCCESS [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.null-pointer-exception.3] Throw null: SUCCESS [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.pointer_dereference.8] reference is null in *new_tmp7: SUCCESS -[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.4] assertion at file test_parseint_with_radix.java line 17 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode_index 61: SUCCESS +[java::test_parseint_with_radix.main:([Ljava/lang/String;)V.assertion.4] assertion at file test_parseint_with_radix.java line 17 function java::test_parseint_with_radix.main:([Ljava/lang/String;)V bytecode-index 61: SUCCESS [java::test_parseint_with_radix.main:([Ljava/lang/String;)V.null-pointer-exception.4] Throw null: SUCCESS [pointer_dereference.7] reference is null in *this: SUCCESS [array-create-negative-size.1] Array size should be >= 0: SUCCESS diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index d482777c2ed..e91e309f919 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -145,27 +145,27 @@ bool coverage_goalst::get_coverage_goals( // ensure minimal requirements for a goal entry PRECONDITION( (!each_goal["goal"].is_null()) || - (!each_goal["sourceLocation"]["bytecode_index"].is_null()) || + (!each_goal["sourceLocation"]["bytecodeIndex"].is_null()) || (!each_goal["sourceLocation"]["file"].is_null() && !each_goal["sourceLocation"]["function"].is_null() && !each_goal["sourceLocation"]["line"].is_null())); - // check whether bytecode_index is provided for Java programs + // check whether bytecodeIndex is provided for Java programs if(mode==ID_java && - each_goal["sourceLocation"]["bytecode_index"].is_null()) + each_goal["sourceLocation"]["bytecodeIndex"].is_null()) { messaget message(message_handler); message.error() << coverage_file - << " file does not contain bytecode_index" + << " file does not contain bytecodeIndex" << messaget::eom; return true; } - if(!each_goal["sourceLocation"]["bytecode_index"].is_null()) + if(!each_goal["sourceLocation"]["bytecodeIndex"].is_null()) { - // get and set the bytecode_index + // get and set the bytecodeIndex irep_idt bytecode_index= - each_goal["sourceLocation"]["bytecode_index"].value; + each_goal["sourceLocation"]["bytecodeIndex"].value; source_location.set_java_bytecode_index(bytecode_index); } @@ -1509,7 +1509,7 @@ bool instrument_cover_goals( if(cmdline.isset("existing-coverage")) { // get the mode to ensure invariants - // (e.g., bytecode_index for Java programs) + // (e.g., bytecodeIndex for Java programs) namespacet ns(symbol_table); const irep_idt &mode=ns.lookup(goto_functions.entry_point()).mode; diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp index 4f5ce44d2fd..676c1940db0 100644 --- a/src/util/json_expr.cpp +++ b/src/util/json_expr.cpp @@ -95,7 +95,7 @@ json_objectt json(const source_locationt &location) result["function"]=json_stringt(id2string(location.get_function())); if(!location.get_java_bytecode_index().empty()) - result["bytecode_index"]= + result["bytecodeIndex"]= json_stringt(id2string(location.get_java_bytecode_index())); return result; diff --git a/src/util/source_location.cpp b/src/util/source_location.cpp index 57d266b2aa4..46f7f5282d9 100644 --- a/src/util/source_location.cpp +++ b/src/util/source_location.cpp @@ -56,7 +56,7 @@ std::string source_locationt::as_string(bool print_cwd) const { if(dest!="") dest+=' '; - dest+="bytecode_index "+id2string(bytecode); + dest+="bytecode-index "+id2string(bytecode); } return dest; From 5ff94dee8f8f40cf140dc14e7f162dc3cadfdd1e Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 2 Aug 2017 18:51:58 +0100 Subject: [PATCH 2/2] Use empty() --- src/analyses/goto_check.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 367b4e13893..26e1297256d 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1703,7 +1703,7 @@ void goto_checkt::goto_check( if(!it->source_location.get_column().empty()) i_it->source_location.set_column(it->source_location.get_column()); - if(it->source_location.get_java_bytecode_index()!=irep_idt()) + if(!it->source_location.get_java_bytecode_index().empty()) i_it->source_location.set_java_bytecode_index( it->source_location.get_java_bytecode_index()); }