facebook / facebook/infer

Infer hangs somewhere in PulseFormula

Open
#2,039 0 comments 0 reactions 0 assignees View on GitHub
bug pulse
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

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.