Skip to content

Unsigned long interval unsoundness with refinement #769

@sim642

Description

@sim642

On 37e0d70 we are unsound on the following program:

// PARAM: --enable ana.int.interval --set ana.int.refinement once
#include <assert.h>

int main() {
  for (unsigned long i = 0; i < 1000; i++) {
    assert(1);
  }

  assert(1); // reachable
  return 0;
}

We claim that the second assert is dead code. The abstract value for i at the loop head is def_exc:Unknown int([0,64]); intervals [0,255].
It's fine with unsigned int and just long.

Metadata

Metadata

Type

No type

Projects

No projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions