Skip to content

[CN-exec] Fix missing instrumentation for ghost arguments under labels and loops#499

Merged
dimecon merged 18 commits intorems-project:mainfrom
dimecon:normalise-label-fix
Mar 12, 2026
Merged

[CN-exec] Fix missing instrumentation for ghost arguments under labels and loops#499
dimecon merged 18 commits intorems-project:mainfrom
dimecon:normalise-label-fix

Conversation

@dimecon
Copy link
Copy Markdown
Contributor

@dimecon dimecon commented Feb 24, 2026

Fixes #452. The analysis of mucore programs for the purpose of instrumenting ghost arguments was incomplete. To complete it for non-loop labels, the core-to-mucore label normalisation is updated to preserve the label body.

@dimecon dimecon changed the title Fix missing instrumentation for ghost arguments under labels Fix missing instrumentation for ghost arguments under labels and loops Feb 24, 2026
@dimecon dimecon marked this pull request as ready for review February 24, 2026 20:02
@dimecon dimecon requested a review from rbanerjee20 March 5, 2026 14:12
@dimecon dimecon changed the title Fix missing instrumentation for ghost arguments under labels and loops [CN-exec] Fix missing instrumentation for ghost arguments under labels and loops Mar 10, 2026
Copy link
Copy Markdown
Contributor

@rbanerjee20 rbanerjee20 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Mostly looks good. I've included some questions on whether changes to the parts of the codebase relating to label inlining are still necessary, and one small comment on the new test cases.

Comment thread lib/core_to_mucore.ml
Comment thread lib/mucore.ml
Comment thread lib/pp_mucore_coq.ml
Comment thread lib/mucore.mli
Comment thread tests/cn/ghost_arg_exec_fail.error.c
Copy link
Copy Markdown
Contributor

@rbanerjee20 rbanerjee20 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me - feel free to merge once CI is done.

@dimecon dimecon merged commit 3af1fca into rems-project:main Mar 12, 2026
14 of 18 checks passed
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.

[CN-exec] Missing instrumentation for ghost arguments at call sites when goto/tag is used

2 participants