Handle the case of null arguments for format

Author: romainbrenguier

src/solvers/strings/string_constraint_generator_format.cpp

@@ -285,9 +285,11 @@ add_axioms_for_format_specifier(
     return_code = add_axioms_for_string_of_float(
         fresh_symbol, res, get_arg(ID_float), array_pool, ns);
     return {res, std::move(return_code.second)};
-  case format_specifiert::CHARACTER:
-    return_code = add_axioms_from_char(res, get_arg(ID_char));
-    return {res, std::move(return_code.second)};
+  case format_specifiert::CHARACTER: {
+    exprt arg_string = get_arg(ID_char);
+    array_string_exprt &string_expr = to_array_string_expr(arg_string);
+    return {std::move(string_expr), {}};
+  }
   case format_specifiert::BOOLEAN:
     return_code = add_axioms_from_bool(res, get_arg(ID_boolean));
     return {res, std::move(return_code.second)};
@@ -378,23 +380,34 @@ exprt format_arg_from_string(
         shl_exprt{typecast_exprt{string[2], type}, 16},
         typecast_exprt{string[3], type}}};
   }
+
+  const and_exprt is_null{
+    equal_exprt{string.length(), from_integer(4, string.length().type())},
+    and_exprt{
+      equal_exprt{string[0], from_integer('n', string[0].type())},
+      equal_exprt{string[1], from_integer('u', string[0].type())},
+      equal_exprt{string[2], from_integer('l', string[0].type())},
+      equal_exprt{string[3], from_integer('l', string[0].type())}}
+  };
+
   if(id == ID_char)
   {
-    // We assume the string has length exactly 4 and ignore the first 3
-    // (unsigned16)string.content[3]
-    const unsignedbv_typet type{16};
-    return typecast_exprt{
+    // We assume the string has length exactly 4 and ignore the first 3, and
+    // construct a string of length 1, which contains (char)string.content[3]
+    array_string_exprt char_as_string;
+    char_as_string.type() = array_typet{
+      string.type().subtype(), from_integer(1, string.length().type())};
+    char_as_string.operands().push_back(typecast_exprt{
       index_exprt{string.content(), from_integer(3, string.length().type())},
-      type};
+      string.type().subtype()});
+    return if_exprt{is_null, string, char_as_string};
   }
   if(id == ID_boolean)
   {
-    // We assume the string has length exactly 4 and ignore the first 3
-    // (bool)string.content[3]
-    const c_bool_typet type{8};
-    return typecast_exprt{
-      index_exprt{string.content(), from_integer(3, string.length().type())},
-      type};
+    // We assume the string has length exactly 4, if it is "null" return false
+    // and otherwise ignore the first 3 and return (bool)string.content[3]
+    return if_exprt{
+      is_null, false_exprt{}, typecast_exprt{string[3], bool_typet()}};
   }
   if(id == ID_float)
   {