Skip to content

Commit

Permalink
Fix warnings about String (anvil-verifier#486)
Browse files Browse the repository at this point in the history 
Signed-off-by: Xudong Sun <[email protected]>
  • Loading branch information
@marshtompsxd
marshtompsxd authored May 31, 2024
1 parent aa5c32c commit c6c47af
Show file tree
Hide file tree
Showing 129 changed files with 1,094 additions and 1,221 deletions.
8 changes: 4 additions & 4 deletions src/conformance_tests/api_server.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -128,8 +128,8 @@ proptest! {
GeneratedRequest::Get{kind, name} => {
let get_request = KubeGetRequest {
api_resource: kind.to_api_resource(),
namespace: String::from_rust_string(namespace.to_string()),
name: String::from_rust_string(name.to_string()),
namespace: namespace.clone(),
name: name.clone(),
};
let model_resp = SimpleExecutableApiServerModel::handle_get_request(&get_request, &api_server_state);

Expand All @@ -148,12 +148,12 @@ proptest! {
GeneratedRequest::Create{kind, name} => {
let obj = {
let mut obj = kind.to_default_dynamic_object();
obj.set_name(String::from_rust_string(name));
obj.set_name(name);
obj
};
let create_request = KubeCreateRequest {
api_resource: kind.to_api_resource(),
namespace: String::from_rust_string(namespace.to_string()),
namespace: namespace.clone(),
obj: obj.clone(),
};
let model_resp = SimpleExecutableApiServerModel::handle_create_request(&create_request, &mut api_server_state);
Expand Down
2 changes: 1 addition & 1 deletion src/controller_examples/fluent_controller/fluentbit/exec/resource/common.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ pub fn make_base_labels(fb: &FluentBit) -> (labels: StringMap)
ensures labels@ == model_resource::make_base_labels(fb@),
{
let mut labels = StringMap::empty();
labels.insert(new_strlit("app").to_string(), fb.metadata().name().unwrap());
labels.insert("app".to_string(), fb.metadata().name().unwrap());
labels
}

Expand Down
48 changes: 24 additions & 24 deletions src/controller_examples/fluent_controller/fluentbit/exec/resource/daemon_set.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -169,7 +169,7 @@ fn make_fluentbit_pod_spec(fb: &FluentBit) -> (pod_spec: PodSpec)
let mut containers = Vec::new();
containers.push({
let mut fb_container = Container::default();
fb_container.set_name(new_strlit("fluent-bit").to_string());
fb_container.set_name("fluent-bit".to_string());
fb_container.set_image(fb.spec().image());
if fb.spec().image_pull_policy().is_some() {
fb_container.set_image_pull_policy(fb.spec().image_pull_policy().unwrap());
Expand Down Expand Up @@ -201,46 +201,46 @@ fn make_fluentbit_pod_spec(fb: &FluentBit) -> (pod_spec: PodSpec)
};
volume_mounts.push({
let mut volume_mount = VolumeMount::default();
volume_mount.set_name(new_strlit("config").to_string());
volume_mount.set_name("config".to_string());
volume_mount.set_read_only(true);
volume_mount.set_mount_path(new_strlit("/fluent-bit/config").to_string());
volume_mount.set_mount_path("/fluent-bit/config".to_string());
volume_mount
});
if !fb.spec().disable_log_volumes() {
volume_mounts.push({
let mut volume_mount = VolumeMount::default();
volume_mount.set_name(new_strlit("varlibcontainers").to_string());
volume_mount.set_name("varlibcontainers".to_string());
volume_mount.set_read_only(true);
if fb.spec().container_log_real_path().is_some() {
volume_mount.set_mount_path(fb.spec().container_log_real_path().unwrap());
} else {
volume_mount.set_mount_path(new_strlit("/containers").to_string());
volume_mount.set_mount_path("/containers".to_string());
}
volume_mount.overwrite_mount_propagation(fb.spec().internal_mount_propagation());
volume_mount
});
volume_mounts.push({
let mut volume_mount = VolumeMount::default();
volume_mount.set_name(new_strlit("varlogs").to_string());
volume_mount.set_name("varlogs".to_string());
volume_mount.set_read_only(true);
volume_mount.set_mount_path(new_strlit("/var/log/").to_string());
volume_mount.set_mount_path("/var/log/".to_string());
volume_mount.overwrite_mount_propagation(fb.spec().internal_mount_propagation());
volume_mount
});
volume_mounts.push({
let mut volume_mount = VolumeMount::default();
volume_mount.set_name(new_strlit("systemd").to_string());
volume_mount.set_name("systemd".to_string());
volume_mount.set_read_only(true);
volume_mount.set_mount_path(new_strlit("/var/log/journal").to_string());
volume_mount.set_mount_path("/var/log/journal".to_string());
volume_mount.overwrite_mount_propagation(fb.spec().internal_mount_propagation());
volume_mount
});
}
if fb.spec().position_db().is_some() {
volume_mounts.push({
let mut volume_mount = VolumeMount::default();
volume_mount.set_name(new_strlit("positions").to_string());
volume_mount.set_mount_path(new_strlit("/fluent-bit/tail").to_string());
volume_mount.set_name("positions".to_string());
volume_mount.set_mount_path("/fluent-bit/tail".to_string());
volume_mount
});
}
Expand All @@ -263,7 +263,7 @@ fn make_fluentbit_pod_spec(fb: &FluentBit) -> (pod_spec: PodSpec)
} else {
2020
};
ports.push(ContainerPort::new_with(new_strlit("metrics").to_string(), metrics_port));
ports.push(ContainerPort::new_with("metrics".to_string(), metrics_port));
proof {
assert_seqs_equal!(
[email protected]_values(|port: ContainerPort| port@),
Expand Down Expand Up @@ -300,7 +300,7 @@ fn make_fluentbit_pod_spec(fb: &FluentBit) -> (pod_spec: PodSpec)
};
volumes.push({
let mut volume = Volume::default();
volume.set_name(new_strlit("config").to_string());
volume.set_name("config".to_string());
volume.set_secret({
let mut secret = SecretVolumeSource::default();
secret.set_secret_name(fb.spec().fluentbit_config_name());
Expand All @@ -311,34 +311,34 @@ fn make_fluentbit_pod_spec(fb: &FluentBit) -> (pod_spec: PodSpec)
if !fb.spec().disable_log_volumes() {
volumes.push({
let mut volume = Volume::default();
volume.set_name(new_strlit("varlibcontainers").to_string());
volume.set_name("varlibcontainers".to_string());
volume.set_host_path({
let mut host_path = HostPathVolumeSource::default();
if fb.spec().container_log_real_path().is_some() {
host_path.set_path(fb.spec().container_log_real_path().unwrap());
} else {
host_path.set_path(new_strlit("/containers").to_string());
host_path.set_path("/containers".to_string());
}
host_path
});
volume
});
volumes.push({
let mut volume = Volume::default();
volume.set_name(new_strlit("varlogs").to_string());
volume.set_name("varlogs".to_string());
volume.set_host_path({
let mut host_path = HostPathVolumeSource::default();
host_path.set_path(new_strlit("/var/log").to_string());
host_path.set_path("/var/log".to_string());
host_path
});
volume
});
volumes.push({
let mut volume = Volume::default();
volume.set_name(new_strlit("systemd").to_string());
volume.set_name("systemd".to_string());
volume.set_host_path({
let mut host_path = HostPathVolumeSource::default();
host_path.set_path(new_strlit("/var/log/journal").to_string());
host_path.set_path("/var/log/journal".to_string());
host_path
});
volume
Expand All @@ -347,7 +347,7 @@ fn make_fluentbit_pod_spec(fb: &FluentBit) -> (pod_spec: PodSpec)
if fb.spec().position_db().is_some() {
volumes.push({
let mut volume = Volume::default();
volume.set_name(new_strlit("positions").to_string());
volume.set_name("positions".to_string());
volume.set_host_path(fb.spec().position_db().unwrap());
volume
});
Expand Down Expand Up @@ -382,16 +382,16 @@ fn make_env(fb: &FluentBit) -> (env_vars: Vec<EnvVar>)
{
let mut env_vars = Vec::new();
env_vars.push(EnvVar::new_with(
new_strlit("NODE_NAME").to_string(), None, Some(EnvVarSource::new_with_field_ref({
"NODE_NAME".to_string(), None, Some(EnvVarSource::new_with_field_ref({
let mut selector = ObjectFieldSelector::default();
selector.set_field_path(new_strlit("spec.nodeName").to_string());
selector.set_field_path("spec.nodeName".to_string());
selector
}))
));
env_vars.push(EnvVar::new_with(
new_strlit("HOST_IP").to_string(), None, Some(EnvVarSource::new_with_field_ref({
"HOST_IP".to_string(), None, Some(EnvVarSource::new_with_field_ref({
let mut selector = ObjectFieldSelector::default();
selector.set_field_path(new_strlit("status.hostIP").to_string());
selector.set_field_path("status.hostIP".to_string());
selector
}))
));
Expand Down
8 changes: 4 additions & 4 deletions src/controller_examples/fluent_controller/fluentbit/exec/resource/role.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,7 @@ pub fn make_role_name(fb: &FluentBit) -> (name: String)
requires [email protected]_formed(),
ensures name@ == model_resource::make_role_name(fb@),
{
fb.metadata().name().unwrap().concat(new_strlit("-role"))
fb.metadata().name().unwrap().concat("-role")
}

pub fn make_rules(fb: &FluentBit) -> (rules: Vec<PolicyRule>)
Expand All @@ -113,7 +113,7 @@ pub fn make_rules(fb: &FluentBit) -> (rules: Vec<PolicyRule>)
let mut rule = PolicyRule::default();
rule.set_api_groups({
let mut api_groups = Vec::new();
api_groups.push(new_strlit("").to_string());
api_groups.push("".to_string());
proof{
assert_seqs_equal!(
[email protected]_values(|p: String| p@),
Expand All @@ -124,7 +124,7 @@ pub fn make_rules(fb: &FluentBit) -> (rules: Vec<PolicyRule>)
});
rule.set_resources({
let mut resources = Vec::new();
resources.push(new_strlit("pods").to_string());
resources.push("pods".to_string());
proof{
assert_seqs_equal!(
[email protected]_values(|p: String| p@),
Expand All @@ -135,7 +135,7 @@ pub fn make_rules(fb: &FluentBit) -> (rules: Vec<PolicyRule>)
});
rule.set_verbs({
let mut verbs = Vec::new();
verbs.push(new_strlit("get").to_string());
verbs.push("get".to_string());
proof{
assert_seqs_equal!(
[email protected]_values(|p: String| p@),
Expand Down
8 changes: 4 additions & 4 deletions src/controller_examples/fluent_controller/fluentbit/exec/resource/role_binding.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,16 +103,16 @@ pub fn make_role_binding_name(fb: &FluentBit) -> (name: String)
requires [email protected]_formed(),
ensures name@ == model_resource::make_role_binding_name(fb@),
{
fb.metadata().name().unwrap().concat(new_strlit("-role-binding"))
fb.metadata().name().unwrap().concat("-role-binding")
}

pub fn make_role_ref(fb: &FluentBit) -> (role_ref: RoleRef)
requires [email protected]_formed(),
ensures role_ref@ == model_resource::make_role_binding(fb@).role_ref
{
let mut role_ref = RoleRef::default();
role_ref.set_api_group(new_strlit("rbac.authorization.k8s.io").to_string());
role_ref.set_kind(new_strlit("Role").to_string());
role_ref.set_api_group("rbac.authorization.k8s.io".to_string());
role_ref.set_kind("Role".to_string());
role_ref.set_name(make_role_name(fb));
role_ref
}
Expand All @@ -124,7 +124,7 @@ pub fn make_subjects(fb: &FluentBit) -> (subjects: Vec<Subject>)
let mut subjects = Vec::new();
subjects.push({
let mut subject = Subject::default();
subject.set_kind(new_strlit("ServiceAccount").to_string());
subject.set_kind("ServiceAccount".to_string());
subject.set_name(make_service_account_name(fb));
subject.set_namespace(fb.metadata().namespace().unwrap());
subject
Expand Down
2 changes: 1 addition & 1 deletion src/controller_examples/fluent_controller/fluentbit/exec/resource/service.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -143,7 +143,7 @@ pub fn make_service(fb: &FluentBit) -> (service: Service)
Vec::new()
};
let mut port = ServicePort::default();
port.set_name(new_strlit("metrics").to_string());
port.set_name("metrics".to_string());
if fb.spec().metrics_port().is_some() {
port.set_port(fb.spec().metrics_port().unwrap());
} else {
Expand Down
2 changes: 1 addition & 1 deletion src/controller_examples/fluent_controller/fluentbit/model/resource/common.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ use vstd::string::*;

verus! {

pub open spec fn make_base_labels(fb: FluentBitView) -> Map<StringView, StringView> { map![new_strlit("app")@ => fb.metadata.name.get_Some_0()] }
pub open spec fn make_base_labels(fb: FluentBitView) -> Map<StringView, StringView> { map!["app"@ => fb.metadata.name.get_Some_0()] }

pub open spec fn make_labels(fb: FluentBitView) -> Map<StringView, StringView> { fb.spec.labels.union_prefer_right(make_base_labels(fb)) }

Expand Down
Loading

0 comments on commit c6c47af

Please sign in to comment.