Add building fluent controller to CI

Signed-off-by: Xudong Sun <[email protected]>
anvil-verifier · Sep 6, 2023 · dc76bee · dc76bee
1 parent 5e72a49
commit dc76bee
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 6 deletions.
diff --git a/.github/workflows/regression-testing.yml b/.github/workflows/regression-testing.yml
@@ -35,3 +35,5 @@ jobs:
         run: VERUS_DIR=$PWD/verus ./build.sh zookeeper_controller.rs --rlimit 30 --time
       - name: Build rabbitmq controller
         run: VERUS_DIR=$PWD/verus ./build.sh rabbitmq_controller.rs --rlimit 30 --time
+      - name: Build fluent controller
+        run: VERUS_DIR=$PWD/verus ./build.sh fluent_controller.rs --rlimit 30 --time
diff --git a/src/controller_examples/fluent_controller/fluentbit/exec/reconciler.rs b/src/controller_examples/fluent_controller/fluentbit/exec/reconciler.rs
@@ -7,9 +7,10 @@ use crate::fluent_controller::fluentbit::exec::types::*;
 use crate::fluent_controller::fluentbit::spec::reconciler as fluent_spec;
 use crate::kubernetes_api_objects::resource::ResourceWrapper;
 use crate::kubernetes_api_objects::{
-    api_method::*, common::*, config_map::*, daemon_set::*, label_selector::*, object_meta::*,
-    owner_reference::*, persistent_volume_claim::*, pod::*, pod_template_spec::*, resource::*,
-    resource_requirements::*, role::*, role_binding::*, secret::*, service::*, service_account::*,
+    api_method::*, common::*, config_map::*, container::*, daemon_set::*, label_selector::*,
+    object_meta::*, owner_reference::*, persistent_volume_claim::*, pod::*, pod_template_spec::*,
+    resource::*, resource_requirements::*, role::*, role_binding::*, secret::*, service::*,
+    service_account::*, volume::*,
 };
 use crate::pervasive_ext::string_map::StringMap;
 use crate::pervasive_ext::string_view::*;

diff --git a/src/controller_examples/fluent_controller/fluentbit/spec/reconciler.rs b/src/controller_examples/fluent_controller/fluentbit/spec/reconciler.rs
@@ -5,9 +5,9 @@ use crate::external_api::spec::*;
 use crate::fluent_controller::fluentbit::common::*;
 use crate::fluent_controller::fluentbit::spec::types::*;
 use crate::kubernetes_api_objects::{
-    api_method::*, common::*, config_map::*, daemon_set::*, label_selector::*, object_meta::*,
-    persistent_volume_claim::*, pod::*, pod_template_spec::*, resource::*, role::*,
-    role_binding::*, secret::*, service::*, service_account::*,
+    api_method::*, common::*, config_map::*, container::*, daemon_set::*, label_selector::*,
+    object_meta::*, persistent_volume_claim::*, pod::*, pod_template_spec::*, resource::*, role::*,
+    role_binding::*, secret::*, service::*, service_account::*, volume::*,
 };
 use crate::kubernetes_cluster::spec::message::*;
 use crate::pervasive_ext::string_view::*;

diff --git a/src/controller_examples/fluent_controller/fluentbit_config/spec/types.rs b/src/controller_examples/fluent_controller/fluentbit_config/spec/types.rs
@@ -92,6 +92,8 @@ impl ResourceView for FluentBitConfigView {
     #[verifier(external_body)]
     proof fn spec_integrity_is_preserved_by_marshal() {}
 
+    proof fn from_dynamic_object_result_determined_by_unmarshal() {}
+
     open spec fn rule(obj: FluentBitConfigView) -> bool {
         true
     }