diff --git a/src/plugins/value/domains/cvalue/cvalue_transfer.ml b/src/plugins/value/domains/cvalue/cvalue_transfer.ml index cf095c211eb8dd675ed2b33dde078e97925582e0..10b707287ea402adc96ce53fa00c1cee5417f014 100644 --- a/src/plugins/value/domains/cvalue/cvalue_transfer.ml +++ b/src/plugins/value/domains/cvalue/cvalue_transfer.ml @@ -60,7 +60,7 @@ let update valuation t = let process exp record t = match exp.enode with | Lval lv -> - if record.reductness = Reduced + if record.reductness = Reduced && Cil.isScalarType (Cil.typeOfLval lv) then let {v; initialized; escaping} = record.value in let v = unbottomize v in diff --git a/tests/value/oracle_multidim/struct2.res.oracle b/tests/value/oracle_multidim/struct2.res.oracle index 8d07aa9bd964f535d7b8bc7effe02f112c892483..b18f3b3d19117c87628a5cbdae0c2a47a4ef0dbe 100644 --- a/tests/value/oracle_multidim/struct2.res.oracle +++ b/tests/value/oracle_multidim/struct2.res.oracle @@ -1,20 +1,10 @@ 53a54,55 > [kernel] struct2.i:78: Warning: > all target addresses were invalid. This path is assumed to be dead. -75a78,81 -> [eva] struct2.i:173: -> Assigning imprecise value to ((s1.c)->c)->b -> (pointing to s2 with offsets {352}). -> The imprecision originates from Misaligned Bottom -129,130c135 -< s8.a ∈ {0} -< .b ∈ {{ &a }} ---- -> s8 ∈ {{ garbled mix of &{a} (origin: Misaligned Bottom) }} -136,137d140 +136,137d137 < tab4[0] ∈ {0; 2} < [1] ∈ {0} -206c209 +206c206 < s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab4[0]; tab5[0]; --- > s4.e[0].a; s8.b; s7; tab1[0..1]; tab2[0..1]; tab3[0..1]; tab5[0];