The summary of function in `pulse-model-free-pattern` is not the same as ` free`

[thanhtoantnt]

I want to simplify the summary of a Custom_Free function by using pulse-model-free-pattern. However, when I check the function summary using infer-debug --procedures --procedures-summary --procedures-filter Custom_Free, the summary is the same as not using the pulse-model-free-pattern option, still really complicated with 5 pre/post pairs.

I expect that the summary of this custom free function would be the same as the summary of the free function, containing 2 pre/post pairs.

Here is the content of my .inferconfig file:

{
    "compilation-database": ["build/compile_commands.json"],
    "pulse-only": true,
    "no-pulse-report-latent-issues": true,
    "pulse-max-disjuncts": 60,
    "pulse-model-free-pattern": "Custom_Free",
    "pulse-model-malloc-pattern": "Custom_Malloc",
}

Please include the following information:

• [x] The version of infer from infer --version: Infer version v1.2.0-af2e6bcbf8
• [x] Your operating system and version: Ubuntu 22.04.4 LTS
• [x] Which command you ran: infer-run and I have a .inferconfig file
• [ ] The full output in a paste, for instance a gist.
• [ ] If possible, a minimal example to reproduce your problem (for instance, some code where infer reports incorrectly, together with the way you run infer to reproduce the incorrect report).

[jvillard]

Specifying the option won't stop pulse from analysing Custom_Free so it will still have the same summary. However, pulse will not use that summary anywhere Custom_Free is called but will bypass it and treat is as free instead.

[thanhtoantnt]

I understand now. Thank you, Jules.