From f283759fc32e310637319e70fe26adc8960aa983 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 14 Dec 2023 13:56:09 -0500 Subject: [PATCH] Addressing code review leftovers --- cprover_bindings/src/goto_program/symbol.rs | 2 +- kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs | 1 + .../modifies/{vec_pass.fixme-2909.rs => vec_pass.rs} | 0 3 files changed, 2 insertions(+), 1 deletion(-) rename tests/expected/function-contract/modifies/{vec_pass.fixme-2909.rs => vec_pass.rs} (100%) diff --git a/cprover_bindings/src/goto_program/symbol.rs b/cprover_bindings/src/goto_program/symbol.rs index 0e5eccf0cd5a..b1082a8f1f80 100644 --- a/cprover_bindings/src/goto_program/symbol.rs +++ b/cprover_bindings/src/goto_program/symbol.rs @@ -386,7 +386,7 @@ impl Symbol { self } - /// Set `is_property` to true. + /// Set `is_property`. pub fn with_is_property(mut self, v: bool) -> Self { self.is_property = v; self diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 8eded8b15ea4..94dae51cf0e2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -256,6 +256,7 @@ impl<'tcx> GotocCtx<'tcx> { pub fn attach_contract(&mut self, instance: Instance<'tcx>, contract: Vec) { // This should be safe, since the contract is pretty much evaluated as // though it was the first (or last) assertion in the function. + assert!(self.current_fn.is_none()); self.set_current_fn(instance); let goto_contract = self.as_goto_contract(contract); let name = self.current_fn().name(); diff --git a/tests/expected/function-contract/modifies/vec_pass.fixme-2909.rs b/tests/expected/function-contract/modifies/vec_pass.rs similarity index 100% rename from tests/expected/function-contract/modifies/vec_pass.fixme-2909.rs rename to tests/expected/function-contract/modifies/vec_pass.rs