Make StrataCoreToGoto accept a user-specified Strata Core file#404
Merged
tautschnig merged 7 commits intomainfrom Mar 13, 2026
Merged
Make StrataCoreToGoto accept a user-specified Strata Core file#404tautschnig merged 7 commits intomainfrom
tautschnig merged 7 commits intomainfrom
Conversation
It was previously hard-coded to a single test. Turn it into a workflow that accepts *.core.st files as command-line arguments.
Contributor
There was a problem hiding this comment.
Pull request overview
Updates the StrataCoreToGoto executable so it can translate a user-specified Strata Core source file (*.core.st) into CBMC-compatible GOTO JSON outputs, instead of being hard-coded to the SimpleAdd test case.
Changes:
- Replace hard-coded SimpleAdd program import/entrypoint with a CLI that reads and elaborates a
.core.stfile. - Add basic CLI options (
--output-dir,--program-name) and derive default output names from the input filename. - Update the SimpleAdd CBMC helper script to invoke the new CLI form.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 4 comments.
| File | Description |
|---|---|
| StrataTest/Backends/CBMC/SimpleAdd/mkGotoBin.sh | Switches the script to call StrataCoreToGoto with an explicit input .core.st file and output directory. |
| StrataCoreToGoto.lean | Implements new CLI parsing, file loading/elaboration, and JSON output file naming for StrataCoreToGoto. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
tautschnig
changed the title
atomb
previously approved these changes
Feb 11, 2026
Contributor
atomb
left a comment
atomb
left a comment
There was a problem hiding this comment.
This looks good to me, though the Copilot comment might be good to address.
Address Copilot PR review feedback: - Reject --program-name values containing '/' or '..' to prevent path traversal outside the output directory. - Use System.FilePath for path construction instead of string interpolation. - Create the output directory (createDirAll) before writing files so that a non-existent --output-dir produces the directory rather than an unhelpful IO exception. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Resolve conflict in CoreToCProverGOTO.lean: keep origin/main's API with explicit programName parameter (used by other callers), and update StrataCoreToGoto.lean to pass programName and use the new import path after the file was relocated to Strata/Backends/CBMC/GOTO/. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Contributor
Author
Addressed in 4afbbae. |
joehendrix
approved these changes
Mar 13, 2026
atomb
approved these changes
Mar 13, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description of changes:
It was previously hard-coded to a single test. Turn it into a workflow that accepts a *.core.st file as command-line argument.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.