Standardize exit codes, use SimpleAPI for inlining, add --no-solve flag#696
Merged
Standardize exit codes, use SimpleAPI for inlining, add --no-solve flag#696
Conversation
…flag - Introduce ExitCode namespace with documented exit code constants (1=user error, 2=failures found, 3=internal error, 4=known limitation) - Add general exit helpers: exitUserError, exitFailuresFound, exitInternalError, exitKnownLimitation - Replace all panic! calls with exitInternalError for proper exit codes - Use Core.inlineProcedures from SimpleAPI in pyAnalyzeLaurelCommand and pyAnalyzeToGotoCommand instead of direct Core.Transform calls - Add --check-only flag to pyAnalyzeLaurel for SMT-only generation - Swap exit codes 2↔3 to group user-actionable (1,2) and tool-side (3,4) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- Add `skipSolver` field to VerifyOptions and wire it through dischargeObligation to write SMT-Lib files without invoking the solver (returns unknown for all VCs) - Add `--no-solve` flag to pyAnalyzeLaurel that sets both `skipSolver` and `alwaysGenerateSMT` so all VCs get SMT files - Validate that --no-solve requires --vc-directory or --keep-all-files - Rename `alwaysRunSMT` to `alwaysGenerateSMT` for clarity - Document all VerifyOptions fields with grouping comments Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
shigoel
changed the title
The explicit @dischargeObligation call needs the skipSolver argument passed positionally since default parameters don't apply with @. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
joscoh
approved these changes
Mar 27, 2026
atomb
approved these changes
Mar 27, 2026
olivier-aws
pushed a commit
that referenced
this pull request
Mar 30, 2026
…ag (#696) ## Summary - Introduce `ExitCode` namespace with documented exit code constants and a common scheme across all `strata` subcommands (1=user error, 2=failures found, 3=internal error, 4=known limitation) - Use `Core.inlineProcedures` from SimpleAPI in `pyAnalyzeLaurelCommand` and `pyAnalyzeToGotoCommand` instead of calling lower-level `Core.Transform.runProgram` directly - Add `--no-solve` flag to `pyAnalyzeLaurel` that generates SMT-Lib files without invoking the solver (requires `--vc-directory` or`--keep-all-files`) - Add `skipSolver` field to `VerifyOptions` and wire through `dischargeObligation` - Rename `alwaysRunSMT` → `alwaysGenerateSMT` for clarity - Document all `VerifyOptions` fields with grouping comments - Replace all `panic!` calls with proper `exitInternalError` (exit code 3) - Swap exit codes 2↔3 to group user-actionable codes (1,2) and tool-side codes (3,4) ## NEXT UP Continue migrating StrataMain commands to use SimpleAPI — deduplicate the shared Laurel text-file parsing across 4 commands and add Laurel verification and Python direct-pipeline functions to SimpleAPI. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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
3 participants
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.
Summary
Introduce
ExitCodenamespace with documented exit code constants and a common scheme across allstratasubcommands (1=user error, 2=failures found, 3=internal error, 4=known limitation)Use
Core.inlineProceduresfrom SimpleAPI inpyAnalyzeLaurelCommandandpyAnalyzeToGotoCommandinstead of calling lower-levelCore.Transform.runProgramdirectlyAdd
--no-solveflag topyAnalyzeLaurelthat generates SMT-Lib files without invoking the solver (requires--vc-directoryor--keep-all-files)Add
skipSolverfield toVerifyOptionsand wire throughdischargeObligationRename
alwaysRunSMT→alwaysGenerateSMTfor clarityDocument all
VerifyOptionsfields with grouping commentsReplace all
panic!calls with properexitInternalError(exit code 3)Swap exit codes 2↔3 to group user-actionable codes (1,2) and tool-side codes (3,4)
NEXT UP
Continue migrating StrataMain commands to use SimpleAPI — deduplicate the shared Laurel text-file parsing across 4 commands and add Laurel verification and Python direct-pipeline functions to SimpleAPI.
🤖 Generated with Claude Code