Skip to content

Commit 7b658f7

Browse files
Apply field sensitivity in symex_printf
This may be necessary for constant propagation of the format string. An example of that is in regression/cbmc/printf1
1 parent fe4a59d commit 7b658f7

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/goto-symex/symex_builtin_functions.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -390,6 +390,7 @@ void goto_symext::symex_printf(
390390
else
391391
{
392392
clean_expr(*va_args, state, false);
393+
*va_args = field_sensitivityt{}.apply(ns, state, *va_args, false);
393394
*va_args = state.rename(*va_args, ns).get();
394395
if(va_args->id() != ID_array)
395396
{

0 commit comments

Comments
 (0)