CBMC coverage incorrect in places

[vecchiot-aws]

• When calling a method on a boxed value, the enclosing function's header is marked as "both" (hit and missed).

  fn helper() {
    Box::new(1_u32).pow(2);
  }
  
  fn main() {
    helper();
  }

• Mutable dereferencing operations are sometimes marked as "both" (can't figure out exact cause).

  fn both() {
    let mut x = 1;
    let y = &mut x;
    let z = *y;
    *y = z + 1; // both
  }
  
  fn hit() {
    let mut x = 1;
    let y = &mut x;
    let _y = *y;
    let z = 2;
    *y = z + 1; // hit
  }
  
  fn main () {
    both();
    hit();
  }

• Asserts

  • A satisfied assert never gets marked as "hit"
  • Sometimes, a satisfied assert gets marked as "none"

    
    fn helper() {
    let x = 1;
    assert!(x == 1); // none
    assert!(x == 1); // both
    assert!(x == 1); // both
    assert!(x == 1); // both
    }

  fn helper2() { let x = 1; x + 1; assert!(x == 1); // both assert!(x == 1); // both assert!(x == 1); // both assert!(x == 1); // both

  assert!(x == 2); // hit }

  fn main() { helper(); helper2(); }

[zhassan-aws]

The boxes issue is now fixed, but the other two issues are still there.