diff --git a/regression/contracts/assigns_enforce_conditional_unions/program-only.desc b/regression/contracts/assigns_enforce_conditional_unions/program-only.desc new file mode 100644 index 00000000000..60374bac639 --- /dev/null +++ b/regression/contracts/assigns_enforce_conditional_unions/program-only.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-contract update _ --program-only +^EXIT=0$ +^SIGNAL=0$ +-- +^\(\d+\) guard#\d+ == .*byte_extract +-- +Confirms that field sensitivity can resolve pointer byte extracts to type casts. diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp index a430fe4c596..a0cb3e1658d 100644 --- a/src/goto-symex/field_sensitivity.cpp +++ b/src/goto-symex/field_sensitivity.cpp @@ -123,6 +123,20 @@ exprt field_sensitivityt::apply( else return apply(ns, state, std::move(tmp), write); } + else if( + recursive_member.has_value() && recursive_member->id() == ID_typecast) + { + if(was_l2) + { + return apply( + ns, + state, + state.rename(std::move(*recursive_member), ns).get(), + write); + } + else + return apply(ns, state, std::move(*recursive_member), write); + } } } }