Skip to content

Improve symbol analysis across imported Tamarin files#33

Open
nikstuckenbrock wants to merge 5 commits into
tamarin-prover:masterfrom
nikstuckenbrock:feature/complete-symbol-tree
Open

Improve symbol analysis across imported Tamarin files#33
nikstuckenbrock wants to merge 5 commits into
tamarin-prover:masterfrom
nikstuckenbrock:feature/complete-symbol-tree

Conversation

@nikstuckenbrock

Copy link
Copy Markdown

Hi all,

This PR improves the analysis logic used by the plugin, especially for checks like check_variable_is_defined_in_premise, which previously only considered symbols defined in the current document.

Problem

The existing implementation only analyzed symbols from the active file. Symbols coming from imported files — or from files importing the current file — were not taken into account. This led to incomplete analysis and false diagnostics in projects that make use of #import.

Changes

The analysis pipeline has been updated as follows:

  1. Workspace-wide parsing on activation

    • When the extension is activated, all relevant Tamarin files are parsed.
    • Symbol tables are created for each file.
  2. Reverse import lookup

    • After parsing, a reverse import lookup table is built.
    • This allows efficient discovery of files that depend on a given file.
  3. Incremental updates

    • When a file changes, it is analyzed again and the import lookup table is updated accordingly.

Result

Checks such as check_variable_is_defined_in_premise can now resolve symbols across imports, resulting in more accurate diagnostics in the future.

Let me know what you think.

@nikstuckenbrock nikstuckenbrock force-pushed the feature/complete-symbol-tree branch from a95cd35 to 3dae436 Compare February 13, 2026 08:36
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.

1 participant