Suboptimal CFG reconstruction

[sonmarcho]

A few more minimized examples where the CFG reconstruction is sub-optimal:

fn f1(b : bool, c : bool)
{
    let a;
    
    if b
    {
        a = 1;
        assert!( a == 1 ); // The presence of this assert triggers the issue
    }
    else if c
    {
        return;
    }
}

which gets reconstructed as:

fn f1(bool b, bool c)
{
  if (!b)
  {
    if (!c)
    {
      return;
    }
    return;
  }
  a = 1;
  assert (a == 1);
}

And:

fn f2(b : bool, c : u32)
{
    let mut a = 0;
    while
    {
        if b
        {
            a = 1;
        }
        c > a
    } {}
}

which gets reconstructed as:

fn f2(bool b, uint32_t c)
{
  let a = 0;
  loop
  {
    if (b)
    {
      a = 1;
      if (!(c > a))
      {
        break;
      }
    }
    else if (!(c > a))
    {
      break;
    }
  }
}

[Nadrieril]

Could you link the other open issues we have on the topic?

[sonmarcho]

The other issues are: https://github.com/AeneasVerif/charon/issues/507 https://github.com/AeneasVerif/charon/issues/297 https://github.com/AeneasVerif/charon/issues/770