Apply field sensitivity in symex_printf

romainbrenguier · romainbrenguier · commit ddb29cb683cd · 2019-07-12T12:08:58.000+01:00
This may be necessary for constant propagation of the format string.
An example of that is in regression/cbmc/printf1
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
@@ -391,6 +391,7 @@ void goto_symext::symex_printf(
   else
   {
     clean_expr(*va_args, state, false);
+    *va_args = field_sensitivityt{}.apply(ns, state, *va_args, false);
     *va_args = state.rename(*va_args, ns).get();
     if(va_args->id() != ID_array)
     {

Original file line number	Diff line number	Diff line change
`@@ -391,6 +391,7 @@ void goto_symext::symex_printf(`
`391`	`391`	`else`
`392`	`392`	`{`
`393`	`393`	`clean_expr(*va_args, state, false);`
	`394`	`+ va_args = field_sensitivityt{}.apply(ns, state, va_args, false);`
`394`	`395`	`va_args = state.rename(va_args, ns).get();`
`395`	`396`	`if(va_args->id() != ID_array)`
`396`	`397`	`{`