From 6d1feea66f519254515ade1c2b6fbce31a4af4d5 Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 20 Apr 2017 11:00:46 +0100 Subject: [PATCH 1/2] Set the bytecode index for the instrumentation in goto_check.cpp --- src/analyses/goto_check.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index cc418d6aed9..635e0eb8f9a 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1820,6 +1820,11 @@ void goto_checkt::goto_check( if(it->source_location.get_column()!=irep_idt()) i_it->source_location.set_column(it->source_location.get_column()); + + if(mode==ID_java && + it->source_location.get_java_bytecode_index()!=irep_idt()) + i_it->source_location.set_java_bytecode_index( + it->source_location.get_java_bytecode_index()); } if(i_it->function==irep_idt()) From 67961355a52e7193dcf99611884b5dcb8d5038ae Mon Sep 17 00:00:00 2001 From: Cristina Date: Thu, 20 Apr 2017 13:44:58 +0100 Subject: [PATCH 2/2] Added the bytecode index to the expected result of the regression tests --- regression/cbmc-java/NullPointer1/test.desc | 2 +- regression/cbmc-java/NullPointer4/test.desc | 2 +- src/analyses/goto_check.cpp | 3 +-- 3 files changed, 3 insertions(+), 4 deletions(-) diff --git a/regression/cbmc-java/NullPointer1/test.desc b/regression/cbmc-java/NullPointer1/test.desc index d479356875a..b11a57a56fd 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$ +^ 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 2e1b728c1fc..28c9e6f47fd 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$ +^ file NullPointer4.java line 6 function java::NullPointer4.main:\(\[Ljava/lang/String;\)V bytecode_index 4$ ^VERIFICATION FAILED$ -- ^warning: ignoring diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 635e0eb8f9a..a6871b94d23 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1821,8 +1821,7 @@ void goto_checkt::goto_check( if(it->source_location.get_column()!=irep_idt()) i_it->source_location.set_column(it->source_location.get_column()); - if(mode==ID_java && - it->source_location.get_java_bytecode_index()!=irep_idt()) + if(it->source_location.get_java_bytecode_index()!=irep_idt()) i_it->source_location.set_java_bytecode_index( it->source_location.get_java_bytecode_index()); }