Infer hangs somewhere in PulseFormula
- Dominant language
- OCaml
- Stars
- 15.7k
- Forks
- 2.1k
- Avg merge
- 19h 36m
- Merged PRs (30d)
- 13
Description
Infer hangs somewhere in PulseFormula while analyzing this C# code snippet:
```csharp ln:false
static int foo(int x, int y)
{
if (x < y + 1 && y - 1 <= x && y <= x) return 1;
return 0;
}
```
It looks like it tries to propagate atom but doesn't remove it from original place, and tries to propagate it again, and so on. Or, maybe fuel is not taken into account...
A commit with reproduction case is here: https://github.com/Kepleress/infer/tree/hang-bug/infer/tests_cram/csharp2.
In dune's test file `run.t` you could see output log where it hangs. Building the test requires infersharp binary, but for debugging you can use ready cfg.json and tenv.json provided at the link above.
Contributor guide
Assessment
This issue has not been assessed yet.