Merge branch 'main' into rust-toolchain-2022-11-20

model-checking · Nov 29, 2022 · fe84d4c · fe84d4c
2 parents 83c1865 + 6869324
commit fe84d4c
Show file tree

Hide file tree

Showing 50 changed files with 382 additions and 2,225 deletions.
diff --git a/cprover_bindings/src/env.rs b/cprover_bindings/src/env.rs
@@ -74,9 +74,6 @@ pub fn machine_model_symbols(mm: &MachineModel) -> Vec<Symbol> {
 pub fn additional_env_symbols() -> Vec<Symbol> {
     vec![
         Symbol::builtin_function("__CPROVER_initialize", vec![], Type::empty()),
-        // https://github.com/diffblue/cbmc/blob/b26d3479679574c6c179f911b488a314bc2f1085/src/util/config.h#L214
-        int_constant("__CPROVER_malloc_failure_mode_assert_then_assume", 2),
-        int_constant("__CPROVER_malloc_failure_mode_return_null", 1),
         Symbol::typedef("__CPROVER_size_t", "__CPROVER_size_t", Type::size_t(), Location::none()),
         Symbol::static_variable(
             "__CPROVER_memory",

diff --git a/cprover_bindings/src/goto_program/mod.rs b/cprover_bindings/src/goto_program/mod.rs
@@ -13,7 +13,6 @@ mod location;
 mod stmt;
 mod symbol;
 mod symbol_table;
-pub mod symtab_transformer;
 mod typ;
 
 pub use builtin::BuiltinFn;

diff --git a/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.rs b/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/expr_transformer.rs
diff --git a/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/mod.rs b/cprover_bindings/src/goto_program/symtab_transformer/gen_c_transformer/mod.rs