<table border="1" cellspacing="0" cellpadding="8">
    <tr>
        <th>Issue</th>
        <td>
            <a href=https://github.com/llvm/llvm-project/issues/76462>76462</a>
        </td>
    </tr>

    <tr>
        <th>Summary</th>
        <td>
            Widening API mismatches flow condition and (previous) values
        </td>
    </tr>

    <tr>
      <th>Labels</th>
      <td>
            clang:dataflow
      </td>
    </tr>

    <tr>
      <th>Assignees</th>
      <td>
            ymand
      </td>
    </tr>

    <tr>
      <th>Reporter</th>
      <td>
          ymand
      </td>
    </tr>
</table>

<pre>
    The [widening API requires](https://github.com/llvm/llvm-project/blob/a01b58aef0e42fb1b52e358adf4c56678a884d37/clang/include/clang/Analysis/FlowSensitive/DataflowEnvironment.h#L108-L134) that analyses return the previous value when it is equivalent to the current values's widening. But, that equivalence is *with respect to the previous environment (and its flow condition)*, while the widening operation will save the *current* environment. So, when checking equivalence, the operation succeeds, but then the resulting environment is incoherent -- the previous value is saved with the current flow condition. It is easy to trigger situations where the current flow condition is too weak to prove assertions about the previous value (for example, that a given property is false).

The API must provide a way for the widened value to be correct with respect to the saved environment.

</pre>
<img width="1px" height="1px" alt="" src="http://email.email.llvm.org/o/eJyUVMGupDYQ_BpzaT0EDQxw4MDmBWmlPUTaSDkbuwFnPfbENpD5-8gwb3ayWkXKZUZAu6qr2tXcezUboo5Vnxji_cqNZIisek_4GhbruuNVMlp5735fCFj1aVeSjDIz9L99Bkd_rcqRZ9U7w2YJ4eZZ0TMcGA6zCss6psJeGQ5abx9_bzdn_yQRGA6jtiPDgWf5WDWcpoxKnMZ8rJCKquFyKkV1udQNb5pSFjXDQWhuZoaDMkKvkl7e9Ibru1ee4TBou38l41VQWyx554FP2u6_mk05a65kQrowLL7kWfP2JS9Khi2EhQfgBwh5cBRWZyAsBDdHm7Krh43rlWBfyIAKoDxE8RvXZAIEe9SK1bn4eJR6hrWHD79S-LQGhr-cRM-jgiISw35XYQFH_kbiCfekpu-dA8OGGwkqeIiiQFgjVVDWMGwZ9pFiX5SmA-E5LXsjx2MV7Epr8Hw7Cxj2j6YZ9q88KXy1JxYZEAuJbxHmpe9TC70g-1UIIunjl3EN8etpoSO_6nCcfxGiPCgj7EKHZW9vP3Nb-aNVCYc9rxb_W3sKn8-RcH8_3HNqnsmBV2E9mvNRiKP_gIjHg7WwE_8WIW7ObgTce3InAB_tKerHJhk2k3VAf_PrTdNzxhxmtZGJQDdy4R4JJq49MWxTlr2zrD9_Y7Jimq6rDwetkgQcdn6HiPucI8kHYbAwEgjrXLwsP7s5p2mv4zypEtkVsi1anlCX11lRZ3l9aZOlK8U0Sl7XMi_yfOJT27R1gVORNW1F-SQS1WGGRY5Y5w222Ka1rC_Iy1xUlzar24mVGV250mkMeWrdnCjvV-rqS3nBRPORtH8smjOzRS8fwXzsHNcd-2FcZ8_KTCsf_HewoIKm7o_X7XNV_sqDWOjHJEAMCMPmY04x32ckk9Xp7n_vqUNI3CyHln8CAAD__77Dyts">