From 5ad0480a933823deefbacf4c0b803d317dc27cf4 Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Thu, 3 Jan 2019 16:13:46 +0000 Subject: [PATCH] Add tag to synthetic type made for String.format() Having this type without a tag made it very hard to identify, e.g. if we want to treat it differently from types which are not synthetic (i.e. which come directly from the source code). Compare with refined_string_typet, which has the tag CPROVER_PREFIX "refined_string_type". --- jbmc/src/java_bytecode/java_string_library_preprocess.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 2f1c5e980b9..c2c337502e5 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1459,6 +1459,7 @@ code_blockt java_string_library_preprocesst::make_string_format_code( // a string, an integer, a floating point, a character, a boolean, // an object of which we take the hash code, or a date/time struct_typet structured_type; + structured_type.set_tag(CPROVER_PREFIX "string_formatter_variant"); structured_type.components().emplace_back("string_expr", refined_string_type); structured_type.components().emplace_back(ID_int, java_int_type()); structured_type.components().emplace_back(ID_float, java_float_type());