Skip to content

Remove --function option #2129

@celinval

Description

@celinval

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 compiler[C] InternalTracks some internal work. I.e.: Users should not be affected.[I] Refactoring / Clean UpRefactoring or cleaning up of existing code

Type

No type

Projects

No projects

Relationships

None yet

Development

No branches or pull requests

Issue actions