Draft
Conversation
- Implements syscall() function model as requested in issue diffblue#7646 - Delegates to existing models where available (read, write, open, close, etc.) - Provides safe overapproximation for unmodeled syscalls - Includes inline models for dup, lseek, getpid, getuid, and related syscalls - Adds comprehensive test suite with 3 test cases covering basic functionality, error handling, and realistic usage scenarios - Includes detailed documentation and implementation summary Addresses: diffblue#7646 Follows approach from: model-checking/kani#2284
As requested by @tautschnig in PR comment #3520785346, this refactors the inline model implementations in syscall.c to follow CBMC library function standards and structure. Changes made: - Extracted 10 inline models into separate CBMC library functions - Created dup.c with dup(), dup2(), dup3() implementations - Created lseek.c with lseek() implementation - Created process_info.c with getpid(), getuid(), getgid(), geteuid(), getegid(), gettid() - Updated syscall() function to delegate to these library functions - Reduced syscall.c complexity by ~150 lines - All functions now follow standard CBMC library patterns Benefits: - Improved maintainability and code organization - Functions can be reused independently of syscall() - Consistent with existing CBMC library structure - Better separation of concerns - Simplified syscall dispatch logic All existing tests continue to pass. The refactoring is fully backward compatible with no change to external interfaces.
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
1 participant
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.
Fixes: #7646