From 70e8f3832aa0efca0764a25f492f6910ff37b734 Mon Sep 17 00:00:00 2001 From: Xudong Sun Date: Tue, 4 Jun 2024 00:54:15 -0500 Subject: [PATCH] Move unit tests out of `verus! { ... }` (#491) Signed-off-by: Xudong Sun --- Cargo.toml | 3 - src/conformance_tests/api_server.rs | 8 +- src/deps_hack/Cargo.lock | 133 +++++++++++ src/deps_hack/Cargo.toml | 1 + src/deps_hack/src/lib.rs | 1 + .../kubernetes_api_objects/affinity.rs | 4 - .../kubernetes_api_objects/api_method.rs | 221 +++++++----------- .../kubernetes_api_objects/api_resource.rs | 42 ++-- .../kubernetes_api_objects/config_map.rs | 86 +++---- .../config_map_projection.rs | 64 ++--- .../config_map_volume_source.rs | 49 ++-- .../kubernetes_api_objects/container.rs | 107 +++++---- .../kubernetes_api_objects/container_port.rs | 37 ++- .../kubernetes_api_objects/daemon_set.rs | 71 +++--- .../kubernetes_api_objects/daemon_set_spec.rs | 82 ++++--- .../daemon_set_status.rs | 38 +-- .../downward_api_volume_file.rs | 45 ++-- .../downward_api_volume_source.rs | 55 +++-- .../kubernetes_api_objects/dynamic_object.rs | 155 ++++++------ .../empty_dir_volume_source.rs | 32 +-- .../kubernetes_api_objects/env_var.rs | 31 ++- .../kubernetes_api_objects/env_var_source.rs | 23 +- .../kubernetes_api_objects/error.rs | 80 ++----- .../kubernetes_api_objects/exec_action.rs | 13 +- .../host_path_volume_source.rs | 37 +-- .../kubernetes_api_objects/key_to_path.rs | 17 +- .../kubernetes_api_objects/label_selector.rs | 22 +- .../kubernetes_api_objects/lifecycle.rs | 24 +- .../lifecycle_handler.rs | 19 +- .../local_object_reference.rs | 13 +- .../object_field_selector.rs | 37 +-- .../kubernetes_api_objects/object_meta.rs | 167 ++++++------- .../kubernetes_api_objects/owner_reference.rs | 9 +- .../persistent_volume_claim.rs | 89 +++---- .../persistent_volume_claim_spec.rs | 52 ++--- src/unit_tests/kubernetes_api_objects/pod.rs | 26 +-- .../pod_security_context.rs | 61 ++--- .../kubernetes_api_objects/pod_spec.rs | 119 ++++++---- .../pod_template_spec.rs | 47 ++-- .../kubernetes_api_objects/policy_rule.rs | 41 ++-- .../kubernetes_api_objects/probe.rs | 27 +-- .../projected_volume_source.rs | 49 ++-- .../resource_requirements.rs | 47 ++-- src/unit_tests/kubernetes_api_objects/role.rs | 133 ++++++----- .../kubernetes_api_objects/role_binding.rs | 142 +++++------ .../kubernetes_api_objects/role_ref.rs | 19 +- .../kubernetes_api_objects/secret.rs | 76 +++--- .../secret_projection.rs | 37 ++- .../secret_volume_source.rs | 38 ++- .../security_context.rs | 9 +- .../kubernetes_api_objects/service.rs | 70 +++--- .../kubernetes_api_objects/service_account.rs | 26 +-- .../kubernetes_api_objects/service_port.rs | 29 ++- .../kubernetes_api_objects/service_spec.rs | 140 +++++------ .../kubernetes_api_objects/stateful_set.rs | 165 +++++++------ ...ersistent_volume_claim_retention_policy.rs | 37 +-- .../stateful_set_spec.rs | 35 +-- .../stateful_set_status.rs | 46 ++-- .../kubernetes_api_objects/subject.rs | 34 +-- .../tcp_socket_action.rs | 33 +-- .../kubernetes_api_objects/toleration.rs | 26 +-- .../kubernetes_api_objects/volume.rs | 105 +++++---- .../kubernetes_api_objects/volume_mount.rs | 49 ++-- .../volume_projection.rs | 28 +-- src/unit_tests/vstd_ext/string_map.rs | 10 +- 65 files changed, 1704 insertions(+), 1867 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index f6d5bc93f..b451f12ac 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -10,6 +10,3 @@ vstd = { path = "../verus/source/vstd" } deps_hack = { path = "src/deps_hack" } tungstenite = "0.20.1" rand = "0.8" - -[dev-dependencies] -proptest = "1.4.0" diff --git a/src/conformance_tests/api_server.rs b/src/conformance_tests/api_server.rs index 4fa5d57be..6060a6d84 100644 --- a/src/conformance_tests/api_server.rs +++ b/src/conformance_tests/api_server.rs @@ -8,8 +8,8 @@ use deps_hack::kube::{ api::{Api, DeleteParams, ListParams, ObjectMeta, PostParams}, Client, }; +use deps_hack::proptest::prelude::*; use deps_hack::tokio::runtime::Runtime; -use proptest::prelude::*; use rand::Rng; use std::process::Command; use vstd::prelude::*; @@ -98,12 +98,14 @@ fn create_new_testing_namespace(len: usize) -> Option { ..Default::default() }; - namespace_api.create(&PostParams::default(), &namespace_obj).await + namespace_api + .create(&PostParams::default(), &namespace_obj) + .await }); match resp { Ok(_) => Some(namespace_name), - Err(_) => None + Err(_) => None, } } diff --git a/src/deps_hack/Cargo.lock b/src/deps_hack/Cargo.lock index ae6781ccf..305332b24 100644 --- a/src/deps_hack/Cargo.lock +++ b/src/deps_hack/Cargo.lock @@ -161,6 +161,21 @@ version = "0.22.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "72b3254f16251a8381aa12e40e3c4d2f0199f8c6508fbecb9d91f575e0fbb8c6" +[[package]] +name = "bit-set" +version = "0.5.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0700ddab506f33b20a03b13996eccd309a48e5ff77d0d95926aa0210fb4e95f1" +dependencies = [ + "bit-vec", +] + +[[package]] +name = "bit-vec" +version = "0.6.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "349f9b6a179ed607305526ca489b34ad0a41aed5f7980fa90eb03160b69598fb" + [[package]] name = "bitflags" version = "1.3.2" @@ -346,6 +361,7 @@ dependencies = [ "kube-client", "kube-core", "kube-derive", + "proptest", "rand", "schemars", "serde", @@ -397,6 +413,16 @@ version = "1.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" +[[package]] +name = "errno" +version = "0.3.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "534c5cf6194dfab3db3242765c03bbe257cf92f22b38f6bc0c58d59108a820ba" +dependencies = [ + "libc", + "windows-sys 0.52.0", +] + [[package]] name = "event-listener" version = "5.3.1" @@ -418,6 +444,12 @@ dependencies = [ "pin-project-lite", ] +[[package]] +name = "fastrand" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9fc0510504f03c51ada170672ac806f1f105a88aa97a5281117e1ddc3368e51a" + [[package]] name = "fnv" version = "1.0.7" @@ -997,6 +1029,12 @@ version = "0.2.151" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "302d7ab3130588088d277783b1e2d2e10c9e9e4a16dd9050e6ec93fb3e7048f4" +[[package]] +name = "libm" +version = "0.2.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4ec2a862134d2a7d32d7983ddcdd1c4923530833c9f2ea1a44fc5fa473989058" + [[package]] name = "linked-hash-map" version = "0.5.6" @@ -1012,6 +1050,12 @@ dependencies = [ "linked-hash-map", ] +[[package]] +name = "linux-raw-sys" +version = "0.4.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "78b3ae25bc7c8c38cec158d1f2757ee79e9b3740fbc7ccf0e59e4b08d793fa89" + [[package]] name = "lock_api" version = "0.4.11" @@ -1131,6 +1175,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "39e3200413f237f41ab11ad6d161bc7239c84dcb631773ccd7de3dfe4b5c267c" dependencies = [ "autocfg", + "libm", ] [[package]] @@ -1360,6 +1405,32 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "proptest" +version = "1.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "31b476131c3c86cb68032fdc5cb6d5a1045e3e42d96b69fa599fd77701e1f5bf" +dependencies = [ + "bit-set", + "bit-vec", + "bitflags 2.4.1", + "lazy_static", + "num-traits", + "rand", + "rand_chacha", + "rand_xorshift", + "regex-syntax", + "rusty-fork", + "tempfile", + "unarray", +] + +[[package]] +name = "quick-error" +version = "1.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1d01941d82fa2ab50be1e79e6714289dd7cde78eba4c074bc5a4374f650dfe0" + [[package]] name = "quote" version = "1.0.33" @@ -1399,6 +1470,15 @@ dependencies = [ "getrandom", ] +[[package]] +name = "rand_xorshift" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d25bf25ec5ae4a3f1b92f929810509a2f53d7dca2f50b794ff57e3face536c8f" +dependencies = [ + "rand_core", +] + [[package]] name = "redox_syscall" version = "0.4.1" @@ -1457,6 +1537,19 @@ version = "0.1.23" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d626bb9dae77e28219937af045c257c28bfd3f69333c512553507f5f9798cb76" +[[package]] +name = "rustix" +version = "0.38.28" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72e572a5e8ca657d7366229cdde4bd14c4eb5499a9573d4d366fe1b599daa316" +dependencies = [ + "bitflags 2.4.1", + "errno", + "libc", + "linux-raw-sys", + "windows-sys 0.52.0", +] + [[package]] name = "rustls" version = "0.23.8" @@ -1512,6 +1605,18 @@ dependencies = [ "untrusted", ] +[[package]] +name = "rusty-fork" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cb3dcc6e454c328bb824492db107ab7c0ae8fcffe4ad210136ef014458c1bc4f" +dependencies = [ + "fnv", + "quick-error", + "tempfile", + "wait-timeout", +] + [[package]] name = "ryu" version = "1.0.16" @@ -1766,6 +1871,19 @@ dependencies = [ "unicode-ident", ] +[[package]] +name = "tempfile" +version = "3.9.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "01ce4141aa927a6d1bd34a041795abd0db1cccba5d5f24b009f694bdf3a1f3fa" +dependencies = [ + "cfg-if 1.0.0", + "fastrand", + "redox_syscall", + "rustix", + "windows-sys 0.52.0", +] + [[package]] name = "thiserror" version = "1.0.51" @@ -2022,6 +2140,12 @@ version = "0.1.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ed646292ffc8188ef8ea4d1e0e0150fb15a5c2e12ad9b8fc191ae7a8a7f3c4b9" +[[package]] +name = "unarray" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "eaea85b334db583fe3274d12b4cd1880032beab409c0d774be044d4480ab9a94" + [[package]] name = "unicode-bidi" version = "0.3.14" @@ -2090,6 +2214,15 @@ version = "0.9.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f" +[[package]] +name = "wait-timeout" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9f200f5b12eb75f8c1ed65abd4b2db8a6e1b138a20de009dacee265a2498f3f6" +dependencies = [ + "libc", +] + [[package]] name = "want" version = "0.3.1" diff --git a/src/deps_hack/Cargo.toml b/src/deps_hack/Cargo.toml index 9790f8f42..b00af4bb9 100644 --- a/src/deps_hack/Cargo.toml +++ b/src/deps_hack/Cargo.toml @@ -33,3 +33,4 @@ base64 = "0.13.0" rand = "0.8" zookeeper = "0.8" chrono = "0.4.19" +proptest = "1.4.0" diff --git a/src/deps_hack/src/lib.rs b/src/deps_hack/src/lib.rs index b630d2776..56ab85d8c 100644 --- a/src/deps_hack/src/lib.rs +++ b/src/deps_hack/src/lib.rs @@ -7,6 +7,7 @@ pub use kube; pub use kube_client; pub use kube_core; pub use kube_derive; +pub use proptest; pub use rand; pub use schemars; pub use serde; diff --git a/src/unit_tests/kubernetes_api_objects/affinity.rs b/src/unit_tests/kubernetes_api_objects/affinity.rs index a64ea5df1..09d456574 100644 --- a/src/unit_tests/kubernetes_api_objects/affinity.rs +++ b/src/unit_tests/kubernetes_api_objects/affinity.rs @@ -9,10 +9,7 @@ use deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::Time; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for affinity #[test] -#[verifier(external)] pub fn test_kube() { let kube_affinity = deps_hack::k8s_openapi::api::core::v1::Affinity { node_affinity: Some(deps_hack::k8s_openapi::api::core::v1::NodeAffinity { @@ -30,4 +27,3 @@ pub fn test_kube() { assert_eq!(affinity.into_kube(), kube_affinity); } -} diff --git a/src/unit_tests/kubernetes_api_objects/api_method.rs b/src/unit_tests/kubernetes_api_objects/api_method.rs index 9606b7203..88039b276 100644 --- a/src/unit_tests/kubernetes_api_objects/api_method.rs +++ b/src/unit_tests/kubernetes_api_objects/api_method.rs @@ -11,185 +11,138 @@ use deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::Time; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for api method #[test] -#[verifier(external)] pub fn test_getrequest_key() { let api_method = KubeGetRequest { - api_resource: ApiResource::from_kube( - deps_hack::kube::api::ApiResource { - group: "group".to_string(), - version: "version".to_string(), - kind: "kind".to_string(), - api_version: "api_version".to_string(), - plural: "plural".to_string(), - }, - ), + api_resource: ApiResource::from_kube(deps_hack::kube::api::ApiResource { + group: "group".to_string(), + version: "version".to_string(), + kind: "kind".to_string(), + api_version: "api_version".to_string(), + plural: "plural".to_string(), + }), name: "name".to_string(), namespace: "namespace".to_string(), }; - assert_eq!( - api_method.key(), - "kind/namespace/name" - ); + assert_eq!(api_method.key(), "kind/namespace/name"); } #[test] -#[verifier(external)] pub fn test_listrequest_key() { let api_method = KubeListRequest { - api_resource: ApiResource::from_kube( - deps_hack::kube::api::ApiResource { - group: "group".to_string(), - version: "version".to_string(), - kind: "kind".to_string(), - api_version: "api_version".to_string(), - plural: "plural".to_string(), - }, - ), + api_resource: ApiResource::from_kube(deps_hack::kube::api::ApiResource { + group: "group".to_string(), + version: "version".to_string(), + kind: "kind".to_string(), + api_version: "api_version".to_string(), + plural: "plural".to_string(), + }), namespace: "namespace".to_string(), }; - assert_eq!( - api_method.key(), - "kind/namespace" - ); + assert_eq!(api_method.key(), "kind/namespace"); } #[test] -#[verifier(external)] pub fn test_createquest_key() { let api_method = KubeCreateRequest { - api_resource: ApiResource::from_kube( - deps_hack::kube::api::ApiResource { - group: "group".to_string(), - version: "version".to_string(), - kind: "kind".to_string(), - api_version: "api_version".to_string(), - plural: "plural".to_string(), - }, - ), + api_resource: ApiResource::from_kube(deps_hack::kube::api::ApiResource { + group: "group".to_string(), + version: "version".to_string(), + kind: "kind".to_string(), + api_version: "api_version".to_string(), + plural: "plural".to_string(), + }), namespace: "namespace".to_string(), - obj: DynamicObject::from_kube( - deps_hack::kube::api::DynamicObject { - metadata: deps_hack::kube::api::ObjectMeta { - name: Some("dyn_name".to_string()), - namespace: Some("namespace".to_string()), - ..Default::default() - }, - types: Some(deps_hack::kube::api::TypeMeta { - api_version: "api_version".to_string(), - kind: "kind".to_string(), - }), - data: deps_hack::serde_json::json!({ - "key": "value", - }), + obj: DynamicObject::from_kube(deps_hack::kube::api::DynamicObject { + metadata: deps_hack::kube::api::ObjectMeta { + name: Some("dyn_name".to_string()), + namespace: Some("namespace".to_string()), + ..Default::default() }, - ) + types: Some(deps_hack::kube::api::TypeMeta { + api_version: "api_version".to_string(), + kind: "kind".to_string(), + }), + data: deps_hack::serde_json::json!({ + "key": "value", + }), + }), }; - assert_eq!( - api_method.key(), - "kind/namespace/dyn_name" - ); + assert_eq!(api_method.key(), "kind/namespace/dyn_name"); } #[test] -#[verifier(external)] pub fn test_deleterequest_key() { let api_method = KubeDeleteRequest { - api_resource: ApiResource::from_kube( - deps_hack::kube::api::ApiResource { - group: "group".to_string(), - version: "version".to_string(), - kind: "kind".to_string(), - api_version: "api_version".to_string(), - plural: "plural".to_string(), - }, - ), + api_resource: ApiResource::from_kube(deps_hack::kube::api::ApiResource { + group: "group".to_string(), + version: "version".to_string(), + kind: "kind".to_string(), + api_version: "api_version".to_string(), + plural: "plural".to_string(), + }), name: "name".to_string(), namespace: "namespace".to_string(), }; - assert_eq!( - api_method.key(), - "kind/namespace/name" - ); + assert_eq!(api_method.key(), "kind/namespace/name"); } #[test] -#[verifier(external)] pub fn test_updaterequest_key() { let api_method = KubeUpdateRequest { - api_resource: ApiResource::from_kube( - deps_hack::kube::api::ApiResource { - group: "group".to_string(), - version: "version".to_string(), - kind: "kind".to_string(), - api_version: "api_version".to_string(), - plural: "plural".to_string(), - }, - ), + api_resource: ApiResource::from_kube(deps_hack::kube::api::ApiResource { + group: "group".to_string(), + version: "version".to_string(), + kind: "kind".to_string(), + api_version: "api_version".to_string(), + plural: "plural".to_string(), + }), name: "name".to_string(), namespace: "namespace".to_string(), - obj: DynamicObject::from_kube( - deps_hack::kube::api::DynamicObject { - metadata: deps_hack::kube::api::ObjectMeta { - name: Some("dyn_name".to_string()), - namespace: Some("namespace".to_string()), - ..Default::default() - }, - types: Some(deps_hack::kube::api::TypeMeta { - api_version: "api_version".to_string(), - kind: "kind".to_string(), - }), - data: deps_hack::serde_json::json!({ - "key": "value", - }), + obj: DynamicObject::from_kube(deps_hack::kube::api::DynamicObject { + metadata: deps_hack::kube::api::ObjectMeta { + name: Some("dyn_name".to_string()), + namespace: Some("namespace".to_string()), + ..Default::default() }, - ) + types: Some(deps_hack::kube::api::TypeMeta { + api_version: "api_version".to_string(), + kind: "kind".to_string(), + }), + data: deps_hack::serde_json::json!({ + "key": "value", + }), + }), }; - assert_eq!( - api_method.key(), - "kind/namespace/name" - ); + assert_eq!(api_method.key(), "kind/namespace/name"); } #[test] -#[verifier(external)] pub fn test_updatestatusrequest_key() { let api_method = KubeUpdateStatusRequest { - api_resource: ApiResource::from_kube( - deps_hack::kube::api::ApiResource { - group: "group".to_string(), - version: "version".to_string(), - kind: "kind".to_string(), - api_version: "api_version".to_string(), - plural: "plural".to_string(), - }, - ), + api_resource: ApiResource::from_kube(deps_hack::kube::api::ApiResource { + group: "group".to_string(), + version: "version".to_string(), + kind: "kind".to_string(), + api_version: "api_version".to_string(), + plural: "plural".to_string(), + }), name: "name".to_string(), namespace: "namespace".to_string(), - obj: DynamicObject::from_kube( - deps_hack::kube::api::DynamicObject { - metadata: deps_hack::kube::api::ObjectMeta { - name: Some("dyn_name".to_string()), - namespace: Some("namespace".to_string()), - ..Default::default() - }, - types: Some(deps_hack::kube::api::TypeMeta { - api_version: "api_version".to_string(), - kind: "kind".to_string(), - }), - data: deps_hack::serde_json::json!({ - "key": "value", - }), + obj: DynamicObject::from_kube(deps_hack::kube::api::DynamicObject { + metadata: deps_hack::kube::api::ObjectMeta { + name: Some("dyn_name".to_string()), + namespace: Some("namespace".to_string()), + ..Default::default() }, - ) + types: Some(deps_hack::kube::api::TypeMeta { + api_version: "api_version".to_string(), + kind: "kind".to_string(), + }), + data: deps_hack::serde_json::json!({ + "key": "value", + }), + }), }; - assert_eq!( - api_method.key(), - "kind/namespace/name" - ); -} - - + assert_eq!(api_method.key(), "kind/namespace/name"); } diff --git a/src/unit_tests/kubernetes_api_objects/api_resource.rs b/src/unit_tests/kubernetes_api_objects/api_resource.rs index 5259a26dd..86b258abc 100644 --- a/src/unit_tests/kubernetes_api_objects/api_resource.rs +++ b/src/unit_tests/kubernetes_api_objects/api_resource.rs @@ -9,38 +9,28 @@ use deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::Time; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for api resource #[test] -#[verifier(external)] pub fn test_kube() { - let kube_api_resource = - deps_hack::kube::api::ApiResource { - group: "group".to_string(), - version: "version".to_string(), - kind: "kind".to_string(), - api_version: "api_version".to_string(), - plural: "plural".to_string(), - }; + let kube_api_resource = deps_hack::kube::api::ApiResource { + group: "group".to_string(), + version: "version".to_string(), + kind: "kind".to_string(), + api_version: "api_version".to_string(), + plural: "plural".to_string(), + }; let api_resource = ApiResource::from_kube(kube_api_resource.clone()); - assert_eq!( - api_resource.into_kube(), - kube_api_resource - ); + assert_eq!(api_resource.into_kube(), kube_api_resource); } #[test] -#[verifier(external)] pub fn test_as_kube_ref() { - let api_resource = ApiResource::from_kube( - deps_hack::kube::api::ApiResource { - group: "group".to_string(), - version: "version".to_string(), - kind: "kind".to_string(), - api_version: "api_version".to_string(), - plural: "plural".to_string(), - }, - ); + let api_resource = ApiResource::from_kube(deps_hack::kube::api::ApiResource { + group: "group".to_string(), + version: "version".to_string(), + kind: "kind".to_string(), + api_version: "api_version".to_string(), + plural: "plural".to_string(), + }); assert_eq!( api_resource.as_kube_ref(), &deps_hack::kube::api::ApiResource { @@ -52,5 +42,3 @@ pub fn test_as_kube_ref() { } ); } - -} diff --git a/src/unit_tests/kubernetes_api_objects/config_map.rs b/src/unit_tests/kubernetes_api_objects/config_map.rs index 356619e12..fbe1f9ebb 100644 --- a/src/unit_tests/kubernetes_api_objects/config_map.rs +++ b/src/unit_tests/kubernetes_api_objects/config_map.rs @@ -8,10 +8,7 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { - #[test] -#[verifier(external)] pub fn test_set_metadata() { let mut object_meta = ObjectMeta::default(); object_meta.set_name("name".to_string()); @@ -22,8 +19,7 @@ pub fn test_set_metadata() { } #[test] -#[verifier(external)] -pub fn test_set_data(){ +pub fn test_set_data() { let mut config_map = ConfigMap::default(); let mut data = StringMap::new(); data.insert("key".to_string(), "value".to_string()); @@ -32,15 +28,16 @@ pub fn test_set_data(){ } #[test] -#[verifier(external)] -pub fn test_default(){ +pub fn test_default() { let config_map = ConfigMap::default(); - assert_eq!(config_map.into_kube(), deps_hack::k8s_openapi::api::core::v1::ConfigMap::default()); + assert_eq!( + config_map.into_kube(), + deps_hack::k8s_openapi::api::core::v1::ConfigMap::default() + ); } #[test] -#[verifier(external)] -pub fn test_clone(){ +pub fn test_clone() { let mut config_map = ConfigMap::default(); let mut data = StringMap::new(); data.insert("key".to_string(), "value".to_string()); @@ -50,8 +47,7 @@ pub fn test_clone(){ } #[test] -#[verifier(external)] -pub fn test_metadata(){ +pub fn test_metadata() { let mut object_meta = ObjectMeta::default(); object_meta.set_name("name".to_string()); @@ -61,77 +57,63 @@ pub fn test_metadata(){ } #[test] -#[verifier(external)] -pub fn test_data(){ +pub fn test_data() { let mut config_map = ConfigMap::default(); let mut data = StringMap::new(); data.insert("key".to_string(), "value".to_string()); config_map.set_data(data.clone()); - assert_eq!(data.into_rust_map(), config_map.data().unwrap().into_rust_map()); + assert_eq!( + data.into_rust_map(), + config_map.data().unwrap().into_rust_map() + ); } #[test] -#[verifier(external)] -pub fn test_api_resource(){ +pub fn test_api_resource() { let api_resource = ConfigMap::api_resource(); assert_eq!(api_resource.into_kube().kind, "ConfigMap"); } #[test] -#[verifier(external)] pub fn test_kube() { let kube_config_map = deps_hack::k8s_openapi::api::core::v1::ConfigMap { - metadata: - deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - name: Some("name".to_string()), - ..Default::default() - }, + metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), + ..Default::default() + }, data: Some( - vec![( - "key".to_string(), - "value".to_string(), - )] - .into_iter() - .collect(), + vec![("key".to_string(), "value".to_string())] + .into_iter() + .collect(), ), ..Default::default() }; - let config_map = ConfigMap::from_kube( - kube_config_map.clone(), - ); + let config_map = ConfigMap::from_kube(kube_config_map.clone()); - assert_eq!(config_map.into_kube(), - kube_config_map); + assert_eq!(config_map.into_kube(), kube_config_map); } #[test] -#[verifier(external)] pub fn test_marshal() { let kube_config_map = deps_hack::k8s_openapi::api::core::v1::ConfigMap { - metadata: - deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - name: Some("name".to_string()), - ..Default::default() - }, + metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), + ..Default::default() + }, data: Some( - vec![( - "key".to_string(), - "value".to_string(), - )] - .into_iter() - .collect(), + vec![("key".to_string(), "value".to_string())] + .into_iter() + .collect(), ), ..Default::default() }; - let config_map = ConfigMap::from_kube( - kube_config_map.clone(), - ); + let config_map = ConfigMap::from_kube(kube_config_map.clone()); assert_eq!( kube_config_map, - ConfigMap::unmarshal(config_map.marshal()).unwrap().into_kube() + ConfigMap::unmarshal(config_map.marshal()) + .unwrap() + .into_kube() ); } - -} diff --git a/src/unit_tests/kubernetes_api_objects/config_map_projection.rs b/src/unit_tests/kubernetes_api_objects/config_map_projection.rs index 88c3edc62..1d8ee8f51 100644 --- a/src/unit_tests/kubernetes_api_objects/config_map_projection.rs +++ b/src/unit_tests/kubernetes_api_objects/config_map_projection.rs @@ -9,25 +9,26 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for configmap projecion #[test] -#[verifier(external)] pub fn test_default() { let config_map_projection = ConfigMapProjection::default(); - assert_eq!(config_map_projection.into_kube(), deps_hack::k8s_openapi::api::core::v1::ConfigMapProjection::default()); + assert_eq!( + config_map_projection.into_kube(), + deps_hack::k8s_openapi::api::core::v1::ConfigMapProjection::default() + ); } #[test] -#[verifier(external)] pub fn test_set_name() { let mut config_map_projection = ConfigMapProjection::default(); config_map_projection.set_name("name".to_string()); - assert_eq!("name".to_string(), config_map_projection.into_kube().name.unwrap()); + assert_eq!( + "name".to_string(), + config_map_projection.into_kube().name.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_items() { let mut config_map_projection = ConfigMapProjection::default(); let key_to_paths_gen = || { @@ -53,7 +54,6 @@ pub fn test_set_items() { } #[test] -#[verifier(external)] pub fn test_clone() { let mut config_map_projection = ConfigMapProjection::default(); config_map_projection.set_name("name".to_string()); @@ -68,32 +68,34 @@ pub fn test_clone() { key_to_paths.push(key_to_path_2); config_map_projection.set_items(key_to_paths); let config_map_projection_clone = config_map_projection.clone(); - assert_eq!(config_map_projection.into_kube(), config_map_projection_clone.into_kube()); + assert_eq!( + config_map_projection.into_kube(), + config_map_projection_clone.into_kube() + ); } #[test] -#[verifier(external)] -pub fn test_kube(){ - let kube_config_map_projection = - deps_hack::k8s_openapi::api::core::v1::ConfigMapProjection { - name: Some("name".to_string()), - items: Some(vec![ - deps_hack::k8s_openapi::api::core::v1::KeyToPath { - key: "key1".to_string(), - path: "path1".to_string(), - mode: None, - }, - deps_hack::k8s_openapi::api::core::v1::KeyToPath { - key: "key2".to_string(), - path: "path2".to_string(), - mode: None, - }, - ]), - optional: None, - }; +pub fn test_kube() { + let kube_config_map_projection = deps_hack::k8s_openapi::api::core::v1::ConfigMapProjection { + name: Some("name".to_string()), + items: Some(vec![ + deps_hack::k8s_openapi::api::core::v1::KeyToPath { + key: "key1".to_string(), + path: "path1".to_string(), + mode: None, + }, + deps_hack::k8s_openapi::api::core::v1::KeyToPath { + key: "key2".to_string(), + path: "path2".to_string(), + mode: None, + }, + ]), + optional: None, + }; let config_map_projection = ConfigMapProjection::from_kube(kube_config_map_projection.clone()); - assert_eq!(config_map_projection.into_kube(), - kube_config_map_projection); -} + assert_eq!( + config_map_projection.into_kube(), + kube_config_map_projection + ); } diff --git a/src/unit_tests/kubernetes_api_objects/config_map_volume_source.rs b/src/unit_tests/kubernetes_api_objects/config_map_volume_source.rs index adae947f8..61a99fff8 100644 --- a/src/unit_tests/kubernetes_api_objects/config_map_volume_source.rs +++ b/src/unit_tests/kubernetes_api_objects/config_map_volume_source.rs @@ -9,46 +9,51 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for config map volume source #[test] -#[verifier(external)] pub fn test_default() { let config_map_volume_source = ConfigMapVolumeSource::default(); - assert_eq!(config_map_volume_source.into_kube(), deps_hack::k8s_openapi::api::core::v1::ConfigMapVolumeSource::default()); + assert_eq!( + config_map_volume_source.into_kube(), + deps_hack::k8s_openapi::api::core::v1::ConfigMapVolumeSource::default() + ); } #[test] -#[verifier(external)] pub fn test_set_name() { let mut config_map_volume_source = ConfigMapVolumeSource::default(); config_map_volume_source.set_name("name".to_string()); - assert_eq!("name".to_string(), config_map_volume_source.into_kube().name.unwrap()); + assert_eq!( + "name".to_string(), + config_map_volume_source.into_kube().name.unwrap() + ); } #[test] -#[verifier(external)] -pub fn test_clone(){ +pub fn test_clone() { let mut config_map_volume_source = ConfigMapVolumeSource::default(); config_map_volume_source.set_name("name".to_string()); let config_map_volume_source_clone = config_map_volume_source.clone(); - assert_eq!(config_map_volume_source.into_kube(), config_map_volume_source_clone.into_kube()); + assert_eq!( + config_map_volume_source.into_kube(), + config_map_volume_source_clone.into_kube() + ); } #[test] -#[verifier(external)] -pub fn test_kube(){ - let kube_config_map_volume_source = deps_hack::k8s_openapi::api::core::v1::ConfigMapVolumeSource{ - default_mode: None, - items: None, - name: Some("name".to_string()), - optional: None, - }; +pub fn test_kube() { + let kube_config_map_volume_source = + deps_hack::k8s_openapi::api::core::v1::ConfigMapVolumeSource { + default_mode: None, + items: None, + name: Some("name".to_string()), + optional: None, + }; - let config_map_volume_source = ConfigMapVolumeSource::from_kube(kube_config_map_volume_source.clone()); - - assert_eq!(config_map_volume_source.into_kube(), - kube_config_map_volume_source); -} + let config_map_volume_source = + ConfigMapVolumeSource::from_kube(kube_config_map_volume_source.clone()); + assert_eq!( + config_map_volume_source.into_kube(), + kube_config_map_volume_source + ); } diff --git a/src/unit_tests/kubernetes_api_objects/container.rs b/src/unit_tests/kubernetes_api_objects/container.rs index ed06f68f4..795f67b3a 100644 --- a/src/unit_tests/kubernetes_api_objects/container.rs +++ b/src/unit_tests/kubernetes_api_objects/container.rs @@ -7,10 +7,7 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { - #[test] -#[verifier(external)] pub fn test_set_image() { let mut container = Container::default(); container.set_image("image".to_string()); @@ -18,16 +15,13 @@ pub fn test_set_image() { } #[test] -#[verifier(external)] pub fn test_set_name() { let mut container = Container::default(); container.set_name("name".to_string()); assert_eq!("name".to_string(), container.into_kube().name); } - #[test] -#[verifier(external)] pub fn test_set_volume_mounts() { let mut container = Container::default(); let volume_mounts = || { @@ -40,12 +34,16 @@ pub fn test_set_volume_mounts() { volume_mounts }; container.set_volume_mounts(volume_mounts()); - assert_eq!(volume_mounts().into_iter().map(|v: VolumeMount| v.into_kube()).collect::>(), - container.into_kube().volume_mounts.unwrap()); + assert_eq!( + volume_mounts() + .into_iter() + .map(|v: VolumeMount| v.into_kube()) + .collect::>(), + container.into_kube().volume_mounts.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_ports() { let mut container = Container::default(); let ports = || { @@ -57,14 +55,16 @@ pub fn test_set_ports() { ports }; container.set_ports(ports()); - assert_eq!(ports().into_iter().map(|v: ContainerPort| v.into_kube()).collect::>(), - container.into_kube().ports.unwrap()); + assert_eq!( + ports() + .into_iter() + .map(|v: ContainerPort| v.into_kube()) + .collect::>(), + container.into_kube().ports.unwrap() + ); } - - #[test] -#[verifier(external)] pub fn test_set_lifecycle() { let mut container = Container::default(); @@ -76,11 +76,13 @@ pub fn test_set_lifecycle() { lifecycle.set_pre_stop(handler); container.set_lifecycle(lifecycle.clone()); - assert_eq!(lifecycle.into_kube(), container.into_kube().lifecycle.unwrap()); + assert_eq!( + lifecycle.into_kube(), + container.into_kube().lifecycle.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_resources() { let mut container = Container::default(); @@ -90,11 +92,13 @@ pub fn test_set_resources() { resources.set_requests(requests); container.set_resources(resources.clone()); - assert_eq!(resources.into_kube(), container.into_kube().resources.unwrap()); + assert_eq!( + resources.into_kube(), + container.into_kube().resources.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_liveness_probe() { let mut container = Container::default(); let mut probe = Probe::default(); @@ -104,11 +108,13 @@ pub fn test_set_liveness_probe() { probe.set_tcp_socket(tcp_socket_action); container.set_liveness_probe(probe.clone()); - assert_eq!(probe.into_kube(), container.into_kube().liveness_probe.unwrap()); + assert_eq!( + probe.into_kube(), + container.into_kube().liveness_probe.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_readiness_probe() { let mut container = Container::default(); let mut probe = Probe::default(); @@ -118,54 +124,66 @@ pub fn test_set_readiness_probe() { probe.set_tcp_socket(tcp_socket_action); container.set_readiness_probe(probe.clone()); - assert_eq!(probe.into_kube(), container.into_kube().readiness_probe.unwrap()); + assert_eq!( + probe.into_kube(), + container.into_kube().readiness_probe.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_command() { let mut container = Container::default(); container.set_command(vec!["command".to_string()]); - assert_eq!(vec!["command".to_string()], container.into_kube().command.unwrap()); + assert_eq!( + vec!["command".to_string()], + container.into_kube().command.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_image_pull_policy() { let mut container = Container::default(); container.set_image_pull_policy("image_pull_policy".to_string()); - assert_eq!("image_pull_policy".to_string(), container.into_kube().image_pull_policy.unwrap()); + assert_eq!( + "image_pull_policy".to_string(), + container.into_kube().image_pull_policy.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_env() { let env_var = EnvVar::from_kube(deps_hack::k8s_openapi::api::core::v1::EnvVar::default()); let mut container = Container::default(); container.set_env(vec![env_var.clone()]); - assert_eq!(vec![env_var.into_kube()], container.into_kube().env.unwrap()); + assert_eq!( + vec![env_var.into_kube()], + container.into_kube().env.unwrap() + ); } #[test] -#[verifier(external)] -pub fn test_default(){ +pub fn test_default() { let container = Container::default(); - assert_eq!(container.into_kube(), deps_hack::k8s_openapi::api::core::v1::Container::default()); + assert_eq!( + container.into_kube(), + deps_hack::k8s_openapi::api::core::v1::Container::default() + ); } #[test] -#[verifier(external)] -pub fn test_set_args(){ +pub fn test_set_args() { let mut container = Container::default(); container.set_args(vec!["args".to_string()]); - assert_eq!(vec!["args".to_string()], container.into_kube().args.unwrap()); + assert_eq!( + vec!["args".to_string()], + container.into_kube().args.unwrap() + ); } #[test] -#[verifier(external)] -pub fn test_set_security_context(){ +pub fn test_set_security_context() { let mut container = Container::default(); - let kube_security_context = deps_hack::k8s_openapi::api::core::v1::SecurityContext { + let kube_security_context = deps_hack::k8s_openapi::api::core::v1::SecurityContext { run_as_user: Some(1000), run_as_group: Some(1000), privileged: Some(true), @@ -174,12 +192,14 @@ pub fn test_set_security_context(){ let security_context = SecurityContext::from_kube(kube_security_context.clone()); container.set_security_context(security_context); - assert_eq!(kube_security_context, container.into_kube().security_context.unwrap()); + assert_eq!( + kube_security_context, + container.into_kube().security_context.unwrap() + ); } #[test] -#[verifier(external)] -pub fn test_clone(){ +pub fn test_clone() { let mut container = Container::default(); container.set_image("image".to_string()); let container_clone = container.clone(); @@ -187,7 +207,6 @@ pub fn test_clone(){ } #[test] -#[verifier(external)] pub fn test_kube() { let kube_container = deps_hack::k8s_openapi::api::core::v1::Container { name: "name".to_string(), @@ -197,8 +216,7 @@ pub fn test_kube() { let container = Container::from_kube(kube_container.clone()); - assert_eq!(container.into_kube(), - kube_container.clone()); + assert_eq!(container.into_kube(), kube_container.clone()); let kube_container = deps_hack::k8s_openapi::api::core::v1::Container { name: "name_2".to_string(), @@ -216,8 +234,5 @@ pub fn test_kube() { let container = Container::from_kube(kube_container.clone()); - assert_eq!(container.into_kube(), - kube_container.clone()); - -} + assert_eq!(container.into_kube(), kube_container.clone()); } diff --git a/src/unit_tests/kubernetes_api_objects/container_port.rs b/src/unit_tests/kubernetes_api_objects/container_port.rs index f99328fb4..6953cb863 100644 --- a/src/unit_tests/kubernetes_api_objects/container_port.rs +++ b/src/unit_tests/kubernetes_api_objects/container_port.rs @@ -7,19 +7,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { - -// Tests for ports(ContainerPort) #[test] -#[verifier(external)] pub fn test_default() { let container_port = ContainerPort::default(); - assert_eq!(container_port.into_kube(), deps_hack::k8s_openapi::api::core::v1::ContainerPort::default()); + assert_eq!( + container_port.into_kube(), + deps_hack::k8s_openapi::api::core::v1::ContainerPort::default() + ); } - #[test] -#[verifier(external)] pub fn test_set_container_port() { let mut container_port = ContainerPort::default(); container_port.set_container_port(8080); @@ -27,7 +24,6 @@ pub fn test_set_container_port() { } #[test] -#[verifier(external)] pub fn test_set_name() { let mut container_port = ContainerPort::default(); container_port.set_name("name".to_string()); @@ -35,7 +31,6 @@ pub fn test_set_name() { } #[test] -#[verifier(external)] pub fn test_name() { let mut container_port = ContainerPort::default(); let temp = container_port.name(); @@ -47,7 +42,6 @@ pub fn test_name() { } #[test] -#[verifier(external)] pub fn test_container_port() { let mut container_port = ContainerPort::default(); container_port.set_container_port(8080); @@ -55,26 +49,25 @@ pub fn test_container_port() { } #[test] -#[verifier(external)] pub fn test_protocol() { let container_port = ContainerPort::default(); let temp = container_port.protocol(); if !temp.is_none() { panic!("protocol should be none"); } - let container_port = ContainerPort::from_kube(deps_hack::k8s_openapi::api::core::v1::ContainerPort { - container_port: 8080, - host_ip: Some("host_ip".to_string()), - host_port: Some(8080), - name: Some("name".to_string()), - protocol: Some("protocol".to_string()), - ..Default::default() - }); + let container_port = + ContainerPort::from_kube(deps_hack::k8s_openapi::api::core::v1::ContainerPort { + container_port: 8080, + host_ip: Some("host_ip".to_string()), + host_port: Some(8080), + name: Some("name".to_string()), + protocol: Some("protocol".to_string()), + ..Default::default() + }); assert_eq!("protocol".to_string(), container_port.protocol().unwrap()); } #[test] -#[verifier(external)] pub fn test_kube() { let kube_container_port = deps_hack::k8s_openapi::api::core::v1::ContainerPort { container_port: 8080, @@ -86,7 +79,5 @@ pub fn test_kube() { let container_port = ContainerPort::from_kube(kube_container_port.clone()); - assert_eq!(container_port.into_kube(), - kube_container_port); -} + assert_eq!(container_port.into_kube(), kube_container_port); } diff --git a/src/unit_tests/kubernetes_api_objects/daemon_set.rs b/src/unit_tests/kubernetes_api_objects/daemon_set.rs index 30fdff3b6..7f199695c 100644 --- a/src/unit_tests/kubernetes_api_objects/daemon_set.rs +++ b/src/unit_tests/kubernetes_api_objects/daemon_set.rs @@ -9,18 +9,17 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for daemon set #[test] -#[verifier(external)] pub fn test_default() { let daemon_set = DaemonSet::default(); - assert_eq!(daemon_set.into_kube(), deps_hack::k8s_openapi::api::apps::v1::DaemonSet::default()); + assert_eq!( + daemon_set.into_kube(), + deps_hack::k8s_openapi::api::apps::v1::DaemonSet::default() + ); } #[test] -#[verifier(external)] -pub fn test_set_metadata(){ +pub fn test_set_metadata() { let mut object_meta = ObjectMeta::default(); object_meta.set_name("name".to_string()); let mut daemon_set = DaemonSet::default(); @@ -29,8 +28,7 @@ pub fn test_set_metadata(){ } #[test] -#[verifier(external)] -pub fn test_metadata(){ +pub fn test_metadata() { let mut object_meta = ObjectMeta::default(); object_meta.set_name("name".to_string()); let mut daemon_set = DaemonSet::default(); @@ -39,7 +37,6 @@ pub fn test_metadata(){ } #[test] -#[verifier(external)] pub fn test_set_sepc() { let mut daemon_set = DaemonSet::default(); let mut daemon_set_spec = DaemonSetSpec::default(); @@ -49,11 +46,13 @@ pub fn test_set_sepc() { label_selector.set_match_labels(match_labels.clone()); daemon_set_spec.set_selector(label_selector.clone()); daemon_set.set_spec(daemon_set_spec.clone()); - assert_eq!(daemon_set_spec.into_kube(), daemon_set.into_kube().spec.unwrap()); + assert_eq!( + daemon_set_spec.into_kube(), + daemon_set.into_kube().spec.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_spec() { let mut daemon_set = DaemonSet::default(); let temp = daemon_set.spec(); @@ -67,18 +66,19 @@ pub fn test_spec() { label_selector.set_match_labels(match_labels.clone()); daemon_set_spec.set_selector(label_selector.clone()); daemon_set.set_spec(daemon_set_spec.clone()); - assert_eq!(daemon_set_spec.into_kube(), daemon_set.spec().unwrap().into_kube()); + assert_eq!( + daemon_set_spec.into_kube(), + daemon_set.spec().unwrap().into_kube() + ); } #[test] -#[verifier(external)] pub fn test_api_resource() { let api_resource = DaemonSet::api_resource(); assert_eq!(api_resource.into_kube().kind, "DaemonSet"); } #[test] -#[verifier(external)] pub fn test_clone() { let mut daemon_set = DaemonSet::default(); let mut daemon_set_spec = DaemonSetSpec::default(); @@ -93,37 +93,31 @@ pub fn test_clone() { } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_daemon_set = - deps_hack::k8s_openapi::api::apps::v1::DaemonSet { - metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - name: Some("name".to_string()), + let kube_daemon_set = deps_hack::k8s_openapi::api::apps::v1::DaemonSet { + metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), + ..Default::default() + }, + spec: Some(deps_hack::k8s_openapi::api::apps::v1::DaemonSetSpec { + selector: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::LabelSelector { + match_labels: Some( + vec![("key".to_string(), "value".to_string())] + .into_iter() + .collect(), + ), ..Default::default() }, - spec: Some(deps_hack::k8s_openapi::api::apps::v1::DaemonSetSpec { - selector: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::LabelSelector { - match_labels: Some( - vec![("key".to_string(), "value".to_string())] - .into_iter() - .collect(), - ), - ..Default::default() - }, - ..Default::default() - }), ..Default::default() - }; + }), + ..Default::default() + }; let daemon_set = DaemonSet::from_kube(kube_daemon_set.clone()); - assert_eq!( - daemon_set.into_kube(), - kube_daemon_set - ); + assert_eq!(daemon_set.into_kube(), kube_daemon_set); } #[test] -#[verifier(external)] pub fn test_marshal() { let kube_daemon_set = deps_hack::k8s_openapi::api::apps::v1::DaemonSet { metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { @@ -146,7 +140,8 @@ pub fn test_marshal() { let daemon_set = DaemonSet::from_kube(kube_daemon_set.clone()); assert_eq!( kube_daemon_set, - DaemonSet::unmarshal(daemon_set.marshal()).unwrap().into_kube() + DaemonSet::unmarshal(daemon_set.marshal()) + .unwrap() + .into_kube() ); } -} diff --git a/src/unit_tests/kubernetes_api_objects/daemon_set_spec.rs b/src/unit_tests/kubernetes_api_objects/daemon_set_spec.rs index e3e13b7e3..af9dc480e 100644 --- a/src/unit_tests/kubernetes_api_objects/daemon_set_spec.rs +++ b/src/unit_tests/kubernetes_api_objects/daemon_set_spec.rs @@ -9,17 +9,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for daemon set spec #[test] -#[verifier(external)] pub fn test_default() { let daemon_set = DaemonSetSpec::default(); - assert_eq!(daemon_set.into_kube(), deps_hack::k8s_openapi::api::apps::v1::DaemonSetSpec::default()); + assert_eq!( + daemon_set.into_kube(), + deps_hack::k8s_openapi::api::apps::v1::DaemonSetSpec::default() + ); } #[test] -#[verifier(external)] pub fn test_set_selector() { let mut daemon_set_spec = DaemonSetSpec::default(); let mut label_selector = LabelSelector::default(); @@ -27,11 +26,13 @@ pub fn test_set_selector() { match_labels.insert("key".to_string(), "value".to_string()); label_selector.set_match_labels(match_labels.clone()); daemon_set_spec.set_selector(label_selector.clone()); - assert_eq!(label_selector.into_kube(), daemon_set_spec.into_kube().selector); + assert_eq!( + label_selector.into_kube(), + daemon_set_spec.into_kube().selector + ); } #[test] -#[verifier(external)] pub fn test_set_template() { let mut daemon_set_spec = DaemonSetSpec::default(); let mut pod_template_spec = PodTemplateSpec::default(); @@ -39,39 +40,45 @@ pub fn test_set_template() { object_meta.set_name("name".to_string()); pod_template_spec.set_metadata(object_meta.clone()); daemon_set_spec.set_template(pod_template_spec.clone()); - assert_eq!(pod_template_spec.into_kube(), daemon_set_spec.into_kube().template); + assert_eq!( + pod_template_spec.into_kube(), + daemon_set_spec.into_kube().template + ); } #[test] -#[verifier(external)] -pub fn test_selector(){ +pub fn test_selector() { let mut daemon_set_spec = DaemonSetSpec::default(); let mut label_selector = LabelSelector::default(); let temp = daemon_set_spec.selector(); - if temp.into_kube() != LabelSelector::default().into_kube() { + if temp.into_kube() != LabelSelector::default().into_kube() { panic!("selector should be default"); } let mut match_labels = StringMap::new(); match_labels.insert("key".to_string(), "value".to_string()); label_selector.set_match_labels(match_labels.clone()); daemon_set_spec.set_selector(label_selector.clone()); - assert_eq!(label_selector.into_kube(), daemon_set_spec.selector().into_kube()); + assert_eq!( + label_selector.into_kube(), + daemon_set_spec.selector().into_kube() + ); } #[test] -#[verifier(external)] -pub fn test_template(){ +pub fn test_template() { let mut daemon_set_spec = DaemonSetSpec::default(); let mut pod_template_spec = PodTemplateSpec::default(); let mut object_meta = ObjectMeta::default(); object_meta.set_name("name".to_string()); pod_template_spec.set_metadata(object_meta.clone()); daemon_set_spec.set_template(pod_template_spec.clone()); - assert_eq!(pod_template_spec.into_kube(), daemon_set_spec.template().into_kube()); + assert_eq!( + pod_template_spec.into_kube(), + daemon_set_spec.template().into_kube() + ); } #[test] -#[verifier(external)] pub fn test_clone() { let mut daemon_set_spec = DaemonSetSpec::default(); let mut pod_template_spec = PodTemplateSpec::default(); @@ -80,32 +87,37 @@ pub fn test_clone() { pod_template_spec.set_metadata(object_meta.clone()); daemon_set_spec.set_template(pod_template_spec.clone()); let daemon_set_spec_clone = daemon_set_spec.clone(); - assert_eq!(daemon_set_spec.into_kube(), daemon_set_spec_clone.into_kube()); + assert_eq!( + daemon_set_spec.into_kube(), + daemon_set_spec_clone.into_kube() + ); } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_daemon_set_spec = - deps_hack::k8s_openapi::api::apps::v1::DaemonSetSpec { - min_ready_seconds: Some(0), - revision_history_limit: Some(0), - selector: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::LabelSelector { - match_expressions: None, - match_labels: Some(vec![("key".to_string(), "value".to_string())].into_iter().collect()), - }, - template: deps_hack::k8s_openapi::api::core::v1::PodTemplateSpec { - metadata: Some(deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + let kube_daemon_set_spec = deps_hack::k8s_openapi::api::apps::v1::DaemonSetSpec { + min_ready_seconds: Some(0), + revision_history_limit: Some(0), + selector: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::LabelSelector { + match_expressions: None, + match_labels: Some( + vec![("key".to_string(), "value".to_string())] + .into_iter() + .collect(), + ), + }, + template: deps_hack::k8s_openapi::api::core::v1::PodTemplateSpec { + metadata: Some( + deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { name: Some("name".to_string()), ..Default::default() - }), - ..Default::default() - }, + }, + ), ..Default::default() - }; + }, + ..Default::default() + }; let daemon_set_spec = DaemonSetSpec::from_kube(kube_daemon_set_spec.clone()); - assert_eq!(daemon_set_spec.into_kube(), - kube_daemon_set_spec); -} + assert_eq!(daemon_set_spec.into_kube(), kube_daemon_set_spec); } diff --git a/src/unit_tests/kubernetes_api_objects/daemon_set_status.rs b/src/unit_tests/kubernetes_api_objects/daemon_set_status.rs index 0da64f2d6..2ba476537 100644 --- a/src/unit_tests/kubernetes_api_objects/daemon_set_status.rs +++ b/src/unit_tests/kubernetes_api_objects/daemon_set_status.rs @@ -9,39 +9,25 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for daemon set status #[test] -#[verifier(external)] pub fn test_kube() { - let kube_daemon_set_status = - deps_hack::k8s_openapi::api::apps::v1::DaemonSetStatus { - current_number_scheduled: 1, - number_misscheduled: 2, - desired_number_scheduled: 3, - number_ready: 4, - ..Default::default() - }; + let kube_daemon_set_status = deps_hack::k8s_openapi::api::apps::v1::DaemonSetStatus { + current_number_scheduled: 1, + number_misscheduled: 2, + desired_number_scheduled: 3, + number_ready: 4, + ..Default::default() + }; let daemon_set_status = DaemonSetStatus::from_kube(kube_daemon_set_status.clone()); - assert_eq!( - daemon_set_status.into_kube(), - kube_daemon_set_status - ); + assert_eq!(daemon_set_status.into_kube(), kube_daemon_set_status); } #[test] -#[verifier(external)] pub fn test_number_ready() { - let daemon_set_status = DaemonSetStatus::from_kube( - deps_hack::k8s_openapi::api::apps::v1::DaemonSetStatus { + let daemon_set_status = + DaemonSetStatus::from_kube(deps_hack::k8s_openapi::api::apps::v1::DaemonSetStatus { number_ready: 1, ..Default::default() - }, - ); - assert_eq!( - 1, - daemon_set_status.into_kube().number_ready - ); -} - + }); + assert_eq!(1, daemon_set_status.into_kube().number_ready); } diff --git a/src/unit_tests/kubernetes_api_objects/downward_api_volume_file.rs b/src/unit_tests/kubernetes_api_objects/downward_api_volume_file.rs index d5093fc5c..b58d5ac34 100644 --- a/src/unit_tests/kubernetes_api_objects/downward_api_volume_file.rs +++ b/src/unit_tests/kubernetes_api_objects/downward_api_volume_file.rs @@ -9,17 +9,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for downwardAPI volume file #[test] -#[verifier(external)] pub fn test_default() { let downward_api_volume_file = DownwardAPIVolumeFile::default(); - assert_eq!(downward_api_volume_file.into_kube(), deps_hack::k8s_openapi::api::core::v1::DownwardAPIVolumeFile::default()); + assert_eq!( + downward_api_volume_file.into_kube(), + deps_hack::k8s_openapi::api::core::v1::DownwardAPIVolumeFile::default() + ); } #[test] -#[verifier(external)] pub fn test_set_field_ref() { let mut downward_api_volume_file = DownwardAPIVolumeFile::default(); let mut object_field_selector = ObjectFieldSelector::default(); @@ -32,29 +31,33 @@ pub fn test_set_field_ref() { } #[test] -#[verifier(external)] pub fn test_set_path() { let mut downward_api_volume_file = DownwardAPIVolumeFile::default(); downward_api_volume_file.set_path("path".to_string()); - assert_eq!("path".to_string(), downward_api_volume_file.into_kube().path); + assert_eq!( + "path".to_string(), + downward_api_volume_file.into_kube().path + ); } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_downward_api_volume_file = deps_hack::k8s_openapi::api::core::v1::DownwardAPIVolumeFile{ - field_ref: Some(deps_hack::k8s_openapi::api::core::v1::ObjectFieldSelector{ - api_version: None, - field_path: "field_path".to_string(), - }), - mode: None, - path: "path".to_string(), - resource_field_ref: None, - }; + let kube_downward_api_volume_file = + deps_hack::k8s_openapi::api::core::v1::DownwardAPIVolumeFile { + field_ref: Some(deps_hack::k8s_openapi::api::core::v1::ObjectFieldSelector { + api_version: None, + field_path: "field_path".to_string(), + }), + mode: None, + path: "path".to_string(), + resource_field_ref: None, + }; - let downward_api_volume_file = DownwardAPIVolumeFile::from_kube(kube_downward_api_volume_file.clone()); + let downward_api_volume_file = + DownwardAPIVolumeFile::from_kube(kube_downward_api_volume_file.clone()); - assert_eq!(downward_api_volume_file.into_kube(), - kube_downward_api_volume_file); -} + assert_eq!( + downward_api_volume_file.into_kube(), + kube_downward_api_volume_file + ); } diff --git a/src/unit_tests/kubernetes_api_objects/downward_api_volume_source.rs b/src/unit_tests/kubernetes_api_objects/downward_api_volume_source.rs index 2e6c38c3d..d9e072809 100644 --- a/src/unit_tests/kubernetes_api_objects/downward_api_volume_source.rs +++ b/src/unit_tests/kubernetes_api_objects/downward_api_volume_source.rs @@ -9,17 +9,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for downwardAPI volume source #[test] -#[verifier(external)] pub fn test_default() { let downward_api_volume_source = DownwardAPIVolumeSource::default(); - assert_eq!(downward_api_volume_source.into_kube(), deps_hack::k8s_openapi::api::core::v1::DownwardAPIVolumeSource::default()); + assert_eq!( + downward_api_volume_source.into_kube(), + deps_hack::k8s_openapi::api::core::v1::DownwardAPIVolumeSource::default() + ); } #[test] -#[verifier(external)] pub fn test_set_items() { let mut downward_api_volume_source = DownwardAPIVolumeSource::default(); let downward_api_volume_file_gen = || { @@ -43,8 +42,7 @@ pub fn test_set_items() { } #[test] -#[verifier(external)] -pub fn test_clone(){ +pub fn test_clone() { let mut downward_api_volume_source = DownwardAPIVolumeSource::default(); let downward_api_volume_file_gen = || { let mut downward_api_volume_file_1 = DownwardAPIVolumeFile::default(); @@ -58,27 +56,34 @@ pub fn test_clone(){ }; downward_api_volume_source.set_items(downward_api_volume_file_gen()); let downward_api_volume_source_clone = downward_api_volume_source.clone(); - assert_eq!(downward_api_volume_source.into_kube(), downward_api_volume_source_clone.into_kube()); + assert_eq!( + downward_api_volume_source.into_kube(), + downward_api_volume_source_clone.into_kube() + ); } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_downward_api_volume_source = deps_hack::k8s_openapi::api::core::v1::DownwardAPIVolumeSource{ - default_mode: None, - items: Some(vec![deps_hack::k8s_openapi::api::core::v1::DownwardAPIVolumeFile{ - field_ref: Some(deps_hack::k8s_openapi::api::core::v1::ObjectFieldSelector{ - api_version: None, - field_path: "field_path".to_string(), - }), - mode: None, - path: "path".to_string(), - resource_field_ref: None, - }]), - }; + let kube_downward_api_volume_source = + deps_hack::k8s_openapi::api::core::v1::DownwardAPIVolumeSource { + default_mode: None, + items: Some(vec![ + deps_hack::k8s_openapi::api::core::v1::DownwardAPIVolumeFile { + field_ref: Some(deps_hack::k8s_openapi::api::core::v1::ObjectFieldSelector { + api_version: None, + field_path: "field_path".to_string(), + }), + mode: None, + path: "path".to_string(), + resource_field_ref: None, + }, + ]), + }; - let downward_api_volume_source = DownwardAPIVolumeSource::from_kube(kube_downward_api_volume_source.clone()); - assert_eq!(downward_api_volume_source.into_kube(), - kube_downward_api_volume_source); -} + let downward_api_volume_source = + DownwardAPIVolumeSource::from_kube(kube_downward_api_volume_source.clone()); + assert_eq!( + downward_api_volume_source.into_kube(), + kube_downward_api_volume_source + ); } diff --git a/src/unit_tests/kubernetes_api_objects/dynamic_object.rs b/src/unit_tests/kubernetes_api_objects/dynamic_object.rs index 2375c2572..851c8eb02 100644 --- a/src/unit_tests/kubernetes_api_objects/dynamic_object.rs +++ b/src/unit_tests/kubernetes_api_objects/dynamic_object.rs @@ -9,52 +9,42 @@ use deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::Time; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for dynamic object #[test] -#[verifier(external)] pub fn test_kube() { - let kube_dynamic_object = - deps_hack::kube::api::DynamicObject { - metadata: deps_hack::kube::api::ObjectMeta { - name: Some("name".to_string()), - namespace: Some("namespace".to_string()), - ..Default::default() - }, - types: Some(deps_hack::kube::api::TypeMeta { - api_version: "api_version".to_string(), - kind: "kind".to_string(), - }), - data: deps_hack::serde_json::json!({ - "key": "value", - }), - }; + let kube_dynamic_object = deps_hack::kube::api::DynamicObject { + metadata: deps_hack::kube::api::ObjectMeta { + name: Some("name".to_string()), + namespace: Some("namespace".to_string()), + ..Default::default() + }, + types: Some(deps_hack::kube::api::TypeMeta { + api_version: "api_version".to_string(), + kind: "kind".to_string(), + }), + data: deps_hack::serde_json::json!({ + "key": "value", + }), + }; let dynamic_object = DynamicObject::from_kube(kube_dynamic_object.clone()); - assert_eq!( - dynamic_object.into_kube(), - kube_dynamic_object - ); + assert_eq!(dynamic_object.into_kube(), kube_dynamic_object); } #[test] -#[verifier(external)] pub fn test_kube_metadata_ref() { - let dynamic_object = DynamicObject::from_kube( - deps_hack::kube::api::DynamicObject { - metadata: deps_hack::kube::api::ObjectMeta { - name: Some("name".to_string()), - namespace: Some("namespace".to_string()), - ..Default::default() - }, - types: Some(deps_hack::kube::api::TypeMeta { - api_version: "api_version".to_string(), - kind: "kind".to_string(), - }), - data: deps_hack::serde_json::json!({ - "key": "value", - }), + let dynamic_object = DynamicObject::from_kube(deps_hack::kube::api::DynamicObject { + metadata: deps_hack::kube::api::ObjectMeta { + name: Some("name".to_string()), + namespace: Some("namespace".to_string()), + ..Default::default() }, - ); + types: Some(deps_hack::kube::api::TypeMeta { + api_version: "api_version".to_string(), + kind: "kind".to_string(), + }), + data: deps_hack::serde_json::json!({ + "key": "value", + }), + }); assert_eq!( dynamic_object.kube_metadata_ref(), &deps_hack::kube::api::ObjectMeta { @@ -66,24 +56,21 @@ pub fn test_kube_metadata_ref() { } #[test] -#[verifier(external)] pub fn test_metadata() { - let dynamic_object = DynamicObject::from_kube( - deps_hack::kube::api::DynamicObject { - metadata: deps_hack::kube::api::ObjectMeta { - name: Some("name".to_string()), - namespace: Some("namespace".to_string()), - ..Default::default() - }, - types: Some(deps_hack::kube::api::TypeMeta { - api_version: "api_version".to_string(), - kind: "kind".to_string(), - }), - data: deps_hack::serde_json::json!({ - "key": "value", - }), + let dynamic_object = DynamicObject::from_kube(deps_hack::kube::api::DynamicObject { + metadata: deps_hack::kube::api::ObjectMeta { + name: Some("name".to_string()), + namespace: Some("namespace".to_string()), + ..Default::default() }, - ); + types: Some(deps_hack::kube::api::TypeMeta { + api_version: "api_version".to_string(), + kind: "kind".to_string(), + }), + data: deps_hack::serde_json::json!({ + "key": "value", + }), + }); assert_eq!( dynamic_object.metadata().into_kube(), deps_hack::kube::api::ObjectMeta { @@ -95,24 +82,21 @@ pub fn test_metadata() { } #[test] -#[verifier(external)] pub fn test_clone() { - let dynamic_object = DynamicObject::from_kube( - deps_hack::kube::api::DynamicObject { - metadata: deps_hack::kube::api::ObjectMeta { - name: Some("name".to_string()), - namespace: Some("namespace".to_string()), - ..Default::default() - }, - types: Some(deps_hack::kube::api::TypeMeta { - api_version: "api_version".to_string(), - kind: "kind".to_string(), - }), - data: deps_hack::serde_json::json!({ - "key": "value", - }), + let dynamic_object = DynamicObject::from_kube(deps_hack::kube::api::DynamicObject { + metadata: deps_hack::kube::api::ObjectMeta { + name: Some("name".to_string()), + namespace: Some("namespace".to_string()), + ..Default::default() }, - ); + types: Some(deps_hack::kube::api::TypeMeta { + api_version: "api_version".to_string(), + kind: "kind".to_string(), + }), + data: deps_hack::serde_json::json!({ + "key": "value", + }), + }); let cloned_dynamic_object = dynamic_object.clone(); @@ -123,28 +107,23 @@ pub fn test_clone() { } #[test] -#[verifier(external)] pub fn test_fmt() { - let dynamic_object = DynamicObject::from_kube( - deps_hack::kube::api::DynamicObject { - metadata: deps_hack::kube::api::ObjectMeta { - name: Some("name".to_string()), - namespace: Some("namespace".to_string()), - ..Default::default() - }, - types: Some(deps_hack::kube::api::TypeMeta { - api_version: "api_version".to_string(), - kind: "kind".to_string(), - }), - data: deps_hack::serde_json::json!({ - "key": "value", - }), + let dynamic_object = DynamicObject::from_kube(deps_hack::kube::api::DynamicObject { + metadata: deps_hack::kube::api::ObjectMeta { + name: Some("name".to_string()), + namespace: Some("namespace".to_string()), + ..Default::default() }, - ); + types: Some(deps_hack::kube::api::TypeMeta { + api_version: "api_version".to_string(), + kind: "kind".to_string(), + }), + data: deps_hack::serde_json::json!({ + "key": "value", + }), + }); assert_eq!( format!("{:?}", dynamic_object), format!("{:?}", dynamic_object.into_kube()) ); } - -} diff --git a/src/unit_tests/kubernetes_api_objects/empty_dir_volume_source.rs b/src/unit_tests/kubernetes_api_objects/empty_dir_volume_source.rs index 81401d6a8..3cf7ae5a6 100644 --- a/src/unit_tests/kubernetes_api_objects/empty_dir_volume_source.rs +++ b/src/unit_tests/kubernetes_api_objects/empty_dir_volume_source.rs @@ -9,33 +9,37 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for EmptyDirVolumeSource #[test] -#[verifier(external)] pub fn test_default() { let empty_dir_volume_source = EmptyDirVolumeSource::default(); - assert_eq!(empty_dir_volume_source.into_kube(), deps_hack::k8s_openapi::api::core::v1::EmptyDirVolumeSource::default()); + assert_eq!( + empty_dir_volume_source.into_kube(), + deps_hack::k8s_openapi::api::core::v1::EmptyDirVolumeSource::default() + ); } #[test] -#[verifier(external)] pub fn test_clone() { let empty_dir_volume_source = EmptyDirVolumeSource::default(); let empty_dir_volume_source_clone = empty_dir_volume_source.clone(); - assert_eq!(empty_dir_volume_source.into_kube(), empty_dir_volume_source_clone.into_kube()); + assert_eq!( + empty_dir_volume_source.into_kube(), + empty_dir_volume_source_clone.into_kube() + ); } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_empty_dir_volume_source = deps_hack::k8s_openapi::api::core::v1::EmptyDirVolumeSource{ - ..Default::default() - }; + let kube_empty_dir_volume_source = + deps_hack::k8s_openapi::api::core::v1::EmptyDirVolumeSource { + ..Default::default() + }; - let empty_dir_volume_source = EmptyDirVolumeSource::from_kube(kube_empty_dir_volume_source.clone()); + let empty_dir_volume_source = + EmptyDirVolumeSource::from_kube(kube_empty_dir_volume_source.clone()); - assert_eq!(empty_dir_volume_source.into_kube(), - kube_empty_dir_volume_source); -} + assert_eq!( + empty_dir_volume_source.into_kube(), + kube_empty_dir_volume_source + ); } diff --git a/src/unit_tests/kubernetes_api_objects/env_var.rs b/src/unit_tests/kubernetes_api_objects/env_var.rs index 69d7840cb..3d4ff646f 100644 --- a/src/unit_tests/kubernetes_api_objects/env_var.rs +++ b/src/unit_tests/kubernetes_api_objects/env_var.rs @@ -8,18 +8,17 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for env var #[test] -#[verifier(external)] -pub fn test_default(){ +pub fn test_default() { let env = EnvVar::default(); - assert_eq!(env.into_kube(), deps_hack::k8s_openapi::api::core::v1::EnvVar::default()); + assert_eq!( + env.into_kube(), + deps_hack::k8s_openapi::api::core::v1::EnvVar::default() + ); } #[test] -#[verifier(external)] -pub fn test_clone(){ +pub fn test_clone() { let mut env = EnvVar::default(); env.set_name("name".to_string()); env.set_value("value".to_string()); @@ -28,36 +27,35 @@ pub fn test_clone(){ } #[test] -#[verifier(external)] -pub fn test_set_name(){ +pub fn test_set_name() { let mut env_var = EnvVar::default(); env_var.set_name("name".to_string()); assert_eq!("name".to_string(), env_var.into_kube().name); } #[test] -#[verifier(external)] -pub fn test_set_value(){ +pub fn test_set_value() { let mut env_var = EnvVar::default(); env_var.set_value("value".to_string()); assert_eq!("value".to_string(), env_var.into_kube().value.unwrap()); } #[test] -#[verifier(external)] -pub fn test_set_value_from(){ +pub fn test_set_value_from() { let mut env_var = EnvVar::default(); let mut env_var_source = EnvVarSource::default(); let mut object_field_selector = ObjectFieldSelector::default(); object_field_selector.set_field_path("field_path".to_string()); env_var_source.set_field_ref(object_field_selector); env_var.set_value_from(env_var_source.clone()); - assert_eq!(env_var_source.into_kube(), env_var.into_kube().value_from.unwrap()); + assert_eq!( + env_var_source.into_kube(), + env_var.into_kube().value_from.unwrap() + ); } #[test] -#[verifier(external)] -pub fn test_kube(){ +pub fn test_kube() { let kube_env_var = deps_hack::k8s_openapi::api::core::v1::EnvVar { name: "name".to_string(), value: Some("value".to_string()), @@ -75,4 +73,3 @@ pub fn test_kube(){ assert_eq!(env_var.into_kube(), kube_env_var); } -} diff --git a/src/unit_tests/kubernetes_api_objects/env_var_source.rs b/src/unit_tests/kubernetes_api_objects/env_var_source.rs index 0419efd06..d99da9d13 100644 --- a/src/unit_tests/kubernetes_api_objects/env_var_source.rs +++ b/src/unit_tests/kubernetes_api_objects/env_var_source.rs @@ -8,10 +8,7 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for EnvVarSource #[test] -#[verifier(external)] pub fn test_set_field_ref() { let mut env_var_source = EnvVarSource::default(); let mut object_field_selector = ObjectFieldSelector::default(); @@ -19,19 +16,23 @@ pub fn test_set_field_ref() { let mut object_field_selector_2 = ObjectFieldSelector::default(); object_field_selector_2.set_field_path("field_path".to_string()); env_var_source.set_field_ref(object_field_selector); - assert_eq!(object_field_selector_2.into_kube(), env_var_source.into_kube().field_ref.unwrap()); + assert_eq!( + object_field_selector_2.into_kube(), + env_var_source.into_kube().field_ref.unwrap() + ); } #[test] -#[verifier(external)] -pub fn test_default(){ +pub fn test_default() { let env_var_source = EnvVarSource::default(); - assert_eq!(env_var_source.into_kube(), deps_hack::k8s_openapi::api::core::v1::EnvVarSource::default()); + assert_eq!( + env_var_source.into_kube(), + deps_hack::k8s_openapi::api::core::v1::EnvVarSource::default() + ); } #[test] -#[verifier(external)] -pub fn test_clone(){ +pub fn test_clone() { let mut env_var_source = EnvVarSource::default(); let mut object_field_selector = ObjectFieldSelector::default(); object_field_selector.set_field_path("field_path".to_string()); @@ -41,8 +42,7 @@ pub fn test_clone(){ } #[test] -#[verifier(external)] -pub fn test_kube(){ +pub fn test_kube() { let kube_env_var_source = deps_hack::k8s_openapi::api::core::v1::EnvVarSource { field_ref: Some(deps_hack::k8s_openapi::api::core::v1::ObjectFieldSelector { field_path: "field_path".to_string(), @@ -55,4 +55,3 @@ pub fn test_kube(){ assert_eq!(env_var_source.into_kube(), kube_env_var_source); } -} diff --git a/src/unit_tests/kubernetes_api_objects/error.rs b/src/unit_tests/kubernetes_api_objects/error.rs index f70d4b1f6..65f90c334 100644 --- a/src/unit_tests/kubernetes_api_objects/error.rs +++ b/src/unit_tests/kubernetes_api_objects/error.rs @@ -10,90 +10,40 @@ use deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::Time; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for error #[test] -#[verifier(external)] pub fn test_apierror_fmt() { let error = APIError::BadRequest; - assert_eq!( - format!("{:?}", error), - "BadRequest" - ); + assert_eq!(format!("{:?}", error), "BadRequest"); let error = APIError::Conflict; - assert_eq!( - format!("{:?}", error), - "Conflict" - ); + assert_eq!(format!("{:?}", error), "Conflict"); let error = APIError::Forbidden; - assert_eq!( - format!("{:?}", error), - "Forbidden" - ); + assert_eq!(format!("{:?}", error), "Forbidden"); let error = APIError::Invalid; - assert_eq!( - format!("{:?}", error), - "Invalid" - ); + assert_eq!(format!("{:?}", error), "Invalid"); let error = APIError::ObjectNotFound; - assert_eq!( - format!("{:?}", error), - "ObjectNotFound" - ); + assert_eq!(format!("{:?}", error), "ObjectNotFound"); let error = APIError::ObjectAlreadyExists; - assert_eq!( - format!("{:?}", error), - "ObjectAlreadyExists" - ); + assert_eq!(format!("{:?}", error), "ObjectAlreadyExists"); let error = APIError::NotSupported; - assert_eq!( - format!("{:?}", error), - "NotSupported" - ); + assert_eq!(format!("{:?}", error), "NotSupported"); let error = APIError::InternalError; - assert_eq!( - format!("{:?}", error), - "InternalError" - ); + assert_eq!(format!("{:?}", error), "InternalError"); let error = APIError::Timeout; - assert_eq!( - format!("{:?}", error), - "Timeout" - ); + assert_eq!(format!("{:?}", error), "Timeout"); let error = APIError::ServerTimeout; - assert_eq!( - format!("{:?}", error), - "ServerTimeout" - ); + assert_eq!(format!("{:?}", error), "ServerTimeout"); let error = APIError::Other; - assert_eq!( - format!("{:?}", error), - "Other" - ); + assert_eq!(format!("{:?}", error), "Other"); } #[test] -#[verifier(external)] pub fn test_parse_dyn_error_fmt() { let error = ParseDynamicObjectError::MissingField; - assert_eq!( - format!("{:?}", error), - "MissingField" - ); + assert_eq!(format!("{:?}", error), "MissingField"); let error = ParseDynamicObjectError::UnexpectedType; - assert_eq!( - format!("{:?}", error), - "UnexpectedType" - ); + assert_eq!(format!("{:?}", error), "UnexpectedType"); let error = ParseDynamicObjectError::UnmarshalError; - assert_eq!( - format!("{:?}", error), - "UnmarshalError" - ); + assert_eq!(format!("{:?}", error), "UnmarshalError"); let error = ParseDynamicObjectError::ExecError; - assert_eq!( - format!("{:?}", error), - "ExecError" - ); -} + assert_eq!(format!("{:?}", error), "ExecError"); } diff --git a/src/unit_tests/kubernetes_api_objects/exec_action.rs b/src/unit_tests/kubernetes_api_objects/exec_action.rs index 23dd4a899..b76c473bc 100644 --- a/src/unit_tests/kubernetes_api_objects/exec_action.rs +++ b/src/unit_tests/kubernetes_api_objects/exec_action.rs @@ -7,10 +7,7 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for life cycle #[test] -#[verifier(external)] pub fn test_set_command() { let mut exec_action = ExecAction::default(); exec_action.set_command(vec!["command".to_string()]); @@ -21,7 +18,6 @@ pub fn test_set_command() { } #[test] -#[verifier(external)] pub fn test_default() { let exec_action = ExecAction::default(); assert_eq!( @@ -31,7 +27,6 @@ pub fn test_default() { } #[test] -#[verifier(external)] pub fn test_clone() { let mut exec_action = ExecAction::default(); exec_action.set_command(vec!["command".to_string()]); @@ -40,7 +35,6 @@ pub fn test_clone() { } #[test] -#[verifier(external)] pub fn test_kube() { let kube_exec_action = deps_hack::k8s_openapi::api::core::v1::ExecAction { command: Some(vec!["command".to_string()]), @@ -48,10 +42,5 @@ pub fn test_kube() { let exec_action = ExecAction::from_kube(kube_exec_action.clone()); - assert_eq!( - exec_action.into_kube(), - kube_exec_action - ); -} - + assert_eq!(exec_action.into_kube(), kube_exec_action); } diff --git a/src/unit_tests/kubernetes_api_objects/host_path_volume_source.rs b/src/unit_tests/kubernetes_api_objects/host_path_volume_source.rs index 4cf3001a2..2290aec89 100644 --- a/src/unit_tests/kubernetes_api_objects/host_path_volume_source.rs +++ b/src/unit_tests/kubernetes_api_objects/host_path_volume_source.rs @@ -9,17 +9,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for host path volume source #[test] -#[verifier(external)] pub fn test_default() { let host_path_volume_source = HostPathVolumeSource::default(); - assert_eq!(host_path_volume_source.into_kube(), deps_hack::k8s_openapi::api::core::v1::HostPathVolumeSource::default()); + assert_eq!( + host_path_volume_source.into_kube(), + deps_hack::k8s_openapi::api::core::v1::HostPathVolumeSource::default() + ); } #[test] -#[verifier(external)] pub fn test_set_path() { let mut host_path_volume_source = HostPathVolumeSource::default(); host_path_volume_source.set_path("path".to_string()); @@ -27,25 +26,29 @@ pub fn test_set_path() { } #[test] -#[verifier(external)] -pub fn test_clone(){ +pub fn test_clone() { let mut host_path_volume_source = HostPathVolumeSource::default(); host_path_volume_source.set_path("path".to_string()); let host_path_volume_source_clone = host_path_volume_source.clone(); - assert_eq!(host_path_volume_source.into_kube(), host_path_volume_source_clone.into_kube()); + assert_eq!( + host_path_volume_source.into_kube(), + host_path_volume_source_clone.into_kube() + ); } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_host_path_volume_source = deps_hack::k8s_openapi::api::core::v1::HostPathVolumeSource{ - path: "path".to_string(), - ..Default::default() - }; + let kube_host_path_volume_source = + deps_hack::k8s_openapi::api::core::v1::HostPathVolumeSource { + path: "path".to_string(), + ..Default::default() + }; - let host_path_volume_source = HostPathVolumeSource::from_kube(kube_host_path_volume_source.clone()); + let host_path_volume_source = + HostPathVolumeSource::from_kube(kube_host_path_volume_source.clone()); - assert_eq!(host_path_volume_source.into_kube(), - kube_host_path_volume_source); -} + assert_eq!( + host_path_volume_source.into_kube(), + kube_host_path_volume_source + ); } diff --git a/src/unit_tests/kubernetes_api_objects/key_to_path.rs b/src/unit_tests/kubernetes_api_objects/key_to_path.rs index 23f115c63..472a19a25 100644 --- a/src/unit_tests/kubernetes_api_objects/key_to_path.rs +++ b/src/unit_tests/kubernetes_api_objects/key_to_path.rs @@ -9,17 +9,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for key to path #[test] -#[verifier(external)] pub fn test_default() { let key_to_path = KeyToPath::default(); - assert_eq!(key_to_path.into_kube(), deps_hack::k8s_openapi::api::core::v1::KeyToPath::default()); + assert_eq!( + key_to_path.into_kube(), + deps_hack::k8s_openapi::api::core::v1::KeyToPath::default() + ); } #[test] -#[verifier(external)] pub fn test_set_key() { let mut key_to_path = KeyToPath::default(); key_to_path.set_key("key".to_string()); @@ -27,7 +26,6 @@ pub fn test_set_key() { } #[test] -#[verifier(external)] pub fn test_set_path() { let mut key_to_path = KeyToPath::default(); key_to_path.set_path("path".to_string()); @@ -35,16 +33,13 @@ pub fn test_set_path() { } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_key_to_path = deps_hack::k8s_openapi::api::core::v1::KeyToPath{ + let kube_key_to_path = deps_hack::k8s_openapi::api::core::v1::KeyToPath { key: "key".to_string(), path: "path".to_string(), ..Default::default() }; let key_to_path = KeyToPath::from_kube(kube_key_to_path.clone()); - assert_eq!(key_to_path.into_kube(), - kube_key_to_path); -} + assert_eq!(key_to_path.into_kube(), kube_key_to_path); } diff --git a/src/unit_tests/kubernetes_api_objects/label_selector.rs b/src/unit_tests/kubernetes_api_objects/label_selector.rs index 786cb7179..80a69feff 100644 --- a/src/unit_tests/kubernetes_api_objects/label_selector.rs +++ b/src/unit_tests/kubernetes_api_objects/label_selector.rs @@ -7,10 +7,7 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for label selector #[test] -#[verifier(external)] pub fn test_default() { let label_selector = LabelSelector::default(); assert_eq!( @@ -20,7 +17,6 @@ pub fn test_default() { } #[test] -#[verifier(external)] pub fn test_set_match_labels() { let mut label_selector = LabelSelector::default(); let mut match_labels = StringMap::new(); @@ -34,7 +30,6 @@ pub fn test_set_match_labels() { } #[test] -#[verifier(external)] pub fn test_clone() { let mut label_selector = LabelSelector::default(); let mut match_labels = StringMap::new(); @@ -49,20 +44,13 @@ pub fn test_clone() { } #[test] -#[verifier(external)] pub fn test_kube() { let kube_label_selector = deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::LabelSelector { match_labels: Some( vec![ - ( - "key".to_string(), - "value".to_string(), - ), - ( - "key_2".to_string(), - "value_2".to_string(), - ), + ("key".to_string(), "value".to_string()), + ("key_2".to_string(), "value_2".to_string()), ] .into_iter() .collect(), @@ -72,9 +60,5 @@ pub fn test_kube() { let label_selector = LabelSelector::from_kube(kube_label_selector.clone()); - assert_eq!( - label_selector.into_kube(), - kube_label_selector - ); -} + assert_eq!(label_selector.into_kube(), kube_label_selector); } diff --git a/src/unit_tests/kubernetes_api_objects/lifecycle.rs b/src/unit_tests/kubernetes_api_objects/lifecycle.rs index 9b1162cad..38583f219 100644 --- a/src/unit_tests/kubernetes_api_objects/lifecycle.rs +++ b/src/unit_tests/kubernetes_api_objects/lifecycle.rs @@ -7,10 +7,7 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for life cycle #[test] -#[verifier(external)] pub fn test_set_pre_stop() { let mut lifecycle = Lifecycle::default(); let mut handler = LifecycleHandler::default(); @@ -19,22 +16,20 @@ pub fn test_set_pre_stop() { handler.set_exec(exec_action); lifecycle.set_pre_stop(handler.clone()); - assert_eq!( - handler.into_kube(), - lifecycle.into_kube().pre_stop.unwrap() - ); + assert_eq!(handler.into_kube(), lifecycle.into_kube().pre_stop.unwrap()); } #[test] -#[verifier(external)] -pub fn test_default(){ +pub fn test_default() { let lifecycle = Lifecycle::default(); - assert_eq!(lifecycle.into_kube(), deps_hack::k8s_openapi::api::core::v1::Lifecycle::default()); + assert_eq!( + lifecycle.into_kube(), + deps_hack::k8s_openapi::api::core::v1::Lifecycle::default() + ); } #[test] -#[verifier(external)] -pub fn test_clone(){ +pub fn test_clone() { let mut handler = LifecycleHandler::default(); let mut exec_action = ExecAction::default(); exec_action.set_command(vec!["command".to_string()]); @@ -44,8 +39,7 @@ pub fn test_clone(){ } #[test] -#[verifier(external)] -pub fn test_kube(){ +pub fn test_kube() { let kube_lifecycle = deps_hack::k8s_openapi::api::core::v1::Lifecycle { pre_stop: Some(deps_hack::k8s_openapi::api::core::v1::LifecycleHandler { exec: Some(deps_hack::k8s_openapi::api::core::v1::ExecAction { @@ -60,5 +54,3 @@ pub fn test_kube(){ assert_eq!(lifecycle.into_kube(), kube_lifecycle); } - -} diff --git a/src/unit_tests/kubernetes_api_objects/lifecycle_handler.rs b/src/unit_tests/kubernetes_api_objects/lifecycle_handler.rs index 1d2230d1e..a0ecc5f97 100644 --- a/src/unit_tests/kubernetes_api_objects/lifecycle_handler.rs +++ b/src/unit_tests/kubernetes_api_objects/lifecycle_handler.rs @@ -7,10 +7,7 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for life cycle handler #[test] -#[verifier(external)] pub fn test_set_exec() { let mut handler = LifecycleHandler::default(); let mut exec_action = ExecAction::default(); @@ -20,15 +17,16 @@ pub fn test_set_exec() { } #[test] -#[verifier(external)] -pub fn test_default(){ +pub fn test_default() { let handler = LifecycleHandler::default(); - assert_eq!(handler.into_kube(), deps_hack::k8s_openapi::api::core::v1::LifecycleHandler::default()); + assert_eq!( + handler.into_kube(), + deps_hack::k8s_openapi::api::core::v1::LifecycleHandler::default() + ); } #[test] -#[verifier(external)] -pub fn test_clone(){ +pub fn test_clone() { let mut handler = LifecycleHandler::default(); let mut exec_action = ExecAction::default(); exec_action.set_command(vec!["command".to_string()]); @@ -38,8 +36,7 @@ pub fn test_clone(){ } #[test] -#[verifier(external)] -pub fn test_kube(){ +pub fn test_kube() { let kube_handler = deps_hack::k8s_openapi::api::core::v1::LifecycleHandler { exec: Some(deps_hack::k8s_openapi::api::core::v1::ExecAction { command: Some(vec!["command".to_string()]), @@ -51,5 +48,3 @@ pub fn test_kube(){ assert_eq!(handler.into_kube(), kube_handler); } - -} diff --git a/src/unit_tests/kubernetes_api_objects/local_object_reference.rs b/src/unit_tests/kubernetes_api_objects/local_object_reference.rs index 09da09d4f..069344537 100644 --- a/src/unit_tests/kubernetes_api_objects/local_object_reference.rs +++ b/src/unit_tests/kubernetes_api_objects/local_object_reference.rs @@ -11,18 +11,17 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for LocalObjectReference #[test] -#[verifier(external)] pub fn test_kube() { let kube_local_object_reference = deps_hack::k8s_openapi::api::core::v1::LocalObjectReference { name: Some("name".to_string()), }; - let local_object_reference = LocalObjectReference::from_kube(kube_local_object_reference.clone()); + let local_object_reference = + LocalObjectReference::from_kube(kube_local_object_reference.clone()); - assert_eq!(local_object_reference.into_kube(), - kube_local_object_reference); -} + assert_eq!( + local_object_reference.into_kube(), + kube_local_object_reference + ); } diff --git a/src/unit_tests/kubernetes_api_objects/object_field_selector.rs b/src/unit_tests/kubernetes_api_objects/object_field_selector.rs index 20947dc63..bc1869376 100644 --- a/src/unit_tests/kubernetes_api_objects/object_field_selector.rs +++ b/src/unit_tests/kubernetes_api_objects/object_field_selector.rs @@ -7,53 +7,58 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for ObjectFieldSelector #[test] -#[verifier(external)] pub fn test_set_field_path() { let mut object_field_selector = ObjectFieldSelector::default(); object_field_selector.set_field_path("field_path".to_string()); - assert_eq!("field_path".to_string(), object_field_selector.into_kube().field_path); + assert_eq!( + "field_path".to_string(), + object_field_selector.into_kube().field_path + ); } #[test] -#[verifier(external)] pub fn test_set_api_version() { let mut object_field_selector = ObjectFieldSelector::default(); object_field_selector.set_api_version("api_version".to_string()); - assert_eq!("api_version".to_string(), object_field_selector.into_kube().api_version.unwrap()); + assert_eq!( + "api_version".to_string(), + object_field_selector.into_kube().api_version.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_default() { let object_field_selector = ObjectFieldSelector::default(); - assert_eq!(object_field_selector.into_kube(), deps_hack::k8s_openapi::api::core::v1::ObjectFieldSelector::default()); + assert_eq!( + object_field_selector.into_kube(), + deps_hack::k8s_openapi::api::core::v1::ObjectFieldSelector::default() + ); } #[test] -#[verifier(external)] pub fn test_clone() { let mut object_field_selector = ObjectFieldSelector::default(); object_field_selector.set_field_path("field_path".to_string()); object_field_selector.set_api_version("api_version".to_string()); let object_field_selector_clone = object_field_selector.clone(); - assert_eq!(object_field_selector.into_kube(), object_field_selector_clone.into_kube()); + assert_eq!( + object_field_selector.into_kube(), + object_field_selector_clone.into_kube() + ); } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_object_field_selector = deps_hack::k8s_openapi::api::core::v1::ObjectFieldSelector{ + let kube_object_field_selector = deps_hack::k8s_openapi::api::core::v1::ObjectFieldSelector { api_version: Some("api_version".to_string()), field_path: "field_path".to_string(), }; let object_field_selector = ObjectFieldSelector::from_kube(kube_object_field_selector.clone()); - assert_eq!(object_field_selector.into_kube(), - kube_object_field_selector); -} - + assert_eq!( + object_field_selector.into_kube(), + kube_object_field_selector + ); } diff --git a/src/unit_tests/kubernetes_api_objects/object_meta.rs b/src/unit_tests/kubernetes_api_objects/object_meta.rs index 1221bf2bf..dd9cf508e 100644 --- a/src/unit_tests/kubernetes_api_objects/object_meta.rs +++ b/src/unit_tests/kubernetes_api_objects/object_meta.rs @@ -9,9 +9,7 @@ use deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::Time; use vstd::prelude::*; use vstd::string::*; -verus! { #[test] -#[verifier(external)] pub fn test_default() { let object_meta = ObjectMeta::default(); assert_eq!( @@ -21,7 +19,6 @@ pub fn test_default() { } #[test] -#[verifier(external)] pub fn test_set_name() { let mut object_meta = ObjectMeta::default(); object_meta.set_name("name".to_string()); @@ -29,7 +26,6 @@ pub fn test_set_name() { } #[test] -#[verifier(external)] pub fn test_name() { let mut object_meta = ObjectMeta::default(); object_meta.set_name("name".to_string()); @@ -37,15 +33,16 @@ pub fn test_name() { } #[test] -#[verifier(external)] pub fn test_set_namespace() { let mut object_meta = ObjectMeta::default(); object_meta.set_namespace("namespace".to_string()); - assert_eq!("namespace".to_string(), object_meta.into_kube().namespace.unwrap()); + assert_eq!( + "namespace".to_string(), + object_meta.into_kube().namespace.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_namespace() { let mut object_meta = ObjectMeta::default(); object_meta.set_namespace("namespace".to_string()); @@ -53,17 +50,18 @@ pub fn test_namespace() { } #[test] -#[verifier(external)] pub fn test_set_labels() { let mut object_meta = ObjectMeta::default(); let mut labels = StringMap::new(); labels.insert("key".to_string(), "value".to_string()); object_meta.set_labels(labels.clone()); - assert_eq!(labels.into_rust_map(), object_meta.into_kube().labels.unwrap()); + assert_eq!( + labels.into_rust_map(), + object_meta.into_kube().labels.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_labels() { let mut object_meta = ObjectMeta::default(); let temp = object_meta.labels(); @@ -73,64 +71,83 @@ pub fn test_labels() { let mut labels = StringMap::new(); labels.insert("key".to_string(), "value".to_string()); object_meta.set_labels(labels.clone()); - assert_eq!(labels.into_rust_map(), object_meta.labels().unwrap().into_rust_map()); + assert_eq!( + labels.into_rust_map(), + object_meta.labels().unwrap().into_rust_map() + ); } #[test] -#[verifier(external)] pub fn test_owner_references_only_contains() { let mut object_meta = ObjectMeta::default(); - assert_eq!(false, object_meta.owner_references_only_contains(OwnerReference::from_kube(deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::OwnerReference::default()))); + assert_eq!( + false, + object_meta.owner_references_only_contains(OwnerReference::from_kube( + deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::OwnerReference::default() + )) + ); let own_refs_gen = || { - let own_ref = deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::OwnerReference::default(); + let own_ref = + deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::OwnerReference::default(); let mut owner_references = Vec::new(); owner_references.push(OwnerReference::from_kube(own_ref.clone())); owner_references }; object_meta.set_owner_references(own_refs_gen()); - assert_eq!(true, object_meta.owner_references_only_contains(OwnerReference::from_kube(deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::OwnerReference::default()))); + assert_eq!( + true, + object_meta.owner_references_only_contains(OwnerReference::from_kube( + deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::OwnerReference::default() + )) + ); } #[test] -#[verifier(external)] pub fn test_resource_version() { let object_meta = ObjectMeta::default(); let temp = object_meta.resource_version(); if !temp.is_none() { panic!("Expected None") } - let object_meta = ObjectMeta::from_kube(deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - resource_version: Some("resource_version".to_string()), - ..Default::default() - }); - assert_eq!("resource_version".to_string(), object_meta.resource_version().unwrap()); + let object_meta = ObjectMeta::from_kube( + deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + resource_version: Some("resource_version".to_string()), + ..Default::default() + }, + ); + assert_eq!( + "resource_version".to_string(), + object_meta.resource_version().unwrap() + ); } #[test] -#[verifier(external)] pub fn test_has_deletion_timestamp() { let object_meta = ObjectMeta::default(); let time = Time(Utc::now()); assert_eq!(false, object_meta.has_deletion_timestamp()); - let object_meta = ObjectMeta::from_kube(deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - deletion_timestamp: Some(time), - ..Default::default() - }); + let object_meta = ObjectMeta::from_kube( + deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + deletion_timestamp: Some(time), + ..Default::default() + }, + ); assert_eq!(true, object_meta.has_deletion_timestamp()); } #[test] -#[verifier(external)] pub fn test_set_annotations() { let mut object_meta = ObjectMeta::default(); let mut annotations = StringMap::new(); annotations.insert("key".to_string(), "value".to_string()); object_meta.set_annotations(annotations.clone()); - assert_eq!(annotations.into_rust_map(), object_meta.into_kube().annotations.unwrap()); + assert_eq!( + annotations.into_rust_map(), + object_meta.into_kube().annotations.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_add_annotation() { let mut object_meta = ObjectMeta::default(); let mut annotations = StringMap::new(); @@ -138,11 +155,13 @@ pub fn test_add_annotation() { let key = "key".to_string(); let value = "value".to_string(); object_meta.add_annotation(key, value); - assert_eq!(annotations.into_rust_map(), object_meta.into_kube().annotations.unwrap()); + assert_eq!( + annotations.into_rust_map(), + object_meta.into_kube().annotations.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_annotations() { let mut object_meta = ObjectMeta::default(); let temp = object_meta.annotations(); @@ -152,11 +171,13 @@ pub fn test_annotations() { let mut annotations = StringMap::new(); annotations.insert("key".to_string(), "value".to_string()); object_meta.set_annotations(annotations.clone()); - assert_eq!(annotations.into_rust_map(), object_meta.annotations().unwrap().into_rust_map()); + assert_eq!( + annotations.into_rust_map(), + object_meta.annotations().unwrap().into_rust_map() + ); } #[test] -#[verifier(external)] pub fn test_set_finalizers() { let mut object_meta = ObjectMeta::default(); // We use a closure to generate the Vec @@ -167,11 +188,13 @@ pub fn test_set_finalizers() { finalizers }; object_meta.set_finalizers(finalizers_gen()); - assert_eq!(finalizers_gen(), object_meta.into_kube().finalizers.unwrap()); + assert_eq!( + finalizers_gen(), + object_meta.into_kube().finalizers.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_unset_finalizers() { let mut object_meta = ObjectMeta::default(); // We use a closure to generate the Vec @@ -187,77 +210,57 @@ pub fn test_unset_finalizers() { } #[test] -#[verifier(external)] -pub fn test_clone(){ +pub fn test_clone() { let mut object_meta = ObjectMeta::default(); object_meta.set_name("name".to_string()); object_meta.set_namespace("namespace".to_string()); object_meta.set_labels(StringMap::new()); let object_meta_clone = object_meta.clone(); - assert_eq!( - object_meta.into_kube(), - object_meta_clone.into_kube() - ); + assert_eq!(object_meta.into_kube(), object_meta_clone.into_kube()); } #[test] -#[verifier(external)] pub fn test_set_owner_references() { let mut object_meta = ObjectMeta::default(); let own_refs_gen = || { - let own_ref = deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::OwnerReference::default(); + let own_ref = + deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::OwnerReference::default(); let mut owner_references = Vec::new(); owner_references.push(OwnerReference::from_kube(own_ref.clone())); owner_references }; object_meta.set_owner_references(own_refs_gen()); - assert_eq!(own_refs_gen().into_iter().map(|s: OwnerReference| s.into_kube()).collect::>(), object_meta.into_kube().owner_references.unwrap()); + assert_eq!( + own_refs_gen() + .into_iter() + .map(|s: OwnerReference| s.into_kube()) + .collect::>(), + object_meta.into_kube().owner_references.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_object_meta = - deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - name: Some("name".to_string()), - namespace: Some("namespace".to_string()), - labels: Some( - vec![ - ( - "key".to_string(), - "value".to_string(), - ), - ] - .into_iter() - .collect(), - ), - annotations: Some( - vec![ - ( - "key".to_string(), - "value".to_string(), - ), - ] + let kube_object_meta = deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), + namespace: Some("namespace".to_string()), + labels: Some( + vec![("key".to_string(), "value".to_string())] .into_iter() .collect(), - ), - finalizers: Some( - vec![ - "finalizer".to_string(), - ] + ), + annotations: Some( + vec![("key".to_string(), "value".to_string())] .into_iter() .collect(), - ), - owner_references: Some( - vec![ - deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::OwnerReference::default(), - ] - ), - ..Default::default() - }; + ), + finalizers: Some(vec!["finalizer".to_string()].into_iter().collect()), + owner_references: Some(vec![ + deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::OwnerReference::default(), + ]), + ..Default::default() + }; let object_meta = ObjectMeta::from_kube(kube_object_meta.clone()); - assert_eq!(object_meta.into_kube(), - kube_object_meta); -} + assert_eq!(object_meta.into_kube(), kube_object_meta); } diff --git a/src/unit_tests/kubernetes_api_objects/owner_reference.rs b/src/unit_tests/kubernetes_api_objects/owner_reference.rs index 9c25b2e52..dda4313e7 100644 --- a/src/unit_tests/kubernetes_api_objects/owner_reference.rs +++ b/src/unit_tests/kubernetes_api_objects/owner_reference.rs @@ -9,10 +9,7 @@ use deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::Time; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for owner reference #[test] -#[verifier(external)] pub fn test_kube() { let kube_owner_reference = deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::OwnerReference { @@ -23,9 +20,5 @@ pub fn test_kube() { ..Default::default() }; let owner_reference = OwnerReference::from_kube(kube_owner_reference.clone()); - assert_eq!( - owner_reference.into_kube(), - kube_owner_reference - ); -} + assert_eq!(owner_reference.into_kube(), kube_owner_reference); } diff --git a/src/unit_tests/kubernetes_api_objects/persistent_volume_claim.rs b/src/unit_tests/kubernetes_api_objects/persistent_volume_claim.rs index 328447504..4df37ca8b 100644 --- a/src/unit_tests/kubernetes_api_objects/persistent_volume_claim.rs +++ b/src/unit_tests/kubernetes_api_objects/persistent_volume_claim.rs @@ -9,10 +9,7 @@ use std::collections::BTreeMap; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for persistent volume claim #[test] -#[verifier(external)] pub fn test_default() { let persistent_volume_claim = PersistentVolumeClaim::default(); assert_eq!( @@ -22,7 +19,6 @@ pub fn test_default() { } #[test] -#[verifier(external)] pub fn test_set_metadata() { let mut object_meta = ObjectMeta::default(); object_meta.set_name("name".to_string()); @@ -36,7 +32,6 @@ pub fn test_set_metadata() { } #[test] -#[verifier(external)] pub fn test_metadata() { let mut object_meta = ObjectMeta::default(); object_meta.set_name("name".to_string()); @@ -50,7 +45,6 @@ pub fn test_metadata() { } #[test] -#[verifier(external)] pub fn test_set_spec() { let mut persistent_volume_claim_spec = PersistentVolumeClaimSpec::default(); persistent_volume_claim_spec.set_access_modes(vec!["ReadWriteOnce".to_string()]); @@ -64,7 +58,6 @@ pub fn test_set_spec() { } #[test] -#[verifier(external)] pub fn test_spec() { let mut persistent_volume_claim_spec = PersistentVolumeClaimSpec::default(); persistent_volume_claim_spec.set_access_modes(vec!["ReadWriteOnce".to_string()]); @@ -81,42 +74,35 @@ pub fn test_spec() { } #[test] -#[verifier(external)] -pub fn test_api_resource(){ +pub fn test_api_resource() { let api_resource = PersistentVolumeClaim::api_resource(); assert_eq!(api_resource.into_kube().kind, "PersistentVolumeClaim"); } #[test] -#[verifier(external)] pub fn test_kube() { let kube_persistent_volume_claim = deps_hack::k8s_openapi::api::core::v1::PersistentVolumeClaim { - metadata: - deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - name: Some("name".to_string()), - namespace: Some("namespace".to_string()), - ..Default::default() - }, + metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), + namespace: Some("namespace".to_string()), + ..Default::default() + }, spec: Some( deps_hack::k8s_openapi::api::core::v1::PersistentVolumeClaimSpec { access_modes: Some( - vec![ - "ReadWriteOnce".to_string(), - "ReadOnlyMany".to_string(), - ] - .into_iter() - .collect(), + vec!["ReadWriteOnce".to_string(), "ReadOnlyMany".to_string()] + .into_iter() + .collect(), ), resources: Some( deps_hack::k8s_openapi::api::core::v1::VolumeResourceRequirements { - requests: Some( - BTreeMap::from([ - ( - "storage".to_string(), deps_hack::k8s_openapi::apimachinery::pkg::api::resource::Quantity("1Gi".to_string()) - ), - ]) - ), + requests: Some(BTreeMap::from([( + "storage".to_string(), + deps_hack::k8s_openapi::apimachinery::pkg::api::resource::Quantity( + "1Gi".to_string(), + ), + )])), ..Default::default() }, ), @@ -127,7 +113,8 @@ pub fn test_kube() { ..Default::default() }; - let persistent_volume_claim = PersistentVolumeClaim::from_kube(kube_persistent_volume_claim.clone()); + let persistent_volume_claim = + PersistentVolumeClaim::from_kube(kube_persistent_volume_claim.clone()); assert_eq!( persistent_volume_claim.into_kube(), @@ -136,35 +123,29 @@ pub fn test_kube() { } #[test] -#[verifier(external)] pub fn test_marshal() { let kube_persistent_volume_claim = deps_hack::k8s_openapi::api::core::v1::PersistentVolumeClaim { - metadata: - deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - name: Some("name".to_string()), - namespace: Some("namespace".to_string()), - ..Default::default() - }, + metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), + namespace: Some("namespace".to_string()), + ..Default::default() + }, spec: Some( deps_hack::k8s_openapi::api::core::v1::PersistentVolumeClaimSpec { access_modes: Some( - vec![ - "ReadWriteOnce".to_string(), - "ReadOnlyMany".to_string(), - ] - .into_iter() - .collect(), + vec!["ReadWriteOnce".to_string(), "ReadOnlyMany".to_string()] + .into_iter() + .collect(), ), resources: Some( deps_hack::k8s_openapi::api::core::v1::VolumeResourceRequirements { - requests: Some( - BTreeMap::from([ - ( - "storage".to_string(), deps_hack::k8s_openapi::apimachinery::pkg::api::resource::Quantity("1Gi".to_string()) - ), - ]) - ), + requests: Some(BTreeMap::from([( + "storage".to_string(), + deps_hack::k8s_openapi::apimachinery::pkg::api::resource::Quantity( + "1Gi".to_string(), + ), + )])), ..Default::default() }, ), @@ -175,11 +156,13 @@ pub fn test_marshal() { ..Default::default() }; - let persistent_volume_claim = PersistentVolumeClaim::from_kube(kube_persistent_volume_claim.clone()); + let persistent_volume_claim = + PersistentVolumeClaim::from_kube(kube_persistent_volume_claim.clone()); assert_eq!( kube_persistent_volume_claim, - PersistentVolumeClaim::unmarshal(persistent_volume_claim.marshal()).unwrap().into_kube() + PersistentVolumeClaim::unmarshal(persistent_volume_claim.marshal()) + .unwrap() + .into_kube() ); } -} diff --git a/src/unit_tests/kubernetes_api_objects/persistent_volume_claim_spec.rs b/src/unit_tests/kubernetes_api_objects/persistent_volume_claim_spec.rs index 25142793c..5aeb938dd 100644 --- a/src/unit_tests/kubernetes_api_objects/persistent_volume_claim_spec.rs +++ b/src/unit_tests/kubernetes_api_objects/persistent_volume_claim_spec.rs @@ -10,10 +10,7 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for persistent volume claim spec #[test] -#[verifier(external)] pub fn test_default() { let persistent_volume_claim_spec = PersistentVolumeClaimSpec::default(); assert_eq!( @@ -23,7 +20,6 @@ pub fn test_default() { } #[test] -#[verifier(external)] pub fn test_set_access_modes() { let mut persistent_volume_claim_spec = PersistentVolumeClaimSpec::default(); let access_modes_gen = || { @@ -35,12 +31,14 @@ pub fn test_set_access_modes() { persistent_volume_claim_spec.set_access_modes(access_modes_gen()); assert_eq!( access_modes_gen(), - persistent_volume_claim_spec.into_kube().access_modes.unwrap() + persistent_volume_claim_spec + .into_kube() + .access_modes + .unwrap() ); } #[test] -#[verifier(external)] pub fn test_set_resources() { let mut persistent_volume_claim_spec = PersistentVolumeClaimSpec::default(); let mut resources = VolumeResourceRequirements::default(); @@ -54,8 +52,7 @@ pub fn test_set_resources() { ); } #[test] -#[verifier(external)] -pub fn test_clone(){ +pub fn test_clone() { let mut persistent_volume_claim_spec = PersistentVolumeClaimSpec::default(); let mut resources = VolumeResourceRequirements::default(); let mut requests = StringMap::new(); @@ -65,43 +62,43 @@ pub fn test_clone(){ let persistent_volume_claim_spec_clone = persistent_volume_claim_spec.clone(); assert_eq!( resources.into_kube(), - persistent_volume_claim_spec_clone.into_kube().resources.unwrap() + persistent_volume_claim_spec_clone + .into_kube() + .resources + .unwrap() ); } #[test] -#[verifier(external)] pub fn test_set_storage_class_name() { let mut persistent_volume_claim_spec = PersistentVolumeClaimSpec::default(); persistent_volume_claim_spec.set_storage_class_name("storage_class_name".to_string()); assert_eq!( "storage_class_name".to_string(), - persistent_volume_claim_spec.into_kube().storage_class_name.unwrap() + persistent_volume_claim_spec + .into_kube() + .storage_class_name + .unwrap() ); } #[test] -#[verifier(external)] pub fn test_kube() { let kube_persistent_volume_claim_spec = deps_hack::k8s_openapi::api::core::v1::PersistentVolumeClaimSpec { access_modes: Some( - vec![ - "ReadWriteOnce".to_string(), - "ReadOnlyMany".to_string(), - ] - .into_iter() - .collect(), + vec!["ReadWriteOnce".to_string(), "ReadOnlyMany".to_string()] + .into_iter() + .collect(), ), resources: Some( deps_hack::k8s_openapi::api::core::v1::VolumeResourceRequirements { - requests: Some( - BTreeMap::from([ - ( - "storage".to_string(), deps_hack::k8s_openapi::apimachinery::pkg::api::resource::Quantity("1Gi".to_string()) - ), - ]) - ), + requests: Some(BTreeMap::from([( + "storage".to_string(), + deps_hack::k8s_openapi::apimachinery::pkg::api::resource::Quantity( + "1Gi".to_string(), + ), + )])), ..Default::default() }, ), @@ -109,11 +106,10 @@ pub fn test_kube() { ..Default::default() }; - let persistent_volume_claim_spec = PersistentVolumeClaimSpec::from_kube(kube_persistent_volume_claim_spec.clone()); + let persistent_volume_claim_spec = + PersistentVolumeClaimSpec::from_kube(kube_persistent_volume_claim_spec.clone()); assert_eq!( persistent_volume_claim_spec.into_kube(), kube_persistent_volume_claim_spec ); } - -} diff --git a/src/unit_tests/kubernetes_api_objects/pod.rs b/src/unit_tests/kubernetes_api_objects/pod.rs index e817cf63f..ae7d35f81 100644 --- a/src/unit_tests/kubernetes_api_objects/pod.rs +++ b/src/unit_tests/kubernetes_api_objects/pod.rs @@ -8,17 +8,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for pod #[test] -#[verifier(external)] pub fn test_default() { let pod = Pod::default(); - assert_eq!(pod.into_kube(), deps_hack::k8s_openapi::api::core::v1::Pod::default()); + assert_eq!( + pod.into_kube(), + deps_hack::k8s_openapi::api::core::v1::Pod::default() + ); } #[test] -#[verifier(external)] pub fn test_metadata() { let mut object_meta = ObjectMeta::default(); object_meta.set_name("name".to_string()); @@ -29,7 +28,6 @@ pub fn test_metadata() { } #[test] -#[verifier(external)] pub fn test_spec() { let mut pod_spec = PodSpec::default(); let mut container = Container::default(); @@ -41,7 +39,6 @@ pub fn test_spec() { } #[test] -#[verifier(external)] pub fn test_set_metadata() { let mut object_meta = ObjectMeta::default(); object_meta.set_name("name".to_string()); @@ -52,7 +49,6 @@ pub fn test_set_metadata() { } #[test] -#[verifier(external)] pub fn test_set_spec() { let mut pod_spec = PodSpec::default(); let mut container = Container::default(); @@ -64,14 +60,12 @@ pub fn test_set_spec() { } #[test] -#[verifier(external)] pub fn test_api_resource() { let api_resource = Pod::api_resource(); assert_eq!(api_resource.into_kube().kind, "Pod"); } #[test] -#[verifier(external)] pub fn test_kube() { let kube_pod = deps_hack::k8s_openapi::api::core::v1::Pod { metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { @@ -90,14 +84,10 @@ pub fn test_kube() { let pod = Pod::from_kube(kube_pod.clone()); - assert_eq!( - pod.into_kube(), - kube_pod - ); + assert_eq!(pod.into_kube(), kube_pod); } #[test] -#[verifier(external)] pub fn test_marshal() { let kube_pod = deps_hack::k8s_openapi::api::core::v1::Pod { metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { @@ -116,9 +106,5 @@ pub fn test_marshal() { let pod = Pod::from_kube(kube_pod.clone()); - assert_eq!( - kube_pod, - Pod::unmarshal(pod.marshal()).unwrap().into_kube() - ); -} + assert_eq!(kube_pod, Pod::unmarshal(pod.marshal()).unwrap().into_kube()); } diff --git a/src/unit_tests/kubernetes_api_objects/pod_security_context.rs b/src/unit_tests/kubernetes_api_objects/pod_security_context.rs index 033da7651..ebd10efae 100644 --- a/src/unit_tests/kubernetes_api_objects/pod_security_context.rs +++ b/src/unit_tests/kubernetes_api_objects/pod_security_context.rs @@ -11,47 +11,32 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for pod security context #[test] -#[verifier(external)] pub fn test_kube() { - let kube_pod_security_context = - deps_hack::k8s_openapi::api::core::v1::PodSecurityContext { - fs_group: Some(1024), - run_as_group: Some(1024), - run_as_non_root: Some(true), - run_as_user: Some(1024), - se_linux_options: Some( - deps_hack::k8s_openapi::api::core::v1::SELinuxOptions { - level: Some("level".to_string()), - role: Some("role".to_string()), - type_: Some("type_".to_string()), - user: Some("user".to_string()), - ..Default::default() - }, - ), - supplemental_groups: Some( - vec![ - 1024, - 1024, - ], - ), - windows_options: Some( - deps_hack::k8s_openapi::api::core::v1::WindowsSecurityContextOptions { - gmsa_credential_spec: Some("gmsa_credential_spec".to_string()), - gmsa_credential_spec_name: Some("gmsa_credential_spec_name".to_string()), - run_as_user_name: Some("run_as_user_name".to_string()), - ..Default::default() - }, - ), + let kube_pod_security_context = deps_hack::k8s_openapi::api::core::v1::PodSecurityContext { + fs_group: Some(1024), + run_as_group: Some(1024), + run_as_non_root: Some(true), + run_as_user: Some(1024), + se_linux_options: Some(deps_hack::k8s_openapi::api::core::v1::SELinuxOptions { + level: Some("level".to_string()), + role: Some("role".to_string()), + type_: Some("type_".to_string()), + user: Some("user".to_string()), ..Default::default() - }; + }), + supplemental_groups: Some(vec![1024, 1024]), + windows_options: Some( + deps_hack::k8s_openapi::api::core::v1::WindowsSecurityContextOptions { + gmsa_credential_spec: Some("gmsa_credential_spec".to_string()), + gmsa_credential_spec_name: Some("gmsa_credential_spec_name".to_string()), + run_as_user_name: Some("run_as_user_name".to_string()), + ..Default::default() + }, + ), + ..Default::default() + }; let pod_security_context = PodSecurityContext::from_kube(kube_pod_security_context.clone()); - assert_eq!( - pod_security_context.into_kube(), - kube_pod_security_context - ); -} + assert_eq!(pod_security_context.into_kube(), kube_pod_security_context); } diff --git a/src/unit_tests/kubernetes_api_objects/pod_spec.rs b/src/unit_tests/kubernetes_api_objects/pod_spec.rs index ec52c3068..f48d2e96a 100644 --- a/src/unit_tests/kubernetes_api_objects/pod_spec.rs +++ b/src/unit_tests/kubernetes_api_objects/pod_spec.rs @@ -11,17 +11,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for pod spec #[test] -#[verifier(external)] pub fn test_default() { let pod_template_spec = PodSpec::default(); - assert_eq!(pod_template_spec.into_kube(), deps_hack::k8s_openapi::api::core::v1::PodSpec::default()); + assert_eq!( + pod_template_spec.into_kube(), + deps_hack::k8s_openapi::api::core::v1::PodSpec::default() + ); } #[test] -#[verifier(external)] pub fn test_clone() { let mut pod_spec = PodSpec::default(); let mut container = Container::default(); @@ -32,16 +31,17 @@ pub fn test_clone() { } #[test] -#[verifier(external)] pub fn test_set_affinity() { let mut pod_spec = PodSpec::default(); let affinity = Affinity::from_kube(deps_hack::k8s_openapi::api::core::v1::Affinity::default()); pod_spec.set_affinity(affinity); - assert_eq!(deps_hack::k8s_openapi::api::core::v1::Affinity::default(), pod_spec.into_kube().affinity.unwrap()); + assert_eq!( + deps_hack::k8s_openapi::api::core::v1::Affinity::default(), + pod_spec.into_kube().affinity.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_containers() { let mut pod_spec = PodSpec::default(); let mut container = Container::default(); @@ -49,11 +49,13 @@ pub fn test_set_containers() { container.set_name("name".to_string()); container2.set_name("name2".to_string()); pod_spec.set_containers(vec![container.clone(), container2.clone()]); - assert_eq!(vec![container.into_kube(), container2.into_kube()], pod_spec.into_kube().containers); + assert_eq!( + vec![container.into_kube(), container2.into_kube()], + pod_spec.into_kube().containers + ); } #[test] -#[verifier(external)] pub fn test_set_volumes() { let mut pod_spec = PodSpec::default(); let mut volume = Volume::default(); @@ -61,11 +63,13 @@ pub fn test_set_volumes() { volume.set_name("name".to_string()); volume2.set_name("name2".to_string()); pod_spec.set_volumes(vec![volume.clone(), volume2.clone()]); - assert_eq!(vec![volume.into_kube(), volume2.into_kube()], pod_spec.into_kube().volumes.unwrap()); + assert_eq!( + vec![volume.into_kube(), volume2.into_kube()], + pod_spec.into_kube().volumes.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_init_containers() { let mut pod_spec = PodSpec::default(); let mut container = Container::default(); @@ -73,121 +77,148 @@ pub fn test_set_init_containers() { container.set_name("name".to_string()); container2.set_name("name2".to_string()); pod_spec.set_init_containers(vec![container.clone(), container2.clone()]); - assert_eq!(vec![container.into_kube(), container2.into_kube()], pod_spec.into_kube().init_containers.unwrap()); + assert_eq!( + vec![container.into_kube(), container2.into_kube()], + pod_spec.into_kube().init_containers.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_service_account_name() { let mut pod_spec = PodSpec::default(); pod_spec.set_service_account_name("name".to_string()); - assert_eq!("name".to_string(), pod_spec.into_kube().service_account_name.unwrap()); + assert_eq!( + "name".to_string(), + pod_spec.into_kube().service_account_name.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_tolerations() { let mut pod_spec = PodSpec::default(); - let toleration = Toleration::from_kube(deps_hack::k8s_openapi::api::core::v1::Toleration::default()); + let toleration = + Toleration::from_kube(deps_hack::k8s_openapi::api::core::v1::Toleration::default()); pod_spec.set_tolerations(vec![toleration]); - assert_eq!(vec![deps_hack::k8s_openapi::api::core::v1::Toleration::default()], pod_spec.into_kube().tolerations.unwrap()); + assert_eq!( + vec![deps_hack::k8s_openapi::api::core::v1::Toleration::default()], + pod_spec.into_kube().tolerations.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_node_selector() { let mut pod_spec = PodSpec::default(); let mut node_selector = StringMap::new(); node_selector.insert("key".to_string(), "value".to_string()); pod_spec.set_node_selector(node_selector.clone()); - assert_eq!(node_selector.into_rust_map(), pod_spec.into_kube().node_selector.unwrap()); + assert_eq!( + node_selector.into_rust_map(), + pod_spec.into_kube().node_selector.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_runtime_class_name() { let mut pod_spec = PodSpec::default(); if pod_spec.clone().into_kube().runtime_class_name.is_some() { panic!("runtime_class_name should be None"); }; pod_spec.set_runtime_class_name("name".to_string()); - assert_eq!("name".to_string(), pod_spec.clone().into_kube().runtime_class_name.unwrap()); + assert_eq!( + "name".to_string(), + pod_spec.clone().into_kube().runtime_class_name.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_dns_policy() { let mut pod_spec = PodSpec::default(); if pod_spec.clone().into_kube().dns_policy.is_some() { panic!("dns_policy should be None"); }; pod_spec.set_dns_policy("name".to_string()); - assert_eq!("name".to_string(), pod_spec.clone().into_kube().dns_policy.unwrap()); + assert_eq!( + "name".to_string(), + pod_spec.clone().into_kube().dns_policy.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_scheduler_name() { let mut pod_spec = PodSpec::default(); if pod_spec.clone().into_kube().scheduler_name.is_some() { panic!("scheduler_name should be None"); }; pod_spec.set_scheduler_name("name".to_string()); - assert_eq!("name".to_string(), pod_spec.clone().into_kube().scheduler_name.unwrap()); + assert_eq!( + "name".to_string(), + pod_spec.clone().into_kube().scheduler_name.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_priority_class_name() { let mut pod_spec = PodSpec::default(); if pod_spec.clone().into_kube().priority_class_name.is_some() { panic!("priority_class_name should be None"); }; pod_spec.set_priority_class_name("name".to_string()); - assert_eq!("name".to_string(), pod_spec.clone().into_kube().priority_class_name.unwrap()); + assert_eq!( + "name".to_string(), + pod_spec.clone().into_kube().priority_class_name.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_security_context() { let mut pod_spec = PodSpec::default(); - let security_context = PodSecurityContext::from_kube(deps_hack::k8s_openapi::api::core::v1::PodSecurityContext::default()); + let security_context = PodSecurityContext::from_kube( + deps_hack::k8s_openapi::api::core::v1::PodSecurityContext::default(), + ); pod_spec.set_security_context(security_context); - assert_eq!(deps_hack::k8s_openapi::api::core::v1::PodSecurityContext::default(), pod_spec.into_kube().security_context.unwrap()); + assert_eq!( + deps_hack::k8s_openapi::api::core::v1::PodSecurityContext::default(), + pod_spec.into_kube().security_context.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_host_network() { let mut pod_spec = PodSpec::default(); pod_spec.set_host_network(true); assert_eq!(true, pod_spec.into_kube().host_network.unwrap()); } - #[test] -#[verifier(external)] -pub fn test_set_image_pull_secrets(){ +pub fn test_set_image_pull_secrets() { let mut pod_spec = PodSpec::default(); let kube_local_object_reference = deps_hack::k8s_openapi::api::core::v1::LocalObjectReference { name: Some("name".to_string()), }; - let local_object_reference = LocalObjectReference::from_kube(kube_local_object_reference.clone()); + let local_object_reference = + LocalObjectReference::from_kube(kube_local_object_reference.clone()); pod_spec.set_image_pull_secrets(vec![local_object_reference]); - assert_eq!(vec![kube_local_object_reference], pod_spec.into_kube().image_pull_secrets.unwrap()); + assert_eq!( + vec![kube_local_object_reference], + pod_spec.into_kube().image_pull_secrets.unwrap() + ); } #[test] -#[verifier(external)] -pub fn test_set_termination_grace_period_seconds(){ +pub fn test_set_termination_grace_period_seconds() { let mut pod_spec = PodSpec::default(); pod_spec.set_termination_grace_period_seconds(1); - assert_eq!(1, pod_spec.into_kube().termination_grace_period_seconds.unwrap()); + assert_eq!( + 1, + pod_spec + .into_kube() + .termination_grace_period_seconds + .unwrap() + ); } #[test] -#[verifier(external)] pub fn test_kube() { let kube_pod_spec = deps_hack::k8s_openapi::api::core::v1::PodSpec { @@ -335,9 +366,5 @@ pub fn test_kube() { }; let pod_spec = PodSpec::from_kube(kube_pod_spec.clone()); - assert_eq!( - pod_spec.into_kube(), - kube_pod_spec - ); -} + assert_eq!(pod_spec.into_kube(), kube_pod_spec); } diff --git a/src/unit_tests/kubernetes_api_objects/pod_template_spec.rs b/src/unit_tests/kubernetes_api_objects/pod_template_spec.rs index 74f83b373..152a00c64 100644 --- a/src/unit_tests/kubernetes_api_objects/pod_template_spec.rs +++ b/src/unit_tests/kubernetes_api_objects/pod_template_spec.rs @@ -9,28 +9,29 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for pod template spec #[test] -#[verifier(external)] pub fn test_default() { let pod_template_spec = PodTemplateSpec::default(); - assert_eq!(pod_template_spec.into_kube(), deps_hack::k8s_openapi::api::core::v1::PodTemplateSpec::default()); + assert_eq!( + pod_template_spec.into_kube(), + deps_hack::k8s_openapi::api::core::v1::PodTemplateSpec::default() + ); } #[test] -#[verifier(external)] pub fn test_set_metadata() { let mut object_meta = ObjectMeta::default(); object_meta.set_name("name".to_string()); let mut pod_template_spec = PodTemplateSpec::default(); pod_template_spec.set_metadata(object_meta.clone()); - assert_eq!(object_meta.into_kube(), pod_template_spec.into_kube().metadata.unwrap()); + assert_eq!( + object_meta.into_kube(), + pod_template_spec.into_kube().metadata.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_spec() { let mut pod_spec = PodSpec::default(); let mut container = Container::default(); @@ -38,11 +39,13 @@ pub fn test_set_spec() { pod_spec.set_containers(vec![container.clone()]); let mut pod_template_spec = PodTemplateSpec::default(); pod_template_spec.set_spec(pod_spec.clone()); - assert_eq!(pod_spec.into_kube(), pod_template_spec.into_kube().spec.unwrap()); + assert_eq!( + pod_spec.into_kube(), + pod_template_spec.into_kube().spec.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_clone() { let mut pod_template_spec = PodTemplateSpec::default(); let mut pod_spec = PodSpec::default(); @@ -51,19 +54,23 @@ pub fn test_clone() { pod_spec.set_containers(vec![container.clone()]); pod_template_spec.set_spec(pod_spec.clone()); let pod_template_spec_clone = pod_template_spec.clone(); - assert_eq!(pod_template_spec.into_kube(), pod_template_spec_clone.into_kube()); + assert_eq!( + pod_template_spec.into_kube(), + pod_template_spec_clone.into_kube() + ); } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_pod_template_spec = deps_hack::k8s_openapi::api::core::v1::PodTemplateSpec{ - metadata: Some(deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta{ - name: Some("name".to_string()), - ..Default::default() - }), - spec: Some(deps_hack::k8s_openapi::api::core::v1::PodSpec{ - containers: vec![deps_hack::k8s_openapi::api::core::v1::Container{ + let kube_pod_template_spec = deps_hack::k8s_openapi::api::core::v1::PodTemplateSpec { + metadata: Some( + deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), + ..Default::default() + }, + ), + spec: Some(deps_hack::k8s_openapi::api::core::v1::PodSpec { + containers: vec![deps_hack::k8s_openapi::api::core::v1::Container { name: "name".to_string(), ..Default::default() }], @@ -74,7 +81,5 @@ pub fn test_kube() { let pod_template_spec = PodTemplateSpec::from_kube(kube_pod_template_spec.clone()); - assert_eq!(pod_template_spec.into_kube(), - kube_pod_template_spec); -} + assert_eq!(pod_template_spec.into_kube(), kube_pod_template_spec); } diff --git a/src/unit_tests/kubernetes_api_objects/policy_rule.rs b/src/unit_tests/kubernetes_api_objects/policy_rule.rs index 21d1a60d1..e9669e598 100644 --- a/src/unit_tests/kubernetes_api_objects/policy_rule.rs +++ b/src/unit_tests/kubernetes_api_objects/policy_rule.rs @@ -7,17 +7,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for policy rule #[test] -#[verifier(external)] pub fn test_default() { let policy_rule = PolicyRule::default(); - assert_eq!(policy_rule.into_kube(), deps_hack::k8s_openapi::api::rbac::v1::PolicyRule::default()); + assert_eq!( + policy_rule.into_kube(), + deps_hack::k8s_openapi::api::rbac::v1::PolicyRule::default() + ); } #[test] -#[verifier(external)] pub fn test_set_api_groups() { let mut policy_rule = PolicyRule::default(); let api_groups_gen = || { @@ -36,7 +35,6 @@ pub fn test_set_api_groups() { } #[test] -#[verifier(external)] pub fn test_set_resources() { let mut policy_rule = PolicyRule::default(); let resources_gen = || { @@ -48,14 +46,10 @@ pub fn test_set_resources() { resources }; policy_rule.set_resources(resources_gen()); - assert_eq!( - resources_gen(), - policy_rule.into_kube().resources.unwrap() - ); + assert_eq!(resources_gen(), policy_rule.into_kube().resources.unwrap()); } #[test] -#[verifier(external)] pub fn test_set_verbs() { let mut policy_rule = PolicyRule::default(); let verbs_gen = || { @@ -67,28 +61,19 @@ pub fn test_set_verbs() { verbs }; policy_rule.set_verbs(verbs_gen()); - assert_eq!( - verbs_gen(), - policy_rule.into_kube().verbs - ); + assert_eq!(verbs_gen(), policy_rule.into_kube().verbs); } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_policy_rule = - deps_hack::k8s_openapi::api::rbac::v1::PolicyRule { - api_groups: Some(vec!["api_groups".to_string()]), - resources: Some(vec!["resources".to_string()]), - verbs: vec!["verbs".to_string()], - ..Default::default() - }; + let kube_policy_rule = deps_hack::k8s_openapi::api::rbac::v1::PolicyRule { + api_groups: Some(vec!["api_groups".to_string()]), + resources: Some(vec!["resources".to_string()]), + verbs: vec!["verbs".to_string()], + ..Default::default() + }; let policy_rule = PolicyRule::from_kube(kube_policy_rule.clone()); - assert_eq!( - policy_rule.into_kube(), - kube_policy_rule - ); -} + assert_eq!(policy_rule.into_kube(), kube_policy_rule); } diff --git a/src/unit_tests/kubernetes_api_objects/probe.rs b/src/unit_tests/kubernetes_api_objects/probe.rs index 7a5b0c125..833a60495 100644 --- a/src/unit_tests/kubernetes_api_objects/probe.rs +++ b/src/unit_tests/kubernetes_api_objects/probe.rs @@ -7,12 +7,8 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for Probe - #[test] -#[verifier(external)] -pub fn test_set_exec(){ +pub fn test_set_exec() { let mut probe = Probe::default(); let mut exec_action = ExecAction::default(); exec_action.set_command(vec!["command".to_string()]); @@ -21,7 +17,6 @@ pub fn test_set_exec(){ } #[test] -#[verifier(external)] pub fn test_set_failure_threshold() { let mut probe = Probe::default(); probe.set_failure_threshold(3); @@ -29,7 +24,6 @@ pub fn test_set_failure_threshold() { } #[test] -#[verifier(external)] pub fn test_set_initial_delay_seconds() { let mut probe = Probe::default(); probe.set_initial_delay_seconds(3); @@ -37,7 +31,6 @@ pub fn test_set_initial_delay_seconds() { } #[test] -#[verifier(external)] pub fn test_set_period_seconds() { let mut probe = Probe::default(); probe.set_period_seconds(3); @@ -45,7 +38,6 @@ pub fn test_set_period_seconds() { } #[test] -#[verifier(external)] pub fn test_set_success_threshold() { let mut probe = Probe::default(); probe.set_success_threshold(3); @@ -53,7 +45,6 @@ pub fn test_set_success_threshold() { } #[test] -#[verifier(external)] pub fn test_set_tcp_socket() { let mut probe = Probe::default(); let mut tcp_socket_action = TCPSocketAction::default(); @@ -61,11 +52,13 @@ pub fn test_set_tcp_socket() { tcp_socket_action.set_port(8080); probe.set_tcp_socket(tcp_socket_action.clone()); - assert_eq!(tcp_socket_action.into_kube(), probe.into_kube().tcp_socket.unwrap()); + assert_eq!( + tcp_socket_action.into_kube(), + probe.into_kube().tcp_socket.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_timeout_seconds() { let mut probe = Probe::default(); probe.set_timeout_seconds(3); @@ -73,14 +66,15 @@ pub fn test_set_timeout_seconds() { } #[test] -#[verifier(external)] pub fn test_default() { let probe = Probe::default(); - assert_eq!(probe.into_kube(), deps_hack::k8s_openapi::api::core::v1::Probe::default()); + assert_eq!( + probe.into_kube(), + deps_hack::k8s_openapi::api::core::v1::Probe::default() + ); } #[test] -#[verifier(external)] pub fn test_clone() { let mut probe = Probe::default(); probe.set_timeout_seconds(3); @@ -89,7 +83,6 @@ pub fn test_clone() { } #[test] -#[verifier(external)] pub fn test_kube() { let kube_probe = deps_hack::k8s_openapi::api::core::v1::Probe { failure_threshold: Some(3), @@ -107,5 +100,3 @@ pub fn test_kube() { assert_eq!(probe.into_kube(), kube_probe); } - -} diff --git a/src/unit_tests/kubernetes_api_objects/projected_volume_source.rs b/src/unit_tests/kubernetes_api_objects/projected_volume_source.rs index 4422306a9..2971bc0e7 100644 --- a/src/unit_tests/kubernetes_api_objects/projected_volume_source.rs +++ b/src/unit_tests/kubernetes_api_objects/projected_volume_source.rs @@ -9,17 +9,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for projected volume source #[test] -#[verifier(external)] pub fn test_default() { let projected_volume_source = ProjectedVolumeSource::default(); - assert_eq!(projected_volume_source.into_kube(), deps_hack::k8s_openapi::api::core::v1::ProjectedVolumeSource::default()); + assert_eq!( + projected_volume_source.into_kube(), + deps_hack::k8s_openapi::api::core::v1::ProjectedVolumeSource::default() + ); } #[test] -#[verifier(external)] pub fn test_set_sources() { let mut projected_volume_source = ProjectedVolumeSource::default(); let volume_projections_gen = || { @@ -43,8 +42,7 @@ pub fn test_set_sources() { } #[test] -#[verifier(external)] -pub fn test_clone(){ +pub fn test_clone() { let mut projected_volume_source = ProjectedVolumeSource::default(); let volume_projections_gen = || { let mut volume_projection_1 = VolumeProjection::default(); @@ -58,33 +56,38 @@ pub fn test_clone(){ }; projected_volume_source.set_sources(volume_projections_gen()); let projected_volume_source_clone = projected_volume_source.clone(); - assert_eq!(projected_volume_source.into_kube(), projected_volume_source_clone.into_kube()); + assert_eq!( + projected_volume_source.into_kube(), + projected_volume_source_clone.into_kube() + ); } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_projected_volume_source = deps_hack::k8s_openapi::api::core::v1::ProjectedVolumeSource{ - sources: Some( - vec![ - deps_hack::k8s_openapi::api::core::v1::VolumeProjection{ - config_map: Some(deps_hack::k8s_openapi::api::core::v1::ConfigMapProjection::default()), + let kube_projected_volume_source = + deps_hack::k8s_openapi::api::core::v1::ProjectedVolumeSource { + sources: Some(vec![ + deps_hack::k8s_openapi::api::core::v1::VolumeProjection { + config_map: Some( + deps_hack::k8s_openapi::api::core::v1::ConfigMapProjection::default(), + ), ..Default::default() }, - deps_hack::k8s_openapi::api::core::v1::VolumeProjection{ - secret: Some(deps_hack::k8s_openapi::api::core::v1::SecretProjection::default()), + deps_hack::k8s_openapi::api::core::v1::VolumeProjection { + secret: Some( + deps_hack::k8s_openapi::api::core::v1::SecretProjection::default(), + ), ..Default::default() - } - ] - ), - ..Default::default() - }; + }, + ]), + ..Default::default() + }; - let projected_volume_source = ProjectedVolumeSource::from_kube(kube_projected_volume_source.clone()); + let projected_volume_source = + ProjectedVolumeSource::from_kube(kube_projected_volume_source.clone()); assert_eq!( projected_volume_source.into_kube(), kube_projected_volume_source ); } -} diff --git a/src/unit_tests/kubernetes_api_objects/resource_requirements.rs b/src/unit_tests/kubernetes_api_objects/resource_requirements.rs index 21b8de6ae..906cc676f 100644 --- a/src/unit_tests/kubernetes_api_objects/resource_requirements.rs +++ b/src/unit_tests/kubernetes_api_objects/resource_requirements.rs @@ -9,39 +9,51 @@ use std::collections::BTreeMap; use vstd::prelude::*; use vstd::string::*; -verus! { #[test] -#[verifier(external)] -pub fn test_default(){ +pub fn test_default() { let resource_requirements = ResourceRequirements::default(); - assert_eq!(resource_requirements.into_kube(), deps_hack::k8s_openapi::api::core::v1::ResourceRequirements::default()); + assert_eq!( + resource_requirements.into_kube(), + deps_hack::k8s_openapi::api::core::v1::ResourceRequirements::default() + ); } #[test] -#[verifier(external)] -pub fn test_set_requests(){ +pub fn test_set_requests() { let mut resource_requirements = ResourceRequirements::default(); let mut requests = StringMap::new(); requests.insert("cpu".to_string(), "100m".to_string()); resource_requirements.set_requests(requests.clone()); - let quantity_request: BTreeMap = requests.into_rust_map().into_iter().map(|(k, v)| (k, Quantity(v))).collect(); - assert_eq!(quantity_request, resource_requirements.into_kube().requests.unwrap()); + let quantity_request: BTreeMap = requests + .into_rust_map() + .into_iter() + .map(|(k, v)| (k, Quantity(v))) + .collect(); + assert_eq!( + quantity_request, + resource_requirements.into_kube().requests.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_limits() { let mut resource_requirements = ResourceRequirements::default(); let mut limits = StringMap::new(); limits.insert("cpu".to_string(), "100m".to_string()); resource_requirements.set_limits(limits.clone()); - let quantity_limits: BTreeMap = limits.into_rust_map().into_iter().map(|(k, v)| (k, Quantity(v))).collect(); - assert_eq!(quantity_limits, resource_requirements.into_kube().limits.unwrap()); + let quantity_limits: BTreeMap = limits + .into_rust_map() + .into_iter() + .map(|(k, v)| (k, Quantity(v))) + .collect(); + assert_eq!( + quantity_limits, + resource_requirements.into_kube().limits.unwrap() + ); } #[test] -#[verifier(external)] -pub fn test_clone(){ +pub fn test_clone() { let mut resource_requirements = ResourceRequirements::default(); let mut requests = StringMap::new(); requests.insert("cpu".to_string(), "100m".to_string()); @@ -50,11 +62,13 @@ pub fn test_clone(){ limits.insert("cpu".to_string(), "100m".to_string()); resource_requirements.set_limits(limits.clone()); let resource_requirements_clone = resource_requirements.clone(); - assert_eq!(resource_requirements.into_kube(), resource_requirements_clone.into_kube()); + assert_eq!( + resource_requirements.into_kube(), + resource_requirements_clone.into_kube() + ); } #[test] -#[verifier(external)] pub fn test_kube() { let kube_resource_requirements = deps_hack::k8s_openapi::api::core::v1::ResourceRequirements { limits: Some( @@ -76,7 +90,4 @@ pub fn test_kube() { resource_requirements.into_kube(), kube_resource_requirements ); - -} - } diff --git a/src/unit_tests/kubernetes_api_objects/role.rs b/src/unit_tests/kubernetes_api_objects/role.rs index 779f76699..48f0c9fd6 100644 --- a/src/unit_tests/kubernetes_api_objects/role.rs +++ b/src/unit_tests/kubernetes_api_objects/role.rs @@ -7,17 +7,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for role #[test] -#[verifier(external)] pub fn test_default() { let role = Role::default(); - assert_eq!(role.into_kube(), deps_hack::k8s_openapi::api::rbac::v1::Role::default()); + assert_eq!( + role.into_kube(), + deps_hack::k8s_openapi::api::rbac::v1::Role::default() + ); } #[test] -#[verifier(external)] pub fn test_set_metadata() { let mut role = Role::default(); let mut object_meta = ObjectMeta::default(); @@ -27,7 +26,6 @@ pub fn test_set_metadata() { } #[test] -#[verifier(external)] pub fn test_metadata() { let mut role = Role::default(); let mut object_meta = ObjectMeta::default(); @@ -37,7 +35,6 @@ pub fn test_metadata() { } #[test] -#[verifier(external)] pub fn test_set_rules() { let mut role = Role::default(); let policy_rule_gen = || { @@ -89,7 +86,6 @@ pub fn test_set_rules() { } #[test] -#[verifier(external)] pub fn test_clone() { let mut role = Role::default(); let mut object_meta = ObjectMeta::default(); @@ -140,77 +136,89 @@ pub fn test_clone() { } #[test] -#[verifier(external)] -pub fn test_api_resource(){ +pub fn test_api_resource() { let api_resource = Role::api_resource(); assert_eq!(api_resource.into_kube().kind, "Role"); } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_role = - deps_hack::k8s_openapi::api::rbac::v1::Role { - metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - name: Some("name".to_string()), - namespace: Some("namespace".to_string()), + let kube_role = deps_hack::k8s_openapi::api::rbac::v1::Role { + metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), + namespace: Some("namespace".to_string()), + ..Default::default() + }, + rules: Some(vec![ + deps_hack::k8s_openapi::api::rbac::v1::PolicyRule { + api_groups: Some(vec![ + "api_groups_1_1".to_string(), + "api_groups_1_2".to_string(), + ]), + resources: Some(vec![ + "resources_1_1".to_string(), + "resources_1_2".to_string(), + ]), + verbs: vec!["verbs_1_1".to_string(), "verbs_1_2".to_string()], ..Default::default() }, - rules: Some( - vec![ - deps_hack::k8s_openapi::api::rbac::v1::PolicyRule { - api_groups: Some(vec!["api_groups_1_1".to_string(), "api_groups_1_2".to_string()]), - resources: Some(vec!["resources_1_1".to_string(), "resources_1_2".to_string()]), - verbs: vec!["verbs_1_1".to_string(), "verbs_1_2".to_string()], - ..Default::default() - }, - deps_hack::k8s_openapi::api::rbac::v1::PolicyRule { - api_groups: Some(vec!["api_groups_2_1".to_string(), "api_groups_2_2".to_string()]), - resources: Some(vec!["resources_2_1".to_string(), "resources_2_2".to_string()]), - verbs: vec!["verbs_2_1".to_string(), "verbs_2_2".to_string()], - ..Default::default() - } - ] - ), - ..Default::default() - }; + deps_hack::k8s_openapi::api::rbac::v1::PolicyRule { + api_groups: Some(vec![ + "api_groups_2_1".to_string(), + "api_groups_2_2".to_string(), + ]), + resources: Some(vec![ + "resources_2_1".to_string(), + "resources_2_2".to_string(), + ]), + verbs: vec!["verbs_2_1".to_string(), "verbs_2_2".to_string()], + ..Default::default() + }, + ]), + ..Default::default() + }; let role = Role::from_kube(kube_role.clone()); - assert_eq!( - role.into_kube(), - kube_role - ); + assert_eq!(role.into_kube(), kube_role); } #[test] -#[verifier(external)] pub fn test_marshal() { - let kube_role = - deps_hack::k8s_openapi::api::rbac::v1::Role { - metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - name: Some("name".to_string()), - namespace: Some("namespace".to_string()), + let kube_role = deps_hack::k8s_openapi::api::rbac::v1::Role { + metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), + namespace: Some("namespace".to_string()), + ..Default::default() + }, + rules: Some(vec![ + deps_hack::k8s_openapi::api::rbac::v1::PolicyRule { + api_groups: Some(vec![ + "api_groups_1_1".to_string(), + "api_groups_1_2".to_string(), + ]), + resources: Some(vec![ + "resources_1_1".to_string(), + "resources_1_2".to_string(), + ]), + verbs: vec!["verbs_1_1".to_string(), "verbs_1_2".to_string()], ..Default::default() }, - rules: Some( - vec![ - deps_hack::k8s_openapi::api::rbac::v1::PolicyRule { - api_groups: Some(vec!["api_groups_1_1".to_string(), "api_groups_1_2".to_string()]), - resources: Some(vec!["resources_1_1".to_string(), "resources_1_2".to_string()]), - verbs: vec!["verbs_1_1".to_string(), "verbs_1_2".to_string()], - ..Default::default() - }, - deps_hack::k8s_openapi::api::rbac::v1::PolicyRule { - api_groups: Some(vec!["api_groups_2_1".to_string(), "api_groups_2_2".to_string()]), - resources: Some(vec!["resources_2_1".to_string(), "resources_2_2".to_string()]), - verbs: vec!["verbs_2_1".to_string(), "verbs_2_2".to_string()], - ..Default::default() - } - ] - ), - ..Default::default() - }; + deps_hack::k8s_openapi::api::rbac::v1::PolicyRule { + api_groups: Some(vec![ + "api_groups_2_1".to_string(), + "api_groups_2_2".to_string(), + ]), + resources: Some(vec![ + "resources_2_1".to_string(), + "resources_2_2".to_string(), + ]), + verbs: vec!["verbs_2_1".to_string(), "verbs_2_2".to_string()], + ..Default::default() + }, + ]), + ..Default::default() + }; let role = Role::from_kube(kube_role.clone()); @@ -219,4 +227,3 @@ pub fn test_marshal() { Role::unmarshal(role.marshal()).unwrap().into_kube() ); } -} diff --git a/src/unit_tests/kubernetes_api_objects/role_binding.rs b/src/unit_tests/kubernetes_api_objects/role_binding.rs index ac64e68e7..b0a4b2880 100644 --- a/src/unit_tests/kubernetes_api_objects/role_binding.rs +++ b/src/unit_tests/kubernetes_api_objects/role_binding.rs @@ -7,17 +7,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for role binding #[test] -#[verifier(external)] pub fn test_default() { let role_binding = RoleBinding::default(); - assert_eq!(role_binding.into_kube(), deps_hack::k8s_openapi::api::rbac::v1::RoleBinding::default()); + assert_eq!( + role_binding.into_kube(), + deps_hack::k8s_openapi::api::rbac::v1::RoleBinding::default() + ); } #[test] -#[verifier(external)] pub fn test_set_metadata() { let mut role_binding = RoleBinding::default(); let mut object_meta = ObjectMeta::default(); @@ -28,7 +27,6 @@ pub fn test_set_metadata() { } #[test] -#[verifier(external)] pub fn test_metadata() { let mut role_binding = RoleBinding::default(); let mut object_meta = ObjectMeta::default(); @@ -39,7 +37,6 @@ pub fn test_metadata() { } #[test] -#[verifier(external)] pub fn test_set_role_ref() { let mut role_binding = RoleBinding::default(); let mut role_ref = RoleRef::default(); @@ -51,7 +48,6 @@ pub fn test_set_role_ref() { } #[test] -#[verifier(external)] pub fn test_set_subjects() { let mut role_binding = RoleBinding::default(); let subject_gen = || { @@ -79,7 +75,6 @@ pub fn test_set_subjects() { } #[test] -#[verifier(external)] pub fn test_clone() { let mut role_binding = RoleBinding::default(); let mut object_meta = ObjectMeta::default(); @@ -111,95 +106,84 @@ pub fn test_clone() { } #[test] -#[verifier(external)] -pub fn test_api_resource(){ +pub fn test_api_resource() { let api_resource = RoleBinding::api_resource(); assert_eq!(api_resource.into_kube().kind, "RoleBinding"); } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_role_binding = - deps_hack::k8s_openapi::api::rbac::v1::RoleBinding { - metadata: - deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - name: Some("name".to_string()), - namespace: Some("namespace".to_string()), - ..Default::default() - }, - role_ref: - deps_hack::k8s_openapi::api::rbac::v1::RoleRef { - api_group: "api_group".to_string(), - kind: "kind".to_string(), - name: "name".to_string(), - ..Default::default() - }, - subjects: Some(vec![ - deps_hack::k8s_openapi::api::rbac::v1::Subject { - kind: "kind1".to_string(), - name: "name1".to_string(), - namespace: Some("namespace1".to_string()), - ..Default::default() - }, - deps_hack::k8s_openapi::api::rbac::v1::Subject { - kind: "kind2".to_string(), - name: "name2".to_string(), - namespace: Some("namespace2".to_string()), - ..Default::default() - }, - ]), + let kube_role_binding = deps_hack::k8s_openapi::api::rbac::v1::RoleBinding { + metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), + namespace: Some("namespace".to_string()), ..Default::default() - }; + }, + role_ref: deps_hack::k8s_openapi::api::rbac::v1::RoleRef { + api_group: "api_group".to_string(), + kind: "kind".to_string(), + name: "name".to_string(), + ..Default::default() + }, + subjects: Some(vec![ + deps_hack::k8s_openapi::api::rbac::v1::Subject { + kind: "kind1".to_string(), + name: "name1".to_string(), + namespace: Some("namespace1".to_string()), + ..Default::default() + }, + deps_hack::k8s_openapi::api::rbac::v1::Subject { + kind: "kind2".to_string(), + name: "name2".to_string(), + namespace: Some("namespace2".to_string()), + ..Default::default() + }, + ]), + ..Default::default() + }; let role_binding = RoleBinding::from_kube(kube_role_binding.clone()); - assert_eq!( - role_binding.into_kube(), - kube_role_binding - ); + assert_eq!(role_binding.into_kube(), kube_role_binding); } #[test] -#[verifier(external)] pub fn test_marshal() { - let kube_role_binding = - deps_hack::k8s_openapi::api::rbac::v1::RoleBinding { - metadata: - deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - name: Some("name".to_string()), - namespace: Some("namespace".to_string()), - ..Default::default() - }, - role_ref: - deps_hack::k8s_openapi::api::rbac::v1::RoleRef { - api_group: "api_group".to_string(), - kind: "kind".to_string(), - name: "name".to_string(), - ..Default::default() - }, - subjects: Some(vec![ - deps_hack::k8s_openapi::api::rbac::v1::Subject { - kind: "kind1".to_string(), - name: "name1".to_string(), - namespace: Some("namespace1".to_string()), - ..Default::default() - }, - deps_hack::k8s_openapi::api::rbac::v1::Subject { - kind: "kind2".to_string(), - name: "name2".to_string(), - namespace: Some("namespace2".to_string()), - ..Default::default() - }, - ]), + let kube_role_binding = deps_hack::k8s_openapi::api::rbac::v1::RoleBinding { + metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), + namespace: Some("namespace".to_string()), + ..Default::default() + }, + role_ref: deps_hack::k8s_openapi::api::rbac::v1::RoleRef { + api_group: "api_group".to_string(), + kind: "kind".to_string(), + name: "name".to_string(), ..Default::default() - }; + }, + subjects: Some(vec![ + deps_hack::k8s_openapi::api::rbac::v1::Subject { + kind: "kind1".to_string(), + name: "name1".to_string(), + namespace: Some("namespace1".to_string()), + ..Default::default() + }, + deps_hack::k8s_openapi::api::rbac::v1::Subject { + kind: "kind2".to_string(), + name: "name2".to_string(), + namespace: Some("namespace2".to_string()), + ..Default::default() + }, + ]), + ..Default::default() + }; let role_binding = RoleBinding::from_kube(kube_role_binding.clone()); assert_eq!( kube_role_binding, - RoleBinding::unmarshal(role_binding.marshal()).unwrap().into_kube() + RoleBinding::unmarshal(role_binding.marshal()) + .unwrap() + .into_kube() ); } -} diff --git a/src/unit_tests/kubernetes_api_objects/role_ref.rs b/src/unit_tests/kubernetes_api_objects/role_ref.rs index 244440ac8..f7dd21cec 100644 --- a/src/unit_tests/kubernetes_api_objects/role_ref.rs +++ b/src/unit_tests/kubernetes_api_objects/role_ref.rs @@ -7,17 +7,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for role ref #[test] -#[verifier(external)] pub fn test_default() { let role_ref = RoleRef::default(); - assert_eq!(role_ref.into_kube(), deps_hack::k8s_openapi::api::rbac::v1::RoleRef::default()); + assert_eq!( + role_ref.into_kube(), + deps_hack::k8s_openapi::api::rbac::v1::RoleRef::default() + ); } #[test] -#[verifier(external)] pub fn test_set_api_group() { let mut role_ref = RoleRef::default(); role_ref.set_api_group("api_group".to_string()); @@ -25,7 +24,6 @@ pub fn test_set_api_group() { } #[test] -#[verifier(external)] pub fn test_set_kind() { let mut role_ref = RoleRef::default(); role_ref.set_kind("kind".to_string()); @@ -33,7 +31,6 @@ pub fn test_set_kind() { } #[test] -#[verifier(external)] pub fn test_set_name() { let mut role_ref = RoleRef::default(); role_ref.set_name("name".to_string()); @@ -41,7 +38,6 @@ pub fn test_set_name() { } #[test] -#[verifier(external)] pub fn test_clone() { let mut role_ref = RoleRef::default(); role_ref.set_api_group("api_group_2".to_string()); @@ -52,9 +48,8 @@ pub fn test_clone() { } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_role_ref = deps_hack::k8s_openapi::api::rbac::v1::RoleRef{ + let kube_role_ref = deps_hack::k8s_openapi::api::rbac::v1::RoleRef { api_group: "api_group".to_string(), kind: "kind".to_string(), name: "name".to_string(), @@ -62,7 +57,5 @@ pub fn test_kube() { let role_ref = RoleRef::from_kube(kube_role_ref.clone()); - assert_eq!(role_ref.into_kube(), - kube_role_ref); -} + assert_eq!(role_ref.into_kube(), kube_role_ref); } diff --git a/src/unit_tests/kubernetes_api_objects/secret.rs b/src/unit_tests/kubernetes_api_objects/secret.rs index 68f159ecd..5fe4648ea 100644 --- a/src/unit_tests/kubernetes_api_objects/secret.rs +++ b/src/unit_tests/kubernetes_api_objects/secret.rs @@ -7,17 +7,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for secret #[test] -#[verifier(external)] pub fn test_default() { let secret = Secret::default(); - assert_eq!(secret.into_kube(), deps_hack::k8s_openapi::api::core::v1::Secret::default()); + assert_eq!( + secret.into_kube(), + deps_hack::k8s_openapi::api::core::v1::Secret::default() + ); } #[test] -#[verifier(external)] pub fn test_set_metadata() { let mut secret = Secret::default(); let mut metadata = ObjectMeta::default(); @@ -28,7 +27,6 @@ pub fn test_set_metadata() { } #[test] -#[verifier(external)] pub fn test_metadata() { let mut secret = Secret::default(); let mut metadata = ObjectMeta::default(); @@ -39,7 +37,6 @@ pub fn test_metadata() { } #[test] -#[verifier(external)] pub fn test_set_data() { let mut secret = Secret::default(); let mut data = StringMap::new(); @@ -53,7 +50,6 @@ pub fn test_set_data() { } #[test] -#[verifier(external)] pub fn test_data() { let mut secret = Secret::default(); let temp = secret.data(); @@ -67,7 +63,6 @@ pub fn test_data() { } #[test] -#[verifier(external)] pub fn test_clone() { let mut secret = Secret::default(); let mut metadata = ObjectMeta::default(); @@ -82,65 +77,50 @@ pub fn test_clone() { } #[test] -#[verifier(external)] pub fn test_api_resource() { let api_resource = Secret::api_resource(); assert_eq!(api_resource.into_kube().kind, "Secret"); } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_secret = - deps_hack::k8s_openapi::api::core::v1::Secret { - metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - name: Some("name".to_string()), - namespace: Some("namespace".to_string()), - ..Default::default() - }, - data: Some( - std::collections::BTreeMap::from_iter(vec![( - "key".to_string(), - deps_hack::k8s_openapi::ByteString("value".to_string().into_bytes()), - )]), - ), + let kube_secret = deps_hack::k8s_openapi::api::core::v1::Secret { + metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), + namespace: Some("namespace".to_string()), ..Default::default() - }; + }, + data: Some(std::collections::BTreeMap::from_iter(vec![( + "key".to_string(), + deps_hack::k8s_openapi::ByteString("value".to_string().into_bytes()), + )])), + ..Default::default() + }; let secret = Secret::from_kube(kube_secret.clone()); - assert_eq!( - secret.into_kube(), - kube_secret - ); + assert_eq!(secret.into_kube(), kube_secret); } #[test] -#[verifier(external)] pub fn test_marshal() { - let kube_secret = - deps_hack::k8s_openapi::api::core::v1::Secret { - metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - name: Some("name".to_string()), - namespace: Some("namespace".to_string()), - ..Default::default() - }, - data: Some( - std::collections::BTreeMap::from_iter(vec![( - "key".to_string(), - deps_hack::k8s_openapi::ByteString("value".to_string().into_bytes()), - )]), - ), + let kube_secret = deps_hack::k8s_openapi::api::core::v1::Secret { + metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), + namespace: Some("namespace".to_string()), ..Default::default() - }; + }, + data: Some(std::collections::BTreeMap::from_iter(vec![( + "key".to_string(), + deps_hack::k8s_openapi::ByteString("value".to_string().into_bytes()), + )])), + ..Default::default() + }; let secret = Secret::from_kube(kube_secret.clone()); assert_eq!( kube_secret, - Secret::unmarshal(secret.marshal()) - .unwrap() - .into_kube() + Secret::unmarshal(secret.marshal()).unwrap().into_kube() ); } -} diff --git a/src/unit_tests/kubernetes_api_objects/secret_projection.rs b/src/unit_tests/kubernetes_api_objects/secret_projection.rs index 14f54151b..3d10397ad 100644 --- a/src/unit_tests/kubernetes_api_objects/secret_projection.rs +++ b/src/unit_tests/kubernetes_api_objects/secret_projection.rs @@ -9,25 +9,26 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for scret projection #[test] -#[verifier(external)] pub fn test_default() { let secret_projection = SecretProjection::default(); - assert_eq!(secret_projection.into_kube(), deps_hack::k8s_openapi::api::core::v1::SecretProjection::default()); + assert_eq!( + secret_projection.into_kube(), + deps_hack::k8s_openapi::api::core::v1::SecretProjection::default() + ); } #[test] -#[verifier(external)] pub fn test_set_name() { let mut secret_projection = SecretProjection::default(); secret_projection.set_name("name".to_string()); - assert_eq!("name".to_string(), secret_projection.into_kube().name.unwrap()); + assert_eq!( + "name".to_string(), + secret_projection.into_kube().name.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_items() { let mut secret_projection = SecretProjection::default(); let key_to_paths_gen = || { @@ -53,35 +54,30 @@ pub fn test_set_items() { } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_secret_projection = deps_hack::k8s_openapi::api::core::v1::SecretProjection{ + let kube_secret_projection = deps_hack::k8s_openapi::api::core::v1::SecretProjection { name: Some("name".to_string()), items: Some(vec![ - deps_hack::k8s_openapi::api::core::v1::KeyToPath{ + deps_hack::k8s_openapi::api::core::v1::KeyToPath { key: "key1".to_string(), path: "path1".to_string(), ..Default::default() }, - deps_hack::k8s_openapi::api::core::v1::KeyToPath{ + deps_hack::k8s_openapi::api::core::v1::KeyToPath { key: "key2".to_string(), path: "path2".to_string(), ..Default::default() - } + }, ]), ..Default::default() }; let secret_projection = SecretProjection::from_kube(kube_secret_projection.clone()); - assert_eq!( - secret_projection.into_kube(), - kube_secret_projection - ); + assert_eq!(secret_projection.into_kube(), kube_secret_projection); } #[test] -#[verifier(external)] pub fn test_clone() { let mut secret_projection = SecretProjection::default(); let key_to_paths_gen = || { @@ -98,7 +94,8 @@ pub fn test_clone() { }; secret_projection.set_items(key_to_paths_gen()); let secret_projection_clone = secret_projection.clone(); - assert_eq!(secret_projection.into_kube(), secret_projection_clone.into_kube()); - -} + assert_eq!( + secret_projection.into_kube(), + secret_projection_clone.into_kube() + ); } diff --git a/src/unit_tests/kubernetes_api_objects/secret_volume_source.rs b/src/unit_tests/kubernetes_api_objects/secret_volume_source.rs index 8ec6831bc..26a8baa37 100644 --- a/src/unit_tests/kubernetes_api_objects/secret_volume_source.rs +++ b/src/unit_tests/kubernetes_api_objects/secret_volume_source.rs @@ -9,46 +9,44 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for secret volume source #[test] -#[verifier(external)] pub fn test_default() { let secret_volume_source = SecretVolumeSource::default(); - assert_eq!(secret_volume_source.into_kube(), deps_hack::k8s_openapi::api::core::v1::SecretVolumeSource::default()); + assert_eq!( + secret_volume_source.into_kube(), + deps_hack::k8s_openapi::api::core::v1::SecretVolumeSource::default() + ); } #[test] -#[verifier(external)] pub fn test_set_secret_name() { let mut secret_volume_source = SecretVolumeSource::default(); secret_volume_source.set_secret_name("secret_name".to_string()); - assert_eq!("secret_name".to_string(), secret_volume_source.into_kube().secret_name.unwrap()); + assert_eq!( + "secret_name".to_string(), + secret_volume_source.into_kube().secret_name.unwrap() + ); } #[test] -#[verifier(external)] -pub fn test_clone(){ +pub fn test_clone() { let mut secret_volume_source = SecretVolumeSource::default(); secret_volume_source.set_secret_name("secret_name".to_string()); let secret_volume_source_clone = secret_volume_source.clone(); - assert_eq!(secret_volume_source.into_kube(), secret_volume_source_clone.into_kube()); + assert_eq!( + secret_volume_source.into_kube(), + secret_volume_source_clone.into_kube() + ); } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_secret_volume_source = - deps_hack::k8s_openapi::api::core::v1::SecretVolumeSource{ - secret_name: Some("secret_name".to_string()), - ..Default::default() - }; + let kube_secret_volume_source = deps_hack::k8s_openapi::api::core::v1::SecretVolumeSource { + secret_name: Some("secret_name".to_string()), + ..Default::default() + }; let secret_volume_source = SecretVolumeSource::from_kube(kube_secret_volume_source.clone()); - assert_eq!( - secret_volume_source.into_kube(), - kube_secret_volume_source - ); -} + assert_eq!(secret_volume_source.into_kube(), kube_secret_volume_source); } diff --git a/src/unit_tests/kubernetes_api_objects/security_context.rs b/src/unit_tests/kubernetes_api_objects/security_context.rs index 739ed920f..45389414f 100644 --- a/src/unit_tests/kubernetes_api_objects/security_context.rs +++ b/src/unit_tests/kubernetes_api_objects/security_context.rs @@ -8,11 +8,8 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for SecurityContext #[test] -#[verifier(external)] -pub fn test_kube(){ +pub fn test_kube() { let kube_security_context = deps_hack::k8s_openapi::api::core::v1::SecurityContext { privileged: Some(true), ..Default::default() @@ -20,7 +17,5 @@ pub fn test_kube(){ let security_context = SecurityContext::from_kube(kube_security_context.clone()); - assert_eq!(security_context.into_kube(), - kube_security_context); -} + assert_eq!(security_context.into_kube(), kube_security_context); } diff --git a/src/unit_tests/kubernetes_api_objects/service.rs b/src/unit_tests/kubernetes_api_objects/service.rs index 4ce83dc3b..9650c333a 100644 --- a/src/unit_tests/kubernetes_api_objects/service.rs +++ b/src/unit_tests/kubernetes_api_objects/service.rs @@ -7,17 +7,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for service #[test] -#[verifier(external)] pub fn test_default() { let service = Service::default(); - assert_eq!(service.into_kube(), deps_hack::k8s_openapi::api::core::v1::Service::default()); + assert_eq!( + service.into_kube(), + deps_hack::k8s_openapi::api::core::v1::Service::default() + ); } #[test] -#[verifier(external)] pub fn test_set_metadata() { let mut service = Service::default(); let mut metadata = ObjectMeta::default(); @@ -27,7 +26,6 @@ pub fn test_set_metadata() { } #[test] -#[verifier(external)] pub fn test_metadata() { let mut service = Service::default(); let mut metadata = ObjectMeta::default(); @@ -37,7 +35,6 @@ pub fn test_metadata() { } #[test] -#[verifier(external)] pub fn test_set_spec() { let mut service = Service::default(); let mut spec = ServiceSpec::default(); @@ -47,7 +44,6 @@ pub fn test_set_spec() { } #[test] -#[verifier(external)] pub fn test_spec() { let mut service = Service::default(); let mut spec = ServiceSpec::default(); @@ -59,14 +55,12 @@ pub fn test_spec() { } #[test] -#[verifier(external)] pub fn test_api_resource() { let api_resource = Service::api_resource(); assert_eq!(api_resource.into_kube().kind, "Service"); } #[test] -#[verifier(external)] pub fn test_clone() { let mut service = Service::default(); let mut metadata = ObjectMeta::default(); @@ -80,48 +74,42 @@ pub fn test_clone() { } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_service = - deps_hack::k8s_openapi::api::core::v1::Service { - metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - name: Some("name".to_string()), - ..Default::default() - }, - spec: Some(deps_hack::k8s_openapi::api::core::v1::ServiceSpec { - cluster_ip: Some("ip".to_string()), - ..Default::default() - }), + let kube_service = deps_hack::k8s_openapi::api::core::v1::Service { + metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), ..Default::default() - }; + }, + spec: Some(deps_hack::k8s_openapi::api::core::v1::ServiceSpec { + cluster_ip: Some("ip".to_string()), + ..Default::default() + }), + ..Default::default() + }; let service = Service::from_kube(kube_service.clone()); - assert_eq!(service.into_kube(), - kube_service); + assert_eq!(service.into_kube(), kube_service); } #[test] -#[verifier(external)] pub fn test_marshal() { - let kube_service = - deps_hack::k8s_openapi::api::core::v1::Service { - metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - name: Some("name".to_string()), - ..Default::default() - }, - spec: Some(deps_hack::k8s_openapi::api::core::v1::ServiceSpec { - cluster_ip: Some("ip".to_string()), - ..Default::default() - }), + let kube_service = deps_hack::k8s_openapi::api::core::v1::Service { + metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), + ..Default::default() + }, + spec: Some(deps_hack::k8s_openapi::api::core::v1::ServiceSpec { + cluster_ip: Some("ip".to_string()), ..Default::default() - }; + }), + ..Default::default() + }; let service = Service::from_kube(kube_service.clone()); - assert_eq!(kube_service, - Service::unmarshal(service.marshal()) - .unwrap() - .into_kube()); -} + assert_eq!( + kube_service, + Service::unmarshal(service.marshal()).unwrap().into_kube() + ); } diff --git a/src/unit_tests/kubernetes_api_objects/service_account.rs b/src/unit_tests/kubernetes_api_objects/service_account.rs index 6e873c777..9ba5d7bfa 100644 --- a/src/unit_tests/kubernetes_api_objects/service_account.rs +++ b/src/unit_tests/kubernetes_api_objects/service_account.rs @@ -7,17 +7,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for service account #[test] -#[verifier(external)] pub fn test_default() { let service_account = ServiceAccount::default(); - assert_eq!(service_account.into_kube(), deps_hack::k8s_openapi::api::core::v1::ServiceAccount::default()); + assert_eq!( + service_account.into_kube(), + deps_hack::k8s_openapi::api::core::v1::ServiceAccount::default() + ); } #[test] -#[verifier(external)] pub fn test_set_metadata() { let mut service_account = ServiceAccount::default(); let mut metadata = ObjectMeta::default(); @@ -27,7 +26,6 @@ pub fn test_set_metadata() { } #[test] -#[verifier(external)] pub fn test_metadata() { let mut service_account = ServiceAccount::default(); let mut metadata = ObjectMeta::default(); @@ -37,25 +35,25 @@ pub fn test_metadata() { } #[test] -#[verifier(external)] pub fn test_api_resource() { let api_resource = ServiceAccount::api_resource(); assert_eq!(api_resource.into_kube().kind, "ServiceAccount"); } #[test] -#[verifier(external)] pub fn test_clone() { let mut service_account = ServiceAccount::default(); let mut metadata = ObjectMeta::default(); metadata.set_name("name".to_string()); service_account.set_metadata(metadata.clone()); let service_account_clone = service_account.clone(); - assert_eq!(service_account.into_kube(), service_account_clone.into_kube()); + assert_eq!( + service_account.into_kube(), + service_account_clone.into_kube() + ); } #[test] -#[verifier(external)] pub fn test_kube() { let kube_service_account = deps_hack::k8s_openapi::api::core::v1::ServiceAccount { metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { @@ -67,14 +65,10 @@ pub fn test_kube() { let service_account = ServiceAccount::from_kube(kube_service_account.clone()); - assert_eq!( - service_account.into_kube(), - kube_service_account - ); + assert_eq!(service_account.into_kube(), kube_service_account); } #[test] -#[verifier(external)] pub fn test_marshal() { let kube_service_account = deps_hack::k8s_openapi::api::core::v1::ServiceAccount { metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { @@ -93,5 +87,3 @@ pub fn test_marshal() { .into_kube() ); } - -} diff --git a/src/unit_tests/kubernetes_api_objects/service_port.rs b/src/unit_tests/kubernetes_api_objects/service_port.rs index c7b96e184..3e706829f 100644 --- a/src/unit_tests/kubernetes_api_objects/service_port.rs +++ b/src/unit_tests/kubernetes_api_objects/service_port.rs @@ -7,17 +7,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for service port #[test] -#[verifier(external)] pub fn test_default() { let service_port = ServicePort::default(); - assert_eq!(service_port.into_kube(), deps_hack::k8s_openapi::api::core::v1::ServicePort::default()); + assert_eq!( + service_port.into_kube(), + deps_hack::k8s_openapi::api::core::v1::ServicePort::default() + ); } #[test] -#[verifier(external)] pub fn test_set_name() { let mut service_port = ServicePort::default(); service_port.set_name("name".to_string()); @@ -25,7 +24,6 @@ pub fn test_set_name() { } #[test] -#[verifier(external)] pub fn test_set_port() { let mut service_port = ServicePort::default(); service_port.set_port(1); @@ -36,23 +34,26 @@ pub fn test_set_port() { } #[test] -#[verifier(external)] pub fn test_set_app_protocol() { let mut service_port = ServicePort::default(); service_port.set_app_protocol("protocol".to_string()); - assert_eq!("protocol".to_string(), service_port.into_kube().app_protocol.unwrap()); + assert_eq!( + "protocol".to_string(), + service_port.into_kube().app_protocol.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_protocaol() { let mut service_port = ServicePort::default(); service_port.set_protocol("protocol".to_string()); - assert_eq!("protocol".to_string(), service_port.into_kube().protocol.unwrap()); + assert_eq!( + "protocol".to_string(), + service_port.into_kube().protocol.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_kube() { let kube_service_port = deps_hack::k8s_openapi::api::core::v1::ServicePort { name: Some("name".to_string()), @@ -63,9 +64,5 @@ pub fn test_kube() { let service_port = ServicePort::from_kube(kube_service_port.clone()); - assert_eq!( - service_port.into_kube(), - kube_service_port - ); -} + assert_eq!(service_port.into_kube(), kube_service_port); } diff --git a/src/unit_tests/kubernetes_api_objects/service_spec.rs b/src/unit_tests/kubernetes_api_objects/service_spec.rs index b717ad35d..e40250f9b 100644 --- a/src/unit_tests/kubernetes_api_objects/service_spec.rs +++ b/src/unit_tests/kubernetes_api_objects/service_spec.rs @@ -7,25 +7,26 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for service spec #[test] -#[verifier(external)] pub fn test_default() { let service_spec = ServiceSpec::default(); - assert_eq!(service_spec.into_kube(), deps_hack::k8s_openapi::api::core::v1::ServiceSpec::default()); + assert_eq!( + service_spec.into_kube(), + deps_hack::k8s_openapi::api::core::v1::ServiceSpec::default() + ); } #[test] -#[verifier(external)] pub fn test_set_cluster_ip() { let mut service_spec = ServiceSpec::default(); service_spec.set_cluster_ip("ip".to_string()); - assert_eq!("ip".to_string(), service_spec.into_kube().cluster_ip.unwrap()); + assert_eq!( + "ip".to_string(), + service_spec.into_kube().cluster_ip.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_ports() { let mut service_spec = ServiceSpec::default(); let ports_gen = || { @@ -40,15 +41,16 @@ pub fn test_set_ports() { ports }; service_spec.set_ports(ports_gen()); - assert_eq!(ports_gen() - .into_iter() - .map(|p: ServicePort| p - .into_kube()).collect::>(), - service_spec.into_kube().ports.unwrap()); + assert_eq!( + ports_gen() + .into_iter() + .map(|p: ServicePort| p.into_kube()) + .collect::>(), + service_spec.into_kube().ports.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_ports() { let mut service_spec = ServiceSpec::default(); let ports_gen = || { @@ -63,51 +65,68 @@ pub fn test_ports() { ports }; service_spec.set_ports(ports_gen()); - assert_eq!(ports_gen() - .into_iter() - .map(|p: ServicePort| p.into_kube()) - .collect::>(), - service_spec.ports().unwrap() - .into_iter() - .map(|p: ServicePort| p.into_kube()) - .collect::>() - ); + assert_eq!( + ports_gen() + .into_iter() + .map(|p: ServicePort| p.into_kube()) + .collect::>(), + service_spec + .ports() + .unwrap() + .into_iter() + .map(|p: ServicePort| p.into_kube()) + .collect::>() + ); } #[test] -#[verifier(external)] pub fn test_set_selector() { let mut service_spec = ServiceSpec::default(); let mut selector = StringMap::new(); selector.insert("key".to_string(), "value".to_string()); service_spec.set_selector(selector.clone()); - assert_eq!(selector.into_rust_map(), service_spec.into_kube().selector.unwrap()); + assert_eq!( + selector.into_rust_map(), + service_spec.into_kube().selector.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_selector() { let mut service_spec = ServiceSpec::default(); let mut selector = StringMap::new(); selector.insert("key".to_string(), "value".to_string()); service_spec.set_selector(selector.clone()); - assert_eq!(selector.into_rust_map(), service_spec.selector().unwrap().into_rust_map()); + assert_eq!( + selector.into_rust_map(), + service_spec.selector().unwrap().into_rust_map() + ); } #[test] -#[verifier(external)] pub fn test_set_publish_not_ready_addresses() { let mut service_spec = ServiceSpec::default(); service_spec.set_publish_not_ready_addresses(true); - assert_eq!(true, service_spec.into_kube().publish_not_ready_addresses.unwrap()); + assert_eq!( + true, + service_spec + .into_kube() + .publish_not_ready_addresses + .unwrap() + ); let mut service_spec_2 = ServiceSpec::default(); service_spec_2.set_publish_not_ready_addresses(false); - assert_eq!(false, service_spec_2.into_kube().publish_not_ready_addresses.unwrap()); + assert_eq!( + false, + service_spec_2 + .into_kube() + .publish_not_ready_addresses + .unwrap() + ); } #[test] -#[verifier(external)] pub fn test_unset_publish_not_ready_addresses() { let mut service_spec = ServiceSpec::default(); service_spec.set_publish_not_ready_addresses(true); @@ -115,9 +134,7 @@ pub fn test_unset_publish_not_ready_addresses() { assert_eq!(None, service_spec.into_kube().publish_not_ready_addresses); } - #[test] -#[verifier(external)] pub fn test_publish_not_ready_addresses() { let mut service_spec = ServiceSpec::default(); assert_eq!(None, service_spec.publish_not_ready_addresses()); @@ -130,7 +147,6 @@ pub fn test_publish_not_ready_addresses() { } #[test] -#[verifier(external)] pub fn test_clone() { let mut service_spec = ServiceSpec::default(); service_spec.set_cluster_ip("ip".to_string()); @@ -151,45 +167,35 @@ pub fn test_clone() { service_spec.set_selector(selector.clone()); service_spec.set_publish_not_ready_addresses(true); let cloned_service_spec = service_spec.clone(); - assert_eq!( - service_spec.into_kube(), - cloned_service_spec.into_kube() - ); + assert_eq!(service_spec.into_kube(), cloned_service_spec.into_kube()); } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_service_spec = - deps_hack::k8s_openapi::api::core::v1::ServiceSpec { - cluster_ip: Some("ip".to_string()), - ports: Some(vec![ - deps_hack::k8s_openapi::api::core::v1::ServicePort { - port: 1, - app_protocol: Some("http".to_string()), - ..Default::default() - }, - deps_hack::k8s_openapi::api::core::v1::ServicePort { - port: 2048, - app_protocol: Some("tcp".to_string()), - ..Default::default() - }, - ]), - selector: Some( - vec![ - ("key".to_string(), "value".to_string()) - ].into_iter().collect() - ), - publish_not_ready_addresses: Some(true), - ..Default::default() - }; + let kube_service_spec = deps_hack::k8s_openapi::api::core::v1::ServiceSpec { + cluster_ip: Some("ip".to_string()), + ports: Some(vec![ + deps_hack::k8s_openapi::api::core::v1::ServicePort { + port: 1, + app_protocol: Some("http".to_string()), + ..Default::default() + }, + deps_hack::k8s_openapi::api::core::v1::ServicePort { + port: 2048, + app_protocol: Some("tcp".to_string()), + ..Default::default() + }, + ]), + selector: Some( + vec![("key".to_string(), "value".to_string())] + .into_iter() + .collect(), + ), + publish_not_ready_addresses: Some(true), + ..Default::default() + }; let service_spec = ServiceSpec::from_kube(kube_service_spec.clone()); - assert_eq!( - service_spec.into_kube(), - kube_service_spec - ); -} - + assert_eq!(service_spec.into_kube(), kube_service_spec); } diff --git a/src/unit_tests/kubernetes_api_objects/stateful_set.rs b/src/unit_tests/kubernetes_api_objects/stateful_set.rs index 7126c9fb1..7ca670fca 100644 --- a/src/unit_tests/kubernetes_api_objects/stateful_set.rs +++ b/src/unit_tests/kubernetes_api_objects/stateful_set.rs @@ -8,10 +8,7 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for stateful set #[test] -#[verifier(external)] pub fn test_default() { let stateful_set = StatefulSet::default(); assert_eq!( @@ -21,7 +18,6 @@ pub fn test_default() { } #[test] -#[verifier(external)] pub fn test_set_metadata() { let mut object_meta = ObjectMeta::default(); object_meta.set_name("name".to_string()); @@ -32,7 +28,6 @@ pub fn test_set_metadata() { } #[test] -#[verifier(external)] pub fn test_metadata() { let mut object_meta = ObjectMeta::default(); object_meta.set_name("name".to_string()); @@ -43,17 +38,18 @@ pub fn test_metadata() { } #[test] -#[verifier(external)] pub fn test_set_spec() { let mut stateful_set_spec = StatefulSetSpec::default(); stateful_set_spec.set_replicas(1); let mut stateful_set = StatefulSet::default(); stateful_set.set_spec(stateful_set_spec.clone()); - assert_eq!(stateful_set_spec.into_kube(), stateful_set.into_kube().spec.unwrap()); + assert_eq!( + stateful_set_spec.into_kube(), + stateful_set.into_kube().spec.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_spec() { let mut stateful_set_spec = StatefulSetSpec::default(); stateful_set_spec.set_replicas(1024); @@ -63,18 +59,19 @@ pub fn test_spec() { panic!("StatefulSet spec should be None, but it's not."); } stateful_set.set_spec(stateful_set_spec.clone()); - assert_eq!(stateful_set_spec.into_kube(), stateful_set.spec().unwrap().into_kube()); + assert_eq!( + stateful_set_spec.into_kube(), + stateful_set.spec().unwrap().into_kube() + ); } #[test] -#[verifier(external)] pub fn test_api_resource() { let api_resource = StatefulSet::api_resource(); assert_eq!(api_resource.into_kube().kind, "StatefulSet"); } #[test] -#[verifier(external)] pub fn test_clone() { let mut object_meta = ObjectMeta::default(); object_meta.set_name("name".to_string()); @@ -85,25 +82,22 @@ pub fn test_clone() { stateful_set_spec.set_replicas(1024); stateful_set.set_spec(stateful_set_spec.clone()); let cloned_stateful_set = stateful_set.clone(); - assert_eq!( - stateful_set.into_kube(), - cloned_stateful_set.into_kube() - ); + assert_eq!(stateful_set.into_kube(), cloned_stateful_set.into_kube()); } #[test] -#[verifier(external)] pub fn test_status() { let stateful_set = StatefulSet::default(); let temp = stateful_set.status(); if !temp.is_none() { panic!("StatefulSet status should be None, but it's not."); } - let stateful_set_status = StatefulSetStatus::from_kube(deps_hack::k8s_openapi::api::apps::v1::StatefulSetStatus { - replicas: 1024, - ready_replicas: Some(1024), - ..Default::default() - }); + let stateful_set_status = + StatefulSetStatus::from_kube(deps_hack::k8s_openapi::api::apps::v1::StatefulSetStatus { + replicas: 1024, + ready_replicas: Some(1024), + ..Default::default() + }); let stateful_set = StatefulSet::from_kube(deps_hack::k8s_openapi::api::apps::v1::StatefulSet { status: Some(deps_hack::k8s_openapi::api::apps::v1::StatefulSetStatus { replicas: 1024, @@ -112,99 +106,97 @@ pub fn test_status() { }), ..Default::default() }); - assert_eq!(stateful_set_status.into_kube(), stateful_set.status().unwrap().into_kube()); + assert_eq!( + stateful_set_status.into_kube(), + stateful_set.status().unwrap().into_kube() + ); } #[test] -#[verifier(external)] pub fn test_kube() { - let kube_stateful_set = - deps_hack::k8s_openapi::api::apps::v1::StatefulSet { - metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - name: Some("name".to_string()), - namespace: Some("namespace".to_string()), + let kube_stateful_set = deps_hack::k8s_openapi::api::apps::v1::StatefulSet { + metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), + namespace: Some("namespace".to_string()), + ..Default::default() + }, + spec: Some(deps_hack::k8s_openapi::api::apps::v1::StatefulSetSpec { + replicas: Some(1), + selector: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::LabelSelector { + match_labels: Some( + vec![("key".to_string(), "value".to_string())] + .into_iter() + .collect(), + ), ..Default::default() }, - spec: Some(deps_hack::k8s_openapi::api::apps::v1::StatefulSetSpec { - replicas: Some(1), - selector: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::LabelSelector { - match_labels: Some(vec![( - "key".to_string(), - "value".to_string(), - )].into_iter().collect()), - ..Default::default() - }, - template: deps_hack::k8s_openapi::api::core::v1::PodTemplateSpec { - metadata: Some(deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + template: deps_hack::k8s_openapi::api::core::v1::PodTemplateSpec { + metadata: Some( + deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { name: Some("name".to_string()), namespace: Some("namespace".to_string()), ..Default::default() - }), - spec: Some(deps_hack::k8s_openapi::api::core::v1::PodSpec { - containers: vec![ - deps_hack::k8s_openapi::api::core::v1::Container { - name: "name".to_string(), - image: Some("image".to_string()), - ..Default::default() - }, - ], + }, + ), + spec: Some(deps_hack::k8s_openapi::api::core::v1::PodSpec { + containers: vec![deps_hack::k8s_openapi::api::core::v1::Container { + name: "name".to_string(), + image: Some("image".to_string()), ..Default::default() - }), + }], ..Default::default() - }, + }), ..Default::default() - }), + }, ..Default::default() - }; + }), + ..Default::default() + }; let stateful_set = StatefulSet::from_kube(kube_stateful_set.clone()); - assert_eq!( - stateful_set.into_kube(), - kube_stateful_set - ); + assert_eq!(stateful_set.into_kube(), kube_stateful_set); } -#[verifier(external)] pub fn test_marshal() { - let kube_stateful_set = - deps_hack::k8s_openapi::api::apps::v1::StatefulSet { - metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { - name: Some("name".to_string()), - namespace: Some("namespace".to_string()), + let kube_stateful_set = deps_hack::k8s_openapi::api::apps::v1::StatefulSet { + metadata: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + name: Some("name".to_string()), + namespace: Some("namespace".to_string()), + ..Default::default() + }, + spec: Some(deps_hack::k8s_openapi::api::apps::v1::StatefulSetSpec { + replicas: Some(1), + selector: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::LabelSelector { + match_labels: Some( + vec![("key".to_string(), "value".to_string())] + .into_iter() + .collect(), + ), ..Default::default() }, - spec: Some(deps_hack::k8s_openapi::api::apps::v1::StatefulSetSpec { - replicas: Some(1), - selector: deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::LabelSelector { - match_labels: Some(vec![( - "key".to_string(), - "value".to_string(), - )].into_iter().collect()), - ..Default::default() - }, - template: deps_hack::k8s_openapi::api::core::v1::PodTemplateSpec { - metadata: Some(deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { + template: deps_hack::k8s_openapi::api::core::v1::PodTemplateSpec { + metadata: Some( + deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::ObjectMeta { name: Some("name".to_string()), namespace: Some("namespace".to_string()), ..Default::default() - }), - spec: Some(deps_hack::k8s_openapi::api::core::v1::PodSpec { - containers: vec![ - deps_hack::k8s_openapi::api::core::v1::Container { - name: "name".to_string(), - image: Some("image".to_string()), - ..Default::default() - }, - ], + }, + ), + spec: Some(deps_hack::k8s_openapi::api::core::v1::PodSpec { + containers: vec![deps_hack::k8s_openapi::api::core::v1::Container { + name: "name".to_string(), + image: Some("image".to_string()), ..Default::default() - }), + }], ..Default::default() - }, + }), ..Default::default() - }), + }, ..Default::default() - }; + }), + ..Default::default() + }; let stateful_set = StatefulSet::from_kube(kube_stateful_set.clone()); @@ -215,4 +207,3 @@ pub fn test_marshal() { .into_kube() ); } -} diff --git a/src/unit_tests/kubernetes_api_objects/stateful_set_persistent_volume_claim_retention_policy.rs b/src/unit_tests/kubernetes_api_objects/stateful_set_persistent_volume_claim_retention_policy.rs index 2d49fc76b..7fcaf3fbb 100644 --- a/src/unit_tests/kubernetes_api_objects/stateful_set_persistent_volume_claim_retention_policy.rs +++ b/src/unit_tests/kubernetes_api_objects/stateful_set_persistent_volume_claim_retention_policy.rs @@ -8,12 +8,10 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for stateful set pvc retention policy #[test] -#[verifier(external)] pub fn test_default() { - let stateful_set_pvc_retention_policy = StatefulSetPersistentVolumeClaimRetentionPolicy::default(); + let stateful_set_pvc_retention_policy = + StatefulSetPersistentVolumeClaimRetentionPolicy::default(); assert_eq!( stateful_set_pvc_retention_policy.into_kube(), deps_hack::k8s_openapi::api::apps::v1::StatefulSetPersistentVolumeClaimRetentionPolicy::default() @@ -21,31 +19,37 @@ pub fn test_default() { } #[test] -#[verifier(external)] pub fn test_set_when_deleted() { - let mut stateful_set_pvc_retention_policy = StatefulSetPersistentVolumeClaimRetentionPolicy::default(); + let mut stateful_set_pvc_retention_policy = + StatefulSetPersistentVolumeClaimRetentionPolicy::default(); stateful_set_pvc_retention_policy.set_when_deleted("Retain".to_string()); assert_eq!( "Retain".to_string(), - stateful_set_pvc_retention_policy.into_kube().when_deleted.unwrap() + stateful_set_pvc_retention_policy + .into_kube() + .when_deleted + .unwrap() ); } #[test] -#[verifier(external)] pub fn test_set_when_scaled() { - let mut stateful_set_pvc_retention_policy = StatefulSetPersistentVolumeClaimRetentionPolicy::default(); + let mut stateful_set_pvc_retention_policy = + StatefulSetPersistentVolumeClaimRetentionPolicy::default(); stateful_set_pvc_retention_policy.set_when_scaled("Delete".to_string()); assert_eq!( "Delete".to_string(), - stateful_set_pvc_retention_policy.into_kube().when_scaled.unwrap() + stateful_set_pvc_retention_policy + .into_kube() + .when_scaled + .unwrap() ); } #[test] -#[verifier(external)] pub fn test_clone() { - let mut stateful_set_pvc_retention_policy = StatefulSetPersistentVolumeClaimRetentionPolicy::default(); + let mut stateful_set_pvc_retention_policy = + StatefulSetPersistentVolumeClaimRetentionPolicy::default(); stateful_set_pvc_retention_policy.set_when_deleted("Retain".to_string()); stateful_set_pvc_retention_policy.set_when_scaled("Delete".to_string()); let cloned_stateful_set_pvc_retention_policy = stateful_set_pvc_retention_policy.clone(); @@ -56,20 +60,21 @@ pub fn test_clone() { } #[test] -#[verifier(external)] pub fn test_kube() { let kube_stateful_set_pvc_retention_policy = - deps_hack::k8s_openapi::api::apps::v1::StatefulSetPersistentVolumeClaimRetentionPolicy{ + deps_hack::k8s_openapi::api::apps::v1::StatefulSetPersistentVolumeClaimRetentionPolicy { when_deleted: Some("Retain".to_string()), when_scaled: Some("Delete".to_string()), ..Default::default() }; - let stateful_set_pvc_retention_policy = StatefulSetPersistentVolumeClaimRetentionPolicy::from_kube(kube_stateful_set_pvc_retention_policy.clone()); + let stateful_set_pvc_retention_policy = + StatefulSetPersistentVolumeClaimRetentionPolicy::from_kube( + kube_stateful_set_pvc_retention_policy.clone(), + ); assert_eq!( stateful_set_pvc_retention_policy.into_kube(), kube_stateful_set_pvc_retention_policy ); } -} diff --git a/src/unit_tests/kubernetes_api_objects/stateful_set_spec.rs b/src/unit_tests/kubernetes_api_objects/stateful_set_spec.rs index 8f2461073..c55aa4885 100644 --- a/src/unit_tests/kubernetes_api_objects/stateful_set_spec.rs +++ b/src/unit_tests/kubernetes_api_objects/stateful_set_spec.rs @@ -8,10 +8,7 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for stateful set spec #[test] -#[verifier(external)] pub fn test_default() { let stateful_set_spec = StatefulSetSpec::default(); assert_eq!( @@ -21,7 +18,6 @@ pub fn test_default() { } #[test] -#[verifier(external)] pub fn test_set_replicas() { let mut stateful_set_spec = StatefulSetSpec::default(); stateful_set_spec.set_replicas(1); @@ -29,7 +25,6 @@ pub fn test_set_replicas() { } #[test] -#[verifier(external)] pub fn test_set_selector() { let mut stateful_set_spec = StatefulSetSpec::default(); let mut label_selector = LabelSelector::default(); @@ -44,7 +39,6 @@ pub fn test_set_selector() { } #[test] -#[verifier(external)] pub fn test_set_service_name() { let mut stateful_set_spec = StatefulSetSpec::default(); stateful_set_spec.set_service_name("name".to_string()); @@ -55,7 +49,6 @@ pub fn test_set_service_name() { } #[test] -#[verifier(external)] pub fn test_set_template() { let mut stateful_set_spec = StatefulSetSpec::default(); let mut pod_template_spec = PodTemplateSpec::default(); @@ -70,7 +63,6 @@ pub fn test_set_template() { } #[test] -#[verifier(external)] pub fn test_set_volume_claim_templates() { let mut stateful_set_spec = StatefulSetSpec::default(); let volume_claim_templates_gen = || { @@ -96,7 +88,6 @@ pub fn test_set_volume_claim_templates() { } #[test] -#[verifier(external)] pub fn test_set_pod_management_policy() { let mut stateful_set_spec = StatefulSetSpec::default(); stateful_set_spec.set_pod_management_policy("policy".to_string()); @@ -107,7 +98,6 @@ pub fn test_set_pod_management_policy() { } #[test] -#[verifier(external)] pub fn test_set_pvc_retention_policy() { let mut stateful_set_spec = StatefulSetSpec::default(); let mut pvc_retention_policy = StatefulSetPersistentVolumeClaimRetentionPolicy::default(); @@ -116,12 +106,14 @@ pub fn test_set_pvc_retention_policy() { stateful_set_spec.set_pvc_retention_policy(pvc_retention_policy.clone()); assert_eq!( pvc_retention_policy.into_kube(), - stateful_set_spec.into_kube().persistent_volume_claim_retention_policy.unwrap() + stateful_set_spec + .into_kube() + .persistent_volume_claim_retention_policy + .unwrap() ); } #[test] -#[verifier(external)] pub fn test_replicas() { let mut stateful_set_spec = StatefulSetSpec::default(); let temp = stateful_set_spec.replicas(); @@ -133,7 +125,6 @@ pub fn test_replicas() { } #[test] -#[verifier(external)] pub fn test_template() { let mut stateful_set_spec = StatefulSetSpec::default(); let mut pod_template_spec = PodTemplateSpec::default(); @@ -148,12 +139,13 @@ pub fn test_template() { } #[test] -#[verifier(external)] pub fn test_persistent_volume_claim_retention_policy() { let mut stateful_set_spec = StatefulSetSpec::default(); let temp = stateful_set_spec.persistent_volume_claim_retention_policy(); if !temp.is_none() { - panic!("StatefulSet persistent_volume_claim_retention_policy should be None, but it's not."); + panic!( + "StatefulSet persistent_volume_claim_retention_policy should be None, but it's not." + ); } let mut pvc_retention_policy = StatefulSetPersistentVolumeClaimRetentionPolicy::default(); pvc_retention_policy.set_when_deleted("Delete".to_string()); @@ -161,12 +153,14 @@ pub fn test_persistent_volume_claim_retention_policy() { stateful_set_spec.set_pvc_retention_policy(pvc_retention_policy.clone()); assert_eq!( pvc_retention_policy.into_kube(), - stateful_set_spec.persistent_volume_claim_retention_policy().unwrap().into_kube() + stateful_set_spec + .persistent_volume_claim_retention_policy() + .unwrap() + .into_kube() ); } #[test] -#[verifier(external)] pub fn test_clone() { let mut stateful_set_spec = StatefulSetSpec::default(); let mut pod_template_spec = PodTemplateSpec::default(); @@ -186,7 +180,6 @@ pub fn test_clone() { } #[test] -#[verifier(external)] pub fn test_kube() { let kube_sts_spec = deps_hack::k8s_openapi::api::apps::v1::StatefulSetSpec { @@ -224,9 +217,5 @@ pub fn test_kube() { }; let sts_spec = StatefulSetSpec::from_kube(kube_sts_spec.clone()); - assert_eq!( - sts_spec.into_kube(), - kube_sts_spec - ); -} + assert_eq!(sts_spec.into_kube(), kube_sts_spec); } diff --git a/src/unit_tests/kubernetes_api_objects/stateful_set_status.rs b/src/unit_tests/kubernetes_api_objects/stateful_set_status.rs index 7ae82845f..05a79caf1 100644 --- a/src/unit_tests/kubernetes_api_objects/stateful_set_status.rs +++ b/src/unit_tests/kubernetes_api_objects/stateful_set_status.rs @@ -8,46 +8,32 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for stateful set status #[test] -#[verifier(external)] pub fn test_kube() { - let kube_stateful_set_status = - deps_hack::k8s_openapi::api::apps::v1::StatefulSetStatus { - replicas: 1, - ready_replicas: Some(1), - current_replicas: Some(1), - updated_replicas: Some(1), - current_revision: Some("current_revision".to_string()), - update_revision: Some("update_revision".to_string()), - collision_count: Some(1), - observed_generation: Some(1), - ..Default::default() - }; + let kube_stateful_set_status = deps_hack::k8s_openapi::api::apps::v1::StatefulSetStatus { + replicas: 1, + ready_replicas: Some(1), + current_replicas: Some(1), + updated_replicas: Some(1), + current_revision: Some("current_revision".to_string()), + update_revision: Some("update_revision".to_string()), + collision_count: Some(1), + observed_generation: Some(1), + ..Default::default() + }; let stateful_set_status = StatefulSetStatus::from_kube(kube_stateful_set_status.clone()); - assert_eq!( - stateful_set_status.into_kube(), - kube_stateful_set_status - ); + assert_eq!(stateful_set_status.into_kube(), kube_stateful_set_status); } #[test] -#[verifier(external)] pub fn test_ready_replicas() { - let stateful_set_status = StatefulSetStatus::from_kube( - deps_hack::k8s_openapi::api::apps::v1::StatefulSetStatus { + let stateful_set_status = + StatefulSetStatus::from_kube(deps_hack::k8s_openapi::api::apps::v1::StatefulSetStatus { replicas: 1, ready_replicas: Some(1), ..Default::default() - }, - ); - assert_eq!( - 1, - stateful_set_status.into_kube().ready_replicas.unwrap() - ); -} - + }); + assert_eq!(1, stateful_set_status.into_kube().ready_replicas.unwrap()); } diff --git a/src/unit_tests/kubernetes_api_objects/subject.rs b/src/unit_tests/kubernetes_api_objects/subject.rs index a83e12dc3..d935e7514 100644 --- a/src/unit_tests/kubernetes_api_objects/subject.rs +++ b/src/unit_tests/kubernetes_api_objects/subject.rs @@ -7,17 +7,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for subject #[test] -#[verifier(external)] pub fn test_default() { let subject = Subject::default(); - assert_eq!(subject.into_kube(), deps_hack::k8s_openapi::api::rbac::v1::Subject::default()); + assert_eq!( + subject.into_kube(), + deps_hack::k8s_openapi::api::rbac::v1::Subject::default() + ); } #[test] -#[verifier(external)] pub fn test_set_kind() { let mut subject = Subject::default(); subject.set_kind("kind".to_string()); @@ -25,7 +24,6 @@ pub fn test_set_kind() { } #[test] -#[verifier(external)] pub fn test_set_name() { let mut subject = Subject::default(); subject.set_name("name".to_string()); @@ -33,15 +31,16 @@ pub fn test_set_name() { } #[test] -#[verifier(external)] pub fn test_set_namespace() { let mut subject = Subject::default(); subject.set_namespace("namespace".to_string()); - assert_eq!("namespace".to_string(), subject.into_kube().namespace.unwrap()); + assert_eq!( + "namespace".to_string(), + subject.into_kube().namespace.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_kube() { let kube_subject = deps_hack::k8s_openapi::api::rbac::v1::Subject { kind: "kind".to_string(), @@ -52,12 +51,13 @@ pub fn test_kube() { let subject = Subject::from_kube(kube_subject.clone()); - assert_eq!(subject.into_kube(), - deps_hack::k8s_openapi::api::rbac::v1::Subject { - kind: "kind".to_string(), - name: "name".to_string(), - namespace: Some("namespace".to_string()), - ..Default::default() - }); -} + assert_eq!( + subject.into_kube(), + deps_hack::k8s_openapi::api::rbac::v1::Subject { + kind: "kind".to_string(), + name: "name".to_string(), + namespace: Some("namespace".to_string()), + ..Default::default() + } + ); } diff --git a/src/unit_tests/kubernetes_api_objects/tcp_socket_action.rs b/src/unit_tests/kubernetes_api_objects/tcp_socket_action.rs index 8978a133c..78789d82b 100644 --- a/src/unit_tests/kubernetes_api_objects/tcp_socket_action.rs +++ b/src/unit_tests/kubernetes_api_objects/tcp_socket_action.rs @@ -7,44 +7,48 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for life cycle #[test] -#[verifier(external)] pub fn test_set_host() { let mut tcp_socket_action = TCPSocketAction::default(); tcp_socket_action.set_host("host".to_string()); - assert_eq!("host".to_string(), tcp_socket_action.into_kube().host.unwrap()); + assert_eq!( + "host".to_string(), + tcp_socket_action.into_kube().host.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_port() { let mut tcp_socket_action = TCPSocketAction::default(); tcp_socket_action.set_port(8080); - assert_eq!(deps_hack::k8s_openapi::apimachinery::pkg::util::intstr::IntOrString::Int(8080), - tcp_socket_action.into_kube().port); + assert_eq!( + deps_hack::k8s_openapi::apimachinery::pkg::util::intstr::IntOrString::Int(8080), + tcp_socket_action.into_kube().port + ); } #[test] -#[verifier(external)] pub fn test_default() { let tcp_socket_action = TCPSocketAction::default(); - assert_eq!(tcp_socket_action.into_kube(), deps_hack::k8s_openapi::api::core::v1::TCPSocketAction::default()); + assert_eq!( + tcp_socket_action.into_kube(), + deps_hack::k8s_openapi::api::core::v1::TCPSocketAction::default() + ); } #[test] -#[verifier(external)] pub fn test_clone() { let mut tcp_socket_action = TCPSocketAction::default(); tcp_socket_action.set_host("host".to_string()); tcp_socket_action.set_port(8080); let tcp_socket_action_clone = tcp_socket_action.clone(); - assert_eq!(tcp_socket_action.into_kube(), tcp_socket_action_clone.into_kube()); + assert_eq!( + tcp_socket_action.into_kube(), + tcp_socket_action_clone.into_kube() + ); } #[test] -#[verifier(external)] pub fn test_kube() { let kube_tcp_socket_action = deps_hack::k8s_openapi::api::core::v1::TCPSocketAction { host: Some("host".to_string()), @@ -53,8 +57,5 @@ pub fn test_kube() { let tcp_socket_action = TCPSocketAction::from_kube(kube_tcp_socket_action.clone()); - assert_eq!(tcp_socket_action.into_kube(), - kube_tcp_socket_action); - -} + assert_eq!(tcp_socket_action.into_kube(), kube_tcp_socket_action); } diff --git a/src/unit_tests/kubernetes_api_objects/toleration.rs b/src/unit_tests/kubernetes_api_objects/toleration.rs index abbbca09f..67584e9c6 100644 --- a/src/unit_tests/kubernetes_api_objects/toleration.rs +++ b/src/unit_tests/kubernetes_api_objects/toleration.rs @@ -9,24 +9,16 @@ use deps_hack::k8s_openapi::apimachinery::pkg::apis::meta::v1::Time; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for toleration #[test] -#[verifier(external)] pub fn test_kube() { - let kube_toleration = - deps_hack::k8s_openapi::api::core::v1::Toleration { - key: Some("key".to_string()), - operator: Some("operator".to_string()), - value: Some("value".to_string()), - effect: Some("effect".to_string()), - toleration_seconds: Some(1), - ..Default::default() - }; + let kube_toleration = deps_hack::k8s_openapi::api::core::v1::Toleration { + key: Some("key".to_string()), + operator: Some("operator".to_string()), + value: Some("value".to_string()), + effect: Some("effect".to_string()), + toleration_seconds: Some(1), + ..Default::default() + }; let toleration = Toleration::from_kube(kube_toleration.clone()); - assert_eq!( - toleration.into_kube(), - kube_toleration - ); -} + assert_eq!(toleration.into_kube(), kube_toleration); } diff --git a/src/unit_tests/kubernetes_api_objects/volume.rs b/src/unit_tests/kubernetes_api_objects/volume.rs index 4e39743a9..2775cdaa6 100644 --- a/src/unit_tests/kubernetes_api_objects/volume.rs +++ b/src/unit_tests/kubernetes_api_objects/volume.rs @@ -9,17 +9,16 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for volume #[test] -#[verifier(external)] pub fn test_default() { let volume = Volume::default(); - assert_eq!(volume.into_kube(), deps_hack::k8s_openapi::api::core::v1::Volume::default()); + assert_eq!( + volume.into_kube(), + deps_hack::k8s_openapi::api::core::v1::Volume::default() + ); } #[test] -#[verifier(external)] pub fn test_set_name() { let mut volume = Volume::default(); volume.set_name("name".to_string()); @@ -31,108 +30,123 @@ pub fn test_set_name() { } #[test] -#[verifier(external)] pub fn test_set_host_path() { let mut volume = Volume::default(); let mut host_path_volume_source = HostPathVolumeSource::default(); host_path_volume_source.set_path("path".to_string()); volume.set_host_path(host_path_volume_source.clone()); - assert_eq!(host_path_volume_source.into_kube(), volume.into_kube().host_path.unwrap()); + assert_eq!( + host_path_volume_source.into_kube(), + volume.into_kube().host_path.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_config_map() { let mut volume = Volume::default(); let mut config_map_volume_source = ConfigMapVolumeSource::default(); config_map_volume_source.set_name("name".to_string()); volume.set_config_map(config_map_volume_source.clone()); - assert_eq!(config_map_volume_source.into_kube(), volume.into_kube().config_map.unwrap()); + assert_eq!( + config_map_volume_source.into_kube(), + volume.into_kube().config_map.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_projected() { let mut volume = Volume::default(); let mut projected_volume_source = ProjectedVolumeSource::default(); projected_volume_source.set_sources(vec![]); volume.set_projected(projected_volume_source.clone()); - assert_eq!(projected_volume_source.into_kube(), volume.into_kube().projected.unwrap()); + assert_eq!( + projected_volume_source.into_kube(), + volume.into_kube().projected.unwrap() + ); } - #[test] -#[verifier(external)] pub fn test_set_secret() { let mut volume = Volume::default(); let mut secret_volume_source = SecretVolumeSource::default(); secret_volume_source.set_secret_name("name".to_string()); volume.set_secret(secret_volume_source.clone()); - assert_eq!(secret_volume_source.into_kube(), volume.into_kube().secret.unwrap()); + assert_eq!( + secret_volume_source.into_kube(), + volume.into_kube().secret.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_downward_api() { let mut volume = Volume::default(); let mut downward_api_volume_source = DownwardAPIVolumeSource::default(); downward_api_volume_source.set_items(vec![]); volume.set_downward_api(downward_api_volume_source.clone()); - assert_eq!(downward_api_volume_source.into_kube(), volume.into_kube().downward_api.unwrap()); + assert_eq!( + downward_api_volume_source.into_kube(), + volume.into_kube().downward_api.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_empty_dir() { let mut volume = Volume::default(); let empty_dir_volume_source = EmptyDirVolumeSource::default(); volume.set_empty_dir(empty_dir_volume_source.clone()); - assert_eq!(empty_dir_volume_source.into_kube(), volume.into_kube().empty_dir.unwrap()); + assert_eq!( + empty_dir_volume_source.into_kube(), + volume.into_kube().empty_dir.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_kube() { let kube_volume = deps_hack::k8s_openapi::api::core::v1::Volume { name: "name".to_string(), - host_path: Some(deps_hack::k8s_openapi::api::core::v1::HostPathVolumeSource { - path: "path".to_string(), - ..Default::default() - }), - config_map: Some(deps_hack::k8s_openapi::api::core::v1::ConfigMapVolumeSource { - name: Some("name".to_string()), - ..Default::default() - }), - projected: Some(deps_hack::k8s_openapi::api::core::v1::ProjectedVolumeSource { - sources: Some(vec![]), - ..Default::default() - }), + host_path: Some( + deps_hack::k8s_openapi::api::core::v1::HostPathVolumeSource { + path: "path".to_string(), + ..Default::default() + }, + ), + config_map: Some( + deps_hack::k8s_openapi::api::core::v1::ConfigMapVolumeSource { + name: Some("name".to_string()), + ..Default::default() + }, + ), + projected: Some( + deps_hack::k8s_openapi::api::core::v1::ProjectedVolumeSource { + sources: Some(vec![]), + ..Default::default() + }, + ), secret: Some(deps_hack::k8s_openapi::api::core::v1::SecretVolumeSource { secret_name: Some("name".to_string()), ..Default::default() }), - downward_api: Some(deps_hack::k8s_openapi::api::core::v1::DownwardAPIVolumeSource { - items: Some(vec![]), - ..Default::default() - }), - empty_dir: Some(deps_hack::k8s_openapi::api::core::v1::EmptyDirVolumeSource { - ..Default::default() - }), + downward_api: Some( + deps_hack::k8s_openapi::api::core::v1::DownwardAPIVolumeSource { + items: Some(vec![]), + ..Default::default() + }, + ), + empty_dir: Some( + deps_hack::k8s_openapi::api::core::v1::EmptyDirVolumeSource { + ..Default::default() + }, + ), ..Default::default() }; let volume = Volume::from_kube(kube_volume.clone()); - assert_eq!( - volume.into_kube(), - kube_volume - ); - + assert_eq!(volume.into_kube(), kube_volume); } #[test] -#[verifier(external)] -pub fn test_clone(){ +pub fn test_clone() { let mut volume = Volume::default(); let mut host_path_volume_source = HostPathVolumeSource::default(); host_path_volume_source.set_path("path".to_string()); @@ -140,4 +154,3 @@ pub fn test_clone(){ let volume_clone = volume.clone(); assert_eq!(volume.into_kube(), volume_clone.into_kube()); } -} diff --git a/src/unit_tests/kubernetes_api_objects/volume_mount.rs b/src/unit_tests/kubernetes_api_objects/volume_mount.rs index 70b7d4966..1159a037a 100644 --- a/src/unit_tests/kubernetes_api_objects/volume_mount.rs +++ b/src/unit_tests/kubernetes_api_objects/volume_mount.rs @@ -7,18 +7,17 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for volume monts #[test] -#[verifier(external)] pub fn test_set_mount_path() { let mut volume_mount = VolumeMount::default(); volume_mount.set_mount_path("mount_path".to_string()); - assert_eq!("mount_path".to_string(), volume_mount.into_kube().mount_path); + assert_eq!( + "mount_path".to_string(), + volume_mount.into_kube().mount_path + ); } #[test] -#[verifier(external)] pub fn test_set_name() { let mut volume_mount = VolumeMount::default(); volume_mount.set_name("name".to_string()); @@ -26,7 +25,6 @@ pub fn test_set_name() { } #[test] -#[verifier(external)] pub fn test_set_read_only() { let mut volume_mount = VolumeMount::default(); volume_mount.set_read_only(true); @@ -34,38 +32,40 @@ pub fn test_set_read_only() { } #[test] -#[verifier(external)] pub fn test_set_sub_path() { let mut volume_mount = VolumeMount::default(); volume_mount.set_sub_path("sub_path".to_string()); - assert_eq!("sub_path".to_string(), volume_mount.into_kube().sub_path.unwrap()); + assert_eq!( + "sub_path".to_string(), + volume_mount.into_kube().sub_path.unwrap() + ); } #[test] -#[verifier(external)] -pub fn test_default(){ +pub fn test_default() { let volume_mount = VolumeMount::default(); - assert_eq!(volume_mount.into_kube(), deps_hack::k8s_openapi::api::core::v1::VolumeMount::default()); + assert_eq!( + volume_mount.into_kube(), + deps_hack::k8s_openapi::api::core::v1::VolumeMount::default() + ); } #[test] -#[verifier(external)] -pub fn test_new_with(){ - let volume_mount = VolumeMount::new_with( - "mount_path".to_string(), - "name".to_string(), +pub fn test_new_with() { + let volume_mount = VolumeMount::new_with("mount_path".to_string(), "name".to_string()); + assert_eq!( + volume_mount.into_kube(), + deps_hack::k8s_openapi::api::core::v1::VolumeMount { + mount_path: "mount_path".to_string(), + name: "name".to_string(), + ..Default::default() + } ); - assert_eq!(volume_mount.into_kube(), deps_hack::k8s_openapi::api::core::v1::VolumeMount{ - mount_path: "mount_path".to_string(), - name: "name".to_string(), - ..Default::default() - }); } #[test] -#[verifier(external)] -pub fn test_kube(){ - let kube_volume_mount = deps_hack::k8s_openapi::api::core::v1::VolumeMount{ +pub fn test_kube() { + let kube_volume_mount = deps_hack::k8s_openapi::api::core::v1::VolumeMount { mount_path: "mount_path".to_string(), name: "name".to_string(), sub_path: Some("sub_path".to_string()), @@ -77,4 +77,3 @@ pub fn test_kube(){ assert_eq!(volume_mount.into_kube(), kube_volume_mount.clone()); } -} diff --git a/src/unit_tests/kubernetes_api_objects/volume_projection.rs b/src/unit_tests/kubernetes_api_objects/volume_projection.rs index dd31279fc..33416dd8c 100644 --- a/src/unit_tests/kubernetes_api_objects/volume_projection.rs +++ b/src/unit_tests/kubernetes_api_objects/volume_projection.rs @@ -9,38 +9,41 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { -// Tests for volume projecion #[test] -#[verifier(external)] pub fn test_default() { let volume_projection = VolumeProjection::default(); - assert_eq!(volume_projection.into_kube(), deps_hack::k8s_openapi::api::core::v1::VolumeProjection::default()); + assert_eq!( + volume_projection.into_kube(), + deps_hack::k8s_openapi::api::core::v1::VolumeProjection::default() + ); } #[test] -#[verifier(external)] pub fn test_set_config_map() { let mut volume_projection = VolumeProjection::default(); let mut config_map_projection = ConfigMapProjection::default(); config_map_projection.set_name("name".to_string()); volume_projection.set_config_map(config_map_projection.clone()); - assert_eq!(config_map_projection.into_kube(), volume_projection.into_kube().config_map.unwrap()); + assert_eq!( + config_map_projection.into_kube(), + volume_projection.into_kube().config_map.unwrap() + ); } #[test] -#[verifier(external)] pub fn test_set_secrets() { let mut volume_projection = VolumeProjection::default(); let mut secret_projection = SecretProjection::default(); secret_projection.set_name("name".to_string()); volume_projection.set_secret(secret_projection.clone()); - assert_eq!(secret_projection.into_kube(), volume_projection.into_kube().secret.unwrap()); + assert_eq!( + secret_projection.into_kube(), + volume_projection.into_kube().secret.unwrap() + ); } #[test] -#[verifier(external)] -pub fn test_kube(){ +pub fn test_kube() { let kube_volume_projection = deps_hack::k8s_openapi::api::core::v1::VolumeProjection { config_map: Some(deps_hack::k8s_openapi::api::core::v1::ConfigMapProjection { name: Some("name".to_string()), @@ -55,8 +58,5 @@ pub fn test_kube(){ let volume_projection = VolumeProjection::from_kube(kube_volume_projection.clone()); - assert_eq!(volume_projection.into_kube(), - kube_volume_projection); - -} + assert_eq!(volume_projection.into_kube(), kube_volume_projection); } diff --git a/src/unit_tests/vstd_ext/string_map.rs b/src/unit_tests/vstd_ext/string_map.rs index 4be74c18f..838f7ed1e 100644 --- a/src/unit_tests/vstd_ext/string_map.rs +++ b/src/unit_tests/vstd_ext/string_map.rs @@ -4,10 +4,7 @@ use crate::vstd_ext::string_map::*; use vstd::prelude::*; use vstd::string::*; -verus! { - #[test] -#[verifier(external)] pub fn test_extend() { let mut m = StringMap::empty(); m.insert("key1".to_string(), "val1".to_string()); @@ -20,9 +17,10 @@ pub fn test_extend() { m.extend(m2); let rust_map = m.into_rust_map(); - assert_eq!(rust_map.get(&"key1".to_string()), Some(&"new_val1".to_string())); + assert_eq!( + rust_map.get(&"key1".to_string()), + Some(&"new_val1".to_string()) + ); assert_eq!(rust_map.get(&"key2".to_string()), Some(&"val2".to_string())); assert_eq!(rust_map.get(&"key3".to_string()), Some(&"val3".to_string())); } - -}