diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index f892c7400a5..822fcd46a97 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1342,7 +1342,7 @@ exprt java_string_library_preprocesst::get_primitive_value_of_object( /// \return An expression representing the object at position `index` of `argv`. exprt java_string_library_preprocesst::get_object_at_index( const exprt &argv, - int index) + std::size_t index) { dereference_exprt deref_objs(argv, argv.type().subtype()); pointer_typet empty_pointer=pointer_type(empty_typet()); @@ -1390,7 +1390,7 @@ exprt java_string_library_preprocesst::get_object_at_index( /// values of the argument at position `index` of `argv`. exprt java_string_library_preprocesst::make_argument_for_format( const exprt &argv, - int index, + std::size_t index, const struct_typet &structured_type, const source_locationt &loc, const irep_idt &function_id, diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.h b/jbmc/src/java_bytecode/java_string_library_preprocess.h index 84317ed9163..382dc1b5d9d 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.h +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.h @@ -337,7 +337,7 @@ class java_string_library_preprocesst:public messaget exprt make_argument_for_format( const exprt &argv, - int index, + std::size_t index, const struct_typet &structured_type, const source_locationt &loc, const irep_idt &function_id, @@ -351,7 +351,7 @@ class java_string_library_preprocesst:public messaget symbol_table_baset &symbol_table, code_blockt &code); - exprt get_object_at_index(const exprt &argv, int index); + exprt get_object_at_index(const exprt &argv, std::size_t index); codet make_init_from_array_code( const code_typet &type,