Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add option to override --crate-name from kani #3054

Merged
merged 9 commits into from
Mar 8, 2024
3 changes: 3 additions & 0 deletions kani-driver/src/args/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,9 @@ pub struct StandaloneArgs {

#[command(subcommand)]
pub command: Option<StandaloneSubcommand>,

#[arg(long, hide = true, requires("enable_unstable"))]
adpaco-aws marked this conversation as resolved.
Show resolved Hide resolved
pub crate_name: Option<String>,
}

/// Kani takes optional subcommands to request specialized behavior.
Expand Down
2 changes: 1 addition & 1 deletion kani-driver/src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ fn standalone_main() -> Result<()> {
print_kani_version(InvocationType::Standalone);
}

let project = project::standalone_project(&args.input.unwrap(), &session)?;
let project = project::standalone_project(&args.input.unwrap(), args.crate_name, &session)?;
if session.args.only_codegen { Ok(()) } else { verify_project(project, session) }
}

Expand Down
12 changes: 8 additions & 4 deletions kani-driver/src/project.rs
adpaco-aws marked this conversation as resolved.
Show resolved Hide resolved
Original file line number Diff line number Diff line change
Expand Up @@ -270,8 +270,12 @@ pub fn cargo_project(session: &KaniSession, keep_going: bool) -> Result<Project>
}

/// Generate a project directly using `kani-compiler` on a single crate.
pub fn standalone_project(input: &Path, session: &KaniSession) -> Result<Project> {
StandaloneProjectBuilder::try_new(input, session)?.build()
pub fn standalone_project(
input: &Path,
crate_name: Option<String>,
session: &KaniSession,
) -> Result<Project> {
StandaloneProjectBuilder::try_new(input, crate_name, session)?.build()
}

/// Builder for a standalone project.
Expand All @@ -291,15 +295,15 @@ struct StandaloneProjectBuilder<'a> {
impl<'a> StandaloneProjectBuilder<'a> {
/// Create a `StandaloneProjectBuilder` from the given input and session.
/// This will perform a few validations before the build.
fn try_new(input: &Path, session: &'a KaniSession) -> Result<Self> {
fn try_new(input: &Path, krate_name: Option<String>, session: &'a KaniSession) -> Result<Self> {
// Ensure the directory exist and it's in its canonical form.
let outdir = if let Some(target_dir) = &session.args.target_dir {
std::fs::create_dir_all(target_dir)?; // This is a no-op if directory exists.
target_dir.canonicalize()?
} else {
input.canonicalize().unwrap().parent().unwrap().to_path_buf()
};
let crate_name = crate_name(&input);
let crate_name = if let Some(name) = krate_name { name } else { crate_name(&input) };
let metadata = standalone_artifact(&outdir, &crate_name, Metadata);
Ok(StandaloneProjectBuilder {
outdir,
Expand Down
Loading