generated from amazon-archives/__template_Apache-2.0
-
Notifications
You must be signed in to change notification settings - Fork 134
Closed
Labels
Z-Kani CompilerIssues that require some changes to the compilerIssues that require some changes to the compiler[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.[I] Refactoring / Clean UpRefactoring or cleaning up of existing codeRefactoring or cleaning up of existing code
Milestone
Description
Proposed change: We should include information about the public functions as part of the KaniMetadata when the reachability mode is pub_fns. We should stop merging all the metadata and goto binaries together.
Motivation: We have a special handling for --function today inside kani-driver because we cannot tell which artifacts are relevant to some function. So we just merge everything. If we treat functions as potential harnesses, we can get rid of the hack described above. We should also restrict the metadata to include functions that don't take any parameter.
Metadata
Metadata
Assignees
Labels
Z-Kani CompilerIssues that require some changes to the compilerIssues that require some changes to the compiler[C] InternalTracks some internal work. I.e.: Users should not be affected.Tracks some internal work. I.e.: Users should not be affected.[I] Refactoring / Clean UpRefactoring or cleaning up of existing codeRefactoring or cleaning up of existing code