Fix printf formatting of C strings

We had failed to update printf formatting to accomodate
annotated_pointer_constant expressions (#6598).

Fixes: #8204

Author: tautschnig

regression/cbmc/printf2/main.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+#include <stdio.h>
+
+int main()
+{
+  printf("results: %s, %d", "five", 5);
+  assert(0);
+}

regression/cbmc/printf2/test.desc

@@ -0,0 +1,8 @@
+CORE no-new-smt
+main.c
+--trace
+^results: five, 5$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

src/goto-programs/printf_formatter.cpp

@@ -136,13 +136,29 @@ void printf_formattert::process_format(std::ostream &out)
       // this is the address of a string
       const exprt &op=*(next_operand++);
       if(
-        op.id() == ID_address_of &&
-        to_address_of_expr(op).object().id() == ID_index &&
-        to_index_expr(to_address_of_expr(op).object()).array().id() ==
-          ID_string_constant)
+        auto pointer_constant =
+          expr_try_dynamic_cast<annotated_pointer_constant_exprt>(op))
       {
-        out << format_constant(
-          to_index_expr(to_address_of_expr(op).object()).array());
+        if(
+          auto address_of = expr_try_dynamic_cast<address_of_exprt>(
+            skip_typecast(pointer_constant->symbolic_pointer())))
+        {
+          if(address_of->object().id() == ID_string_constant)
+          {
+            out << format_constant(address_of->object());
+          }
+          else if(
+            auto index_expr =
+              expr_try_dynamic_cast<index_exprt>(address_of->object()))
+          {
+            if(
+              index_expr->index().is_zero() &&
+              index_expr->array().id() == ID_string_constant)
+            {
+              out << format_constant(index_expr->array());
+            }
+          }
+        }
       }
     }
     break;

src/goto-symex/symex_builtin_functions.cpp

@@ -397,10 +397,16 @@ void goto_symext::symex_printf(
       return;
     }
 
+    // Visual Studio has va_list == char*, else we have va_list == void** and
+    // need to add dereferencing
+    const bool need_deref =
+      operands.back().type().id() == ID_pointer &&
+      to_pointer_type(operands.back().type()).base_type().id() == ID_pointer;
+
     for(const auto &op : va_args->operands())
     {
       exprt parameter = skip_typecast(op);
-      if(parameter.id() == ID_address_of)
+      if(need_deref && parameter.id() == ID_address_of)
         parameter = to_address_of_expr(parameter).object();
       clean_expr(parameter, state, false);
       parameter = state.rename(std::move(parameter), ns).get();