@@ -49,25 +49,35 @@ impl GotocCtx<'_> {
49
49
/// handled later.
50
50
pub fn codegen_foreign_fn ( & mut self , instance : Instance ) -> & Symbol {
51
51
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 ( ) ;
53
54
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) {
60
62
// 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 {
61
70
// When C-FFI feature is enabled, we just trust the rust declaration.
62
71
// TODO: Add proper casting and clashing definitions check.
63
72
// https://github.com/model-checking/kani/issues/1350
64
73
// https://github.com/model-checking/kani/issues/2426
65
- self . ensure ( fn_name , |gcx, _| {
74
+ self . ensure ( mangled_fn_name , |gcx, _| {
66
75
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 )
68
78
} )
69
79
} else {
70
- let shim_name = format ! ( "{fn_name }_ffi_shim" ) ;
80
+ let shim_name = format ! ( "{mangled_fn_name }_ffi_shim" ) ;
71
81
trace ! ( ?shim_name, "codegen_foreign_function" ) ;
72
82
self . ensure ( & shim_name, |gcx, _| {
73
83
// Generate a shim with an unsupported C-FFI error message.
0 commit comments