From 2b09c0b0b4d611937c48b00f7be74e3128dcf34d Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 24 Mar 2017 11:04:21 +0000 Subject: [PATCH 1/4] Remove unused variable and braces --- src/java_bytecode/java_object_factory.cpp | 27 ++++++++++------------- 1 file changed, 12 insertions(+), 15 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 088a25f7038..ea102a52996 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -250,20 +250,18 @@ void java_object_factoryt::gen_nondet_init( { exprt allocated= allocate_object(expr, subtype, loc, create_dynamic_objects); - { - exprt init_expr; - if(allocated.id()==ID_address_of) - init_expr=allocated.op0(); - else - init_expr=dereference_exprt(allocated, allocated.type().subtype()); - gen_nondet_init( - init_expr, - false, - "", - loc, - false, - create_dynamic_objects); - } + exprt init_expr; + if(allocated.id()==ID_address_of) + init_expr=allocated.op0(); + else + init_expr=dereference_exprt(allocated, allocated.type().subtype()); + gen_nondet_init( + init_expr, + false, + "", + loc, + false, + create_dynamic_objects); } if(!assume_non_null) @@ -592,7 +590,6 @@ exprt object_factory( exprt object=aux_symbol.symbol_expr(); - const namespacet ns(symbol_table); gen_nondet_init( object, init_code, From a3f49a341b5e43a104e74feac28c33c574f68545 Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 24 Mar 2017 11:19:20 +0000 Subject: [PATCH 2/4] Move function comments to the right place --- src/java_bytecode/java_object_factory.cpp | 53 ++++++++++++----------- 1 file changed, 28 insertions(+), 25 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index ea102a52996..2c22d71e4ac 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -25,18 +25,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_types.h" #include "java_utils.h" -/*******************************************************************\ - -Function: gen_nondet_init - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - class java_object_factoryt:public messaget { code_blockt &init_code; @@ -81,19 +69,15 @@ class java_object_factoryt:public messaget const typet &override_type=empty_typet()); }; - /*******************************************************************\ -Function: gen_nondet_array_init +Function: java_object_factoryt::allocate_object - Inputs: the target expression, desired object type, source location - and Boolean whether to create a dynamic object + Inputs: - Outputs: the allocated object + Outputs: - Purpose: Returns false if we can't figure out the size of allocate_type. - allocate_type may differ from target_expr, e.g. for target_expr - having type int* and allocate_type being an int[10]. + Purpose: \*******************************************************************/ @@ -165,10 +149,29 @@ exprt java_object_factoryt::allocate_object( } } -// Override type says to ignore the LHS' real type, and init it with the given -// type regardless. Used at the moment for reference arrays, which are -// implemented as void* arrays but should be init'd as their true type with -// appropriate casts. +/*******************************************************************\ + +Function: java_object_factoryt::gen_nondet_init + + Inputs: + expr - + is_sub - + class_identifier - + loc - + skip_classid - + create_dynamic_objects - + override - Ignore the LHS' real type. Used at the moment for + reference arrays, which are implemented as void* + arrays but should be init'd as their true type with + appropriate casts. + override_type - Type to use if ignoring the LHS' real type + + Outputs: + + Purpose: + +\*******************************************************************/ + void java_object_factoryt::gen_nondet_init( const exprt &expr, bool is_sub, @@ -343,7 +346,7 @@ void java_object_factoryt::gen_nondet_init( /*******************************************************************\ -Function: gen_nondet_array_init +Function: java_object_factoryt::gen_nondet_array_init Inputs: From 4c4ccc032919a94753e824c892155a8ca9d55f4a Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 24 Mar 2017 12:04:19 +0000 Subject: [PATCH 3/4] Remove variable that is always false skip_classid was always false, so there wasn't any point having it. --- src/java_bytecode/java_object_factory.cpp | 14 +------------- src/java_bytecode/java_object_factory.h | 1 - 2 files changed, 1 insertion(+), 14 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 2c22d71e4ac..602bc4bb497 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -63,7 +63,6 @@ class java_object_factoryt:public messaget bool is_sub, irep_idt class_identifier, const source_locationt &loc, - bool skip_classid, bool create_dynamic_objects, bool override=false, const typet &override_type=empty_typet()); @@ -158,7 +157,6 @@ Function: java_object_factoryt::gen_nondet_init is_sub - class_identifier - loc - - skip_classid - create_dynamic_objects - override - Ignore the LHS' real type. Used at the moment for reference arrays, which are implemented as void* @@ -177,7 +175,6 @@ void java_object_factoryt::gen_nondet_init( bool is_sub, irep_idt class_identifier, const source_locationt &loc, - bool skip_classid, bool create_dynamic_objects, bool override, const typet &override_type) @@ -263,7 +260,6 @@ void java_object_factoryt::gen_nondet_init( false, "", loc, - false, create_dynamic_objects); } @@ -298,9 +294,6 @@ void java_object_factoryt::gen_nondet_init( if(name=="@class_identifier") { - if(skip_classid) - continue; - irep_idt qualified_clsid="java::"+as_string(class_identifier); constant_exprt ci(qualified_clsid, string_typet()); code_assignt code(me, ci); @@ -328,7 +321,6 @@ void java_object_factoryt::gen_nondet_init( _is_sub, class_identifier, loc, - false, create_dynamic_objects); } } @@ -380,7 +372,7 @@ void java_object_factoryt::gen_nondet_array_init( const auto &length_sym_expr=length_sym.symbol_expr(); // Initialize array with some undetermined length: - gen_nondet_init(length_sym_expr, false, irep_idt(), loc, false, false); + gen_nondet_init(length_sym_expr, false, irep_idt(), loc, false); // Insert assumptions to bound its length: binary_relation_exprt @@ -465,7 +457,6 @@ void java_object_factoryt::gen_nondet_array_init( false, irep_idt(), loc, - false, true, true, element_type); @@ -495,7 +486,6 @@ void gen_nondet_init( code_blockt &init_code, symbol_tablet &symbol_table, const source_locationt &loc, - bool skip_classid, bool create_dyn_objs, bool assume_non_null, message_handlert &message_handler, @@ -512,7 +502,6 @@ void gen_nondet_init( false, "", loc, - skip_classid, create_dyn_objs); } @@ -599,7 +588,6 @@ exprt object_factory( symbol_table, loc, false, - false, !allow_null, message_handler, max_nondet_array_length); diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h index 6122d3e2780..5141ca45f42 100644 --- a/src/java_bytecode/java_object_factory.h +++ b/src/java_bytecode/java_object_factory.h @@ -27,7 +27,6 @@ void gen_nondet_init( code_blockt &init_code, symbol_tablet &symbol_table, const source_locationt &, - bool skip_classid, bool create_dynamic_objects, bool assume_non_null, message_handlert &message_handler, From 9a1dae0323dad1f71ca7a946e4ee8c41596982b6 Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 24 Mar 2017 15:05:50 +0000 Subject: [PATCH 4/4] Remove function that's only used once gen_nondet_init() is only used once, and is only two lines long, so get rid of it and just put those two lines. This also avoids confusion with java_object_factory::gen_nondet_init(). --- src/java_bytecode/java_object_factory.cpp | 51 ++++------------------- src/java_bytecode/java_object_factory.h | 11 ----- 2 files changed, 9 insertions(+), 53 deletions(-) diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 602bc4bb497..166be7827c9 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -471,42 +471,6 @@ void java_object_factoryt::gen_nondet_array_init( /*******************************************************************\ -Function: gen_nondet_init - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void gen_nondet_init( - const exprt &expr, - code_blockt &init_code, - symbol_tablet &symbol_table, - const source_locationt &loc, - bool create_dyn_objs, - bool assume_non_null, - message_handlert &message_handler, - size_t max_nondet_array_length) -{ - java_object_factoryt state( - init_code, - assume_non_null, - max_nondet_array_length, - symbol_table, - message_handler); - state.gen_nondet_init( - expr, - false, - "", - loc, - create_dyn_objs); -} - -/*******************************************************************\ - Function: new_tmp_symbol Inputs: @@ -582,15 +546,18 @@ exprt object_factory( exprt object=aux_symbol.symbol_expr(); - gen_nondet_init( - object, + java_object_factoryt state( init_code, + !allow_null, + max_nondet_array_length, symbol_table, - loc, + message_handler); + state.gen_nondet_init( + object, false, - !allow_null, - message_handler, - max_nondet_array_length); + "", + loc, + false); return object; } diff --git a/src/java_bytecode/java_object_factory.h b/src/java_bytecode/java_object_factory.h index 5141ca45f42..37ed40f0ec9 100644 --- a/src/java_bytecode/java_object_factory.h +++ b/src/java_bytecode/java_object_factory.h @@ -22,17 +22,6 @@ exprt object_factory( const source_locationt &, message_handlert &message_handler); -void gen_nondet_init( - const exprt &expr, - code_blockt &init_code, - symbol_tablet &symbol_table, - const source_locationt &, - bool create_dynamic_objects, - bool assume_non_null, - message_handlert &message_handler, - size_t max_nondet_array_length=5); - - exprt get_nondet_bool(const typet &); symbolt &new_tmp_symbol(