diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml index adb32ee38ed5f3e66a5b64104fb931f3374f2fd4..fb9f072b6f9d7d5d581ca117963b15416923c531 100644 --- a/src/plugins/value/domains/taint_domain.ml +++ b/src/plugins/value/domains/taint_domain.ml @@ -210,8 +210,11 @@ module TransferTaint = struct let lv_zone, lv_indirect_zone, singleton = compute_zones lval to_loc in let exp_zone = Value_util.zone_of_expr to_loc exp in (* [lv] becomes data-tainted if a memory location on which the value of - [exp] depends on is data-tainted. *) - let data_tainted = Zone.intersects state.locs_data exp_zone in + [exp] or the location of [lval] depends on is data-tainted. *) + let data_tainted = + Zone.intersects state.locs_data exp_zone + || Zone.intersects state.locs_data lv_indirect_zone + in (* [lv] becomes control-tainted if: - the current call depends on a tainted assume statements of a caller; - the execution of the assignment depends on a tainted assume statement; diff --git a/tests/value/oracle/taint.res.oracle b/tests/value/oracle/taint.res.oracle index 7f657cbe01701cb97ccad973761108a2cbe99436..77cc014292ccdd5390421d622c76bfcb39492a64 100644 --- a/tests/value/oracle/taint.res.oracle +++ b/tests/value/oracle/taint.res.oracle @@ -12,7 +12,7 @@ Frama_C_dump_each: # taint: Locations (data): - tainted; t; u; x + tainted; t; u; x; buf[0] Locations (control): w; buf[0] ==END OF DUMP== @@ -142,7 +142,7 @@ Frama_C_dump_each: # taint: Locations (data): - tainted; t; u; x; t + tainted; t; u; x; buf[0]; t Locations (control): t; u; w; x; y; buf[0..1] ==END OF DUMP==