@@ -49,25 +49,35 @@ impl GotocCtx<'_> {
4949 /// handled later.
5050 pub fn codegen_foreign_fn ( & mut self , instance : Instance ) -> & Symbol {
5151 debug ! ( ?instance, "codegen_foreign_function" ) ;
52- let fn_name = instance. mangled_name ( ) . intern ( ) ;
52+ let trimmed_fn_name = instance. trimmed_name ( ) . intern ( ) ;
53+ let mangled_fn_name = instance. mangled_name ( ) . intern ( ) ;
5354 let loc = self . codegen_span_stable ( instance. def . span ( ) ) ;
54- if self . symbol_table . contains ( fn_name) {
55- // Symbol has been added (either a built-in CBMC function or a Rust allocation function).
56- self . symbol_table . lookup ( fn_name) . unwrap ( )
57- } else if RUST_ALLOC_FNS . contains ( & fn_name)
58- || ( self . is_cffi_enabled ( ) && instance. fn_abi ( ) . unwrap ( ) . conv == CallConvention :: C )
59- {
55+ if self . symbol_table . contains ( mangled_fn_name) {
56+ // Symbol has been added (a built-in CBMC function)
57+ self . symbol_table . lookup ( mangled_fn_name) . unwrap ( )
58+ } else if self . symbol_table . contains ( trimmed_fn_name) {
59+ // Symbol has been added (a Rust allocation function)
60+ self . symbol_table . lookup ( trimmed_fn_name) . unwrap ( )
61+ } else if RUST_ALLOC_FNS . contains ( & trimmed_fn_name) {
6062 // Add a Rust alloc lib function as is declared by core.
63+ // We use the trimmed name to ensure that it matches the function names in kani_lib.c
64+ self . ensure ( trimmed_fn_name, |gcx, _| {
65+ let typ = gcx. codegen_ffi_type ( instance) ;
66+ Symbol :: function ( trimmed_fn_name, typ, None , instance. name ( ) , loc)
67+ . with_is_extern ( true )
68+ } )
69+ } else if self . is_cffi_enabled ( ) && instance. fn_abi ( ) . unwrap ( ) . conv == CallConvention :: C {
6170 // When C-FFI feature is enabled, we just trust the rust declaration.
6271 // TODO: Add proper casting and clashing definitions check.
6372 // https://github.com/model-checking/kani/issues/1350
6473 // https://github.com/model-checking/kani/issues/2426
65- self . ensure ( fn_name , |gcx, _| {
74+ self . ensure ( mangled_fn_name , |gcx, _| {
6675 let typ = gcx. codegen_ffi_type ( instance) ;
67- Symbol :: function ( fn_name, typ, None , instance. name ( ) , loc) . with_is_extern ( true )
76+ Symbol :: function ( mangled_fn_name, typ, None , instance. name ( ) , loc)
77+ . with_is_extern ( true )
6878 } )
6979 } else {
70- let shim_name = format ! ( "{fn_name }_ffi_shim" ) ;
80+ let shim_name = format ! ( "{mangled_fn_name }_ffi_shim" ) ;
7181 trace ! ( ?shim_name, "codegen_foreign_function" ) ;
7282 self . ensure ( & shim_name, |gcx, _| {
7383 // Generate a shim with an unsupported C-FFI error message.
0 commit comments