From 03bae458ea25d2c48921102d287df6b6cfdf08c2 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Mon, 17 Sep 2018 15:22:30 +0100 Subject: [PATCH 1/2] Store the final status of fields in `componentt` --- jbmc/src/java_bytecode/java_bytecode_convert_class.cpp | 2 ++ src/util/std_types.h | 10 ++++++++++ 2 files changed, 12 insertions(+) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 306df0a0ef6..15277d84ddb 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -753,6 +753,8 @@ void java_bytecode_convert_classt::convert( else component.set_access(ID_default); + component.set_is_final(f.is_final); + // Load annotations if(!f.annotations.empty()) { diff --git a/src/util/std_types.h b/src/util/std_types.h index 487fde2e51b..a100de8c08f 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -189,6 +189,16 @@ class struct_union_typet:public typet { return set(ID_C_is_padding, is_padding); } + + bool get_is_final() const + { + return get_bool(ID_final); + } + + void set_is_final(const bool is_final) + { + set(ID_final, is_final); + } }; typedef std::vector componentst; From 5874f53e2475ba0d4941d2322bfb18164f8d3fa5 Mon Sep 17 00:00:00 2001 From: Thomas Spriggs Date: Tue, 18 Sep 2018 14:41:03 +0100 Subject: [PATCH 2/2] Add unit tests on final status of fields --- jbmc/unit/Makefile | 1 + .../ClassWithFields.class | Bin 0 -> 645 bytes .../java_bytecode_parser/ClassWithFields.java | 10 +++++ .../java_bytecode_parser/parse_java_field.cpp | 41 ++++++++++++++++++ 4 files changed, 52 insertions(+) create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithFields.class create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithFields.java create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_field.cpp diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 5bf5f13742e..2c57d8008e5 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -38,6 +38,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \ java_bytecode/java_bytecode_parser/parse_java_annotations.cpp \ java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \ java_bytecode/java_bytecode_parser/parse_java_class.cpp \ + java_bytecode/java_bytecode_parser/parse_java_field.cpp \ java_bytecode/java_object_factory/gen_nondet_string_init.cpp \ java_bytecode/java_replace_nondet/replace_nondet.cpp \ java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithFields.class b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithFields.class new file mode 100644 index 0000000000000000000000000000000000000000..b11af28caa0a9077ec658b4aabb74b472b18ae5e GIT binary patch literal 645 zcmZ8e%We}v5UloYyzw#+$9eD$fjqF6gowut!~sh_S>ymRQf^~slT5OimAvcx7Y7T( zfe+xLBC3s@L^(`%b@g<2P0!!U-+utS$8L-m&uXY)J;rmqP_&_DQ_Yr|Z8a|=G$XVG z)g$L^_C_EFg1hb97p3)O&t{`EU`LtVcq>@yp4tn$msx+j_c_nA)cOyz^gBW0MtZ-0 znhr{4Yd-g#>4YoHURRif)sN1*@{=HFwt9lFogb!xg|74Im(h7Y9e%U@j7+1O4{X-6 zL#OeS49gQ&2o}5T%ofFWSDtiSnjIFL9e>S7!$I0{TD*KK|61Q-u!{QzcVHqU2CuMV zuzk*w*ZcVYVCuN0rYjOe7rM>;Bf)C(pmk$Qvn67kKN54> zRn%1s_!EpOxW|}!i0dke9;#~MDQx1Yjb3>87WxN7XRKAGmHdPx;TV-9_=RAMFp)9l xl&MacNSXN`yj;OU+BHNI93r5okYnfAIKpGhV}r~iW>p}YlY2rhcsi+A`v;*WdXWGC literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithFields.java b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithFields.java new file mode 100644 index 00000000000..70719cb1654 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/ClassWithFields.java @@ -0,0 +1,10 @@ + +class ClassWithFields { + final boolean final1 = true; + final Boolean final2 = false; + final Object final3 = null; + + boolean nonFinal1 = true; + Boolean nonFinal2 = false; + Object nonFinal3 = null; +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_field.cpp b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_field.cpp new file mode 100644 index 00000000000..4faab4915e0 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parser/parse_java_field.cpp @@ -0,0 +1,41 @@ +/*******************************************************************\ + + Module: Unit tests for converting fields + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include +#include +#include +#include + +SCENARIO( + "java_bytecode_parse_field", + "[core][java_bytecode][java_bytecode_parser]") +{ + GIVEN("Some class with final and non final fields") + { + const symbol_tablet &symbol_table = load_java_class( + "ClassWithFields", "./java_bytecode/java_bytecode_parser"); + + WHEN("Parsing the class file structure") + { + THEN("The the final status of the classes fields should be correct.") + { + const symbolt &class_symbol = + symbol_table.lookup_ref("java::ClassWithFields"); + const java_class_typet &java_class = + to_java_class_type(class_symbol.type); + REQUIRE(java_class.get_component("final1").get_is_final()); + REQUIRE(java_class.get_component("final2").get_is_final()); + REQUIRE(java_class.get_component("final3").get_is_final()); + REQUIRE(!java_class.get_component("nonFinal1").get_is_final()); + REQUIRE(!java_class.get_component("nonFinal1").get_is_final()); + REQUIRE(!java_class.get_component("nonFinal1").get_is_final()); + } + } + } +}