Skip to content

Generate symbolic arguments based on function signature #525

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 12 commits into from
Apr 11, 2025
Merged

Generate symbolic arguments based on function signature #525

merged 12 commits into from
Apr 11, 2025
+110 −5

Conversation

gtrepta
Copy link
Contributor

@gtrepta gtrepta commented Apr 10, 2025

fixes: #495

  • Creates a symbolic KMIR-SYMBOLIC-LOCALS module with symbolic counterparts to the #init and #execFunction symbols in KMIR.
  • Modifies kmir gen-spec to use #initSymbolic in the generated claim.

@gtrepta gtrepta marked this pull request as ready for review April 10, 2025 22:52
@gtrepta gtrepta requested review from jberthold and dkcumming April 10, 2025 22:52
jberthold
jberthold approved these changes Apr 10, 2025
View reviewed changes
Copy link
Member

@jberthold jberthold left a comment

Choose a reason for hiding this comment

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

LGTM
It would be great to have a single #init function but maybe the two backends just require this split into two of them. Having a way to provide concrete arguments and separate rules for the two backends in one module might enable this (later, not now).

@automergerpr-permission-manager automergerpr-permission-manager bot merged commit b5e58dc into master Apr 11, 2025
6 checks passed
@automergerpr-permission-manager automergerpr-permission-manager bot deleted the guy/symbolic-args branch April 11, 2025 23:25
This was referenced Apr 14, 2025
Closed
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jberthold jberthold jberthold approved these changes

@dkcumming dkcumming Awaiting requested review from dkcumming

Assignees
No one assigned
Labels
automerge
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Add symbolic arguments to execution according to start symbol
3 participants
@gtrepta @jberthold @rv-auditor