Skip to content

Commit 212e471

Browse files
committed
Enable stubs of non-implemented interface functions.
Updates requested in the review: - removal of map 'NONDET_retvals_replacements' from a program - replaced auto by concrete type - removed extra space character
1 parent aed2b15 commit 212e471

File tree

2 files changed

+7
-31
lines changed

2 files changed

+7
-31
lines changed

src/driver/sec_driver_parse_options.cpp

Lines changed: 7 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -512,30 +512,11 @@ void sec_driver_parse_optionst::process_goto_function(
512512

513513
replace_java_nondet(function);
514514

515-
#if 1 // Enable this when remove handling of NONDET in taint_analysis
516-
// Similar removal of java nondet statements:
517-
// TODO Should really get this from java_bytecode_language somehow, but we
518-
// don't have an instance of that here.
519-
object_factory_parameterst factory_params;
520-
factory_params.max_nondet_array_length=
521-
cmdline.isset("java-max-input-array-length")
522-
? std::stoul(cmdline.get_value("java-max-input-array-length"))
523-
: MAX_NONDET_ARRAY_LENGTH_DEFAULT;
524-
factory_params.max_nondet_string_length=
525-
cmdline.isset("string-max-input-length")
526-
? std::stoul(cmdline.get_value("string-max-input-length"))
527-
: MAX_NONDET_STRING_LENGTH;
528-
factory_params.max_nondet_tree_depth=
529-
cmdline.isset("java-max-input-tree-depth")
530-
? std::stoul(cmdline.get_value("java-max-input-tree-depth"))
531-
: MAX_NONDET_TREE_DEPTH;
532-
533515
convert_nondet(
534516
function,
535517
get_message_handler(),
536-
factory_params,
518+
object_factory_params,
537519
ID_java);
538-
#endif
539520

540521
adjust_float_expressions(goto_function, namespacet(symbol_table));
541522

@@ -658,12 +639,12 @@ bool sec_driver_parse_optionst::generate_function_body(
658639
{
659640
// Provide a simple stub implementation for any function we don't have a
660641
// bytecode implementation for:
661-
662-
if(body_available)
663-
return false;
664-
665-
if(!can_generate_function_body(function_name))
666-
return false;
642+
if(body_available || !can_generate_function_body(function_name))
643+
{
644+
const symbolt *symbol = symbol_table.lookup(function_name);
645+
if (symbol == nullptr || !symbol->type.get_bool(ID_C_abstract))
646+
return false;
647+
}
667648

668649
if(symbol_table.lookup_ref(function_name).mode == ID_java)
669650
{

src/taint-analysis/taint_program.h

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -21,11 +21,6 @@
2121

2222
typedef goto_programt::instructiont::const_targett instruction_iteratort;
2323

24-
typedef std::unordered_map<
25-
instruction_iteratort,
26-
symbol_exprt,
27-
instruction_iterator_hashert> replacements_of_NONDET_retvalst;
28-
2924
class taint_statisticst;
3025

3126

0 commit comments

Comments
 (0)