Infer hangs somewhere in PulseFormula while analyzing this C# code snippet:
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.
Infer hangs somewhere in PulseFormula while analyzing this C# code snippet:
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.tyou 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.