Skip to content

Allow disabling context-sensitivity for specific functions#1995

Draft
Copilot wants to merge 2 commits intomasterfrom
copilot/allow-disable-context-sensitivity
Draft

Allow disabling context-sensitivity for specific functions#1995
Copilot wants to merge 2 commits intomasterfrom
copilot/allow-disable-context-sensitivity

Conversation

Copy link
Copy Markdown
Contributor

Copilot AI commented Apr 12, 2026

Functions called with many different contexts can cause analysis blowup. This adds a way to disable context-sensitivity for specific functions at the MCP level, returning an empty context list [] for all call sites of the annotated function.

Three mechanisms supported

  • C attribute (no source modification to definition needed):

    int f(int x) __attribute__((goblint_context("no-context")));
    int f(int x) { ... }
  • Config option (no source changes required):

    --set ana.context.no_fun[+] f
    
  • Per-function annotation config:

    --set annotation.goblint_context.f[+] no-context
    

Changes

  • src/analyses/mCP.ml: context function now short-circuits to [] when the function has the no-context attribute or appears in ana.context.no_fun, making it context-insensitive across all activated analyses
  • src/config/options.schema.json: Added "no-context" to goblint_context attribute enum; added ana.context.no_fun string-list option
  • docs/user-guide/annotating.md: Documented new no-context attribute value
  • tests/regression/90-context/: Regression tests for all three mechanisms

…on context-insensitivity

Agent-Logs-Url: https://github.com/goblint/analyzer/sessions/5d5147c1-4b56-47f6-b7ef-01b3c007d358

Co-authored-by: michael-schwarz <13812333+michael-schwarz@users.noreply.github.com>
Copilot AI changed the title [WIP] Add option to disable context-sensitivity for specific functions Allow disabling context-sensitivity for specific functions Apr 12, 2026
Copilot AI requested a review from michael-schwarz April 12, 2026 07:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Allow disabling context-sensitivity for specific functions

2 participants