[PATCH] D104917: [Analyzer] Extend exploded-graph-rewriter to support eq and diseq classes

Wed Jul 14 08:07:19 PDT 2021

martong added a comment.

In D104917#2860923 <https://reviews.llvm.org/D104917#2860923>, @NoQ wrote:

> WDYT about the following format:
>
>   Equality constraints:
>   reg_$0<a> == reg_$1<b>
>             == reg_$2<c>
>   
>   Disequality constraints:
>   reg_$0<a> != reg_$3<d>,
>             != reg_$4<e>
>
> Comma is a bit hard to notice but otherwise kinda nicely readable?

IMHO this format would be confusing if you have two SVals that include comparison operators:
E.g. SVal1 `(reg_$1<int b>) == (reg_$2<int c>)` and SVal2 `(reg_$0<int a>) != 42`. They might be in the same equivalence class, that would result this format:

  Equality constraints:
  (reg_$1<int b>) == (reg_$2<int c>) == (reg_$0<int a>) != 42

Well, ... I know the current table with the borders looks a bit rough and ugly, but I think the information is displayed in an obvious way and can be interpreted unambiguously.

Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D104917/new/

https://reviews.llvm.org/D104917