Apply field sensitivity in symex_printf

romainbrenguier · romainbrenguier · commit 7b658f77d1b5 · 2019-06-03T09:08:43.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
@@ -390,6 +390,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
`@@ -390,6 +390,7 @@ void goto_symext::symex_printf(`
`390`	`390`	`else`
`391`	`391`	`{`
`392`	`392`	`clean_expr(*va_args, state, false);`
	`393`	`+ va_args = field_sensitivityt{}.apply(ns, state, va_args, false);`
`393`	`394`	`va_args = state.rename(va_args, ns).get();`
`394`	`395`	`if(va_args->id() != ID_array)`
`395`	`396`	`{`