Factor out access to __CPROVER_dead_object

tautschnig · Jun 21, 2024 · 7f996e7 · 7f996e7
1 parent e7242f2
commit 7f996e7
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 15 deletions.
diff --git a/cprover_bindings/src/env.rs b/cprover_bindings/src/env.rs
@@ -8,7 +8,7 @@
 //! c.f. CBMC code [src/ansi-c/ansi_c_internal_additions.cpp].
 //! One possible invocation of this insertion in CBMC can be found in \[ansi_c_languaget::parse\].
 
-use super::goto_program::{Expr, Location, Symbol, Type};
+use super::goto_program::{Expr, Location, Symbol, SymbolTable, Type};
 use super::MachineModel;
 use num::bigint::BigInt;
 fn int_constant<T>(name: &str, value: T) -> Symbol
@@ -82,5 +82,16 @@ pub fn additional_env_symbols() -> Vec<Symbol> {
  Location::none(),
  )
  .with_is_extern(true),
+ Symbol::static_variable(
+ "__CPROVER_dead_object",
+ "__CPROVER_dead_object",
+ Type::void_pointer(),
+ Location::none(),
+ )
+ .with_is_extern(true),
  ]
 }
+
+pub fn global_dead_object(symbol_table: &SymbolTable) -> Expr {
+ symbol_table.lookup("__CPROVER_dead_object").unwrap().to_expr()
+}
diff --git a/cprover_bindings/src/lib.rs b/cprover_bindings/src/lib.rs
@@ -30,6 +30,7 @@
 //! 1. [irep::IrepId::Empty] and [irep::IrepId::Nil] behaves like \[null\].
 
 mod env;
+pub use env::global_dead_object;
 pub mod goto_program;
 pub mod irep;
 mod machine_model;

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -79,13 +79,7 @@ impl<'tcx> GotocCtx<'tcx> {
  if !self.current_fn().is_address_taken_local(*var_id) {
  Stmt::skip(location)
  } else {
- let global_dead_object = self.ensure_global_var(
- "__CPROVER_dead_object",
- false,
- Type::void_pointer(),
- Location::none(),
- |_, _| None,
- );
+ let global_dead_object = cbmc::global_dead_object(&self.symbol_table);
  Stmt::assign(
  global_dead_object.clone(),
  global_dead_object
@@ -103,13 +97,7 @@ impl<'tcx> GotocCtx<'tcx> {
  if !self.current_fn().is_address_taken_local(*var_id) {
  Stmt::skip(location)
  } else {
- let global_dead_object = self.ensure_global_var(
- "__CPROVER_dead_object",
- false,
- Type::void_pointer(),
- Location::none(),
- |_, _| None,
- );
+ let global_dead_object = cbmc::global_dead_object(&self.symbol_table);
  Stmt::assign(
  global_dead_object.clone(),
  Type::bool().nondet().ternary(