Skip to content

Commit 3b374aa

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 b55f2c4 commit 3b374aa

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
@@ -391,6 +391,7 @@ void goto_symext::symex_printf(
391391
else
392392
{
393393
clean_expr(*va_args, state, false);
394+
*va_args = field_sensitivityt{}.apply(ns, state, *va_args, false);
394395
*va_args = state.rename(*va_args, ns).get();
395396
if(va_args->id() != ID_array)
396397
{

0 commit comments

Comments
 (0)