From bd09cbc973927bf7e62988c3171096e46cb1abad Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Wed, 13 Jul 2022 15:18:32 -0700 Subject: [PATCH 1/3] Fix env list parsing --- prusti-common/src/config.rs | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/prusti-common/src/config.rs b/prusti-common/src/config.rs index 78478b3c988..ee68afcc592 100644 --- a/prusti-common/src/config.rs +++ b/prusti-common/src/config.rs @@ -178,7 +178,14 @@ lazy_static::lazy_static! { // 4. Override with env variables (`PRUSTI_VIPER_BACKEND`, ...) settings.merge( - Environment::with_prefix("PRUSTI").ignore_empty(true) + Environment::with_prefix("PRUSTI") + .ignore_empty(true) + .try_parsing(true) + .with_list_parse_key("delete_basic_blocks") + .with_list_parse_key("extra_jvm_args") + .with_list_parse_key("extra_verifier_args") + .with_list_parse_key("verify_only_basic_block_path") + .list_separator("_") ).unwrap(); check_keys(&settings, &allowed_keys, "environment variables"); @@ -241,7 +248,7 @@ fn read_setting(name: &'static str) -> T where T: Deserialize<'static>, { - read_optional_setting(name).unwrap_or_else(|| panic!("Failed to read setting {:?}", name)) + SETTINGS.read().unwrap().get(name).expect(&format!("Failed to read setting {}", name)) } // The following methods are all convenience wrappers for the actual call to From 48db8f909d18a1ad8fb87f575e6c62d1d48fb528 Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Wed, 13 Jul 2022 15:52:07 -0700 Subject: [PATCH 2/3] Appease clippy --- prusti-common/src/config.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prusti-common/src/config.rs b/prusti-common/src/config.rs index ee68afcc592..aafaf89e401 100644 --- a/prusti-common/src/config.rs +++ b/prusti-common/src/config.rs @@ -248,7 +248,7 @@ fn read_setting(name: &'static str) -> T where T: Deserialize<'static>, { - SETTINGS.read().unwrap().get(name).expect(&format!("Failed to read setting {}", name)) + SETTINGS.read().unwrap().get(name).unwrap_or_else(|e| panic!("Failed to read setting {} due to {}", name, e)) } // The following methods are all convenience wrappers for the actual call to From 0767831e4dbc65423b6c6b2c26a0d394fa379b5c Mon Sep 17 00:00:00 2001 From: Zack Grannan Date: Wed, 13 Jul 2022 23:02:40 -0700 Subject: [PATCH 3/3] space makes more sense as list separator --- prusti-common/src/config.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prusti-common/src/config.rs b/prusti-common/src/config.rs index aafaf89e401..69ff7e94bce 100644 --- a/prusti-common/src/config.rs +++ b/prusti-common/src/config.rs @@ -185,7 +185,7 @@ lazy_static::lazy_static! { .with_list_parse_key("extra_jvm_args") .with_list_parse_key("extra_verifier_args") .with_list_parse_key("verify_only_basic_block_path") - .list_separator("_") + .list_separator(" ") ).unwrap(); check_keys(&settings, &allowed_keys, "environment variables");