Apply field sensitivity in symex_printf

romainbrenguier · romainbrenguier · commit 7cca54c17411 · 2019-08-06T07:33:41.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
@@ -394,6 +394,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
`@@ -394,6 +394,7 @@ void goto_symext::symex_printf(`
`394`	`394`	`else`
`395`	`395`	`{`
`396`	`396`	`clean_expr(*va_args, state, false);`
	`397`	`+ va_args = field_sensitivityt{}.apply(ns, state, va_args, false);`
`397`	`398`	`va_args = state.rename(va_args, ns).get();`
`398`	`399`	`if(va_args->id() != ID_array)`
`399`	`400`	`{`