Fix after rebase

viperproject · Apr 11, 2023 · beafef8 · beafef8
1 parent 68a518e
commit beafef8
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 4 deletions.
diff --git a/native-verifier/src/fol.rs b/native-verifier/src/fol.rs
@@ -114,12 +114,12 @@ fn vir_statement_to_fol_statements(
                         position: op.position,
                     }),
                     Expression::UnaryOp(op) => Expression::UnaryOp(UnaryOp {
-                        op_kind: op.op_kind.clone(), // TODO: Copy trait derivation
+                        op_kind: op.op_kind,
                         argument: Box::new(substitute(&op.argument, mapping)),
                         position: op.position,
                     }),
                     Expression::ContainerOp(op) => Expression::ContainerOp(ContainerOp {
-                        kind: op.kind.clone(), // TODO: Copy trait derivation
+                        kind: op.kind,
                         container_type: op.container_type.clone(),
                         operands: op
                             .operands
@@ -163,7 +163,7 @@ fn vir_statement_to_fol_statements(
             preconds.chain(postconds).collect::<Vec<_>>()
         }
         Statement::Comment(comment) => vec![FolStatement::Comment(comment.comment.clone())],
-        Statement::LogEvent(_) => vec![], // TODO: Embed in SMT-LIB code
+        Statement::LogEvent(_) => vec![], // ignored
         _ => {
             unimplemented!("Statement {:?} not yet supported", statement);
         }

diff --git a/native-verifier/src/smt_lib.rs b/native-verifier/src/smt_lib.rs
@@ -303,7 +303,8 @@ impl SMTTranslatable for Program {
         self.domains.iter().for_each(|d| d.build_smt(smt));
         self.methods.iter().for_each(|d| d.build_smt(smt));
         self.procedures.iter().for_each(|d| d.build_smt(smt));
-        // TODO: Everything else
+        debug_assert!(self.functions.len() == 0); // TODO: Implement
+        debug_assert!(self.predicates.len() == 0);
     }
 }
 

diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs
@@ -69,6 +69,9 @@ impl<'a> Verifier<'a> {
                     VerificationBackend::Carbon => {
                         carbon::CarbonFrontend::with(env).new(reporter, logger)
                     }
+                    VerificationBackend::Lithium => {
+                        unreachable!("Lithium is not a JVM-based backend")
+                    }
                 }
             };
             let frontend_instance = jni.unwrap_result(unwrapped_frontend_instance);

diff --git a/vir/defs/low/ast/expression.rs b/vir/defs/low/ast/expression.rs
@@ -175,6 +175,7 @@ pub struct ContainerOp {
     pub position: Position,
 }
 
+#[derive(Copy)]
 pub enum ContainerOpKind {
     SeqEmpty,
     SeqConstructor,