File tree Expand file tree Collapse file tree 4 files changed +44
-1
lines changed Expand file tree Collapse file tree 4 files changed +44
-1
lines changed Original file line number Diff line number Diff line change
1
+ #ifdef __GNUC__
2
+ // example extracted from SV-COMP's ldv-linux-3.4-simple/
3
+ // 32_7_cpp_false-unreach-call_single_drivers-net-phy-dp83640
4
+ static int __attribute__((__section__ (".init.text" )))
5
+ __attribute__((no_instrument_function )) dp83640_init (void )
6
+ {
7
+ return 0 ;
8
+ }
9
+ int init_module (void ) __attribute__((alias ("dp83640_init" )));
10
+ #endif
11
+
12
+ int main ()
13
+ {
14
+ #ifdef __GNUC__
15
+ dp83640_init ();
16
+ #endif
17
+ return 0 ;
18
+ }
Original file line number Diff line number Diff line change
1
+ CORE
2
+ main.c
3
+
4
+ ^EXIT=0$
5
+ ^SIGNAL=0$
6
+ --
7
+ ^warning: ignoring
8
+ ^CONVERSION ERROR$
Original file line number Diff line number Diff line change @@ -11,11 +11,23 @@ const char* __attribute__((section("s"))) __attribute__((weak)) bar();
11
11
volatile int __attribute__((__section__ (".init.data1" ))) txt_heap_base1 ;
12
12
volatile int __attribute__((__section__ (".init.data3" ))) txt_heap_base , __attribute__ ((__section__ (".init.data4" ))) txt_heap_size ;
13
13
14
+ int __attribute__((__section__ (".init.text" ))) __attribute__((__cold__ ))
15
+ __alloc_bootmem_huge_page (void * h );
16
+ int __attribute__((__section__ (".init.text" ))) __attribute__((__cold__ ))
17
+ alloc_bootmem_huge_page (void * h );
18
+ int alloc_bootmem_huge_page (void * h )
19
+ __attribute__((weak , alias ("__alloc_bootmem_huge_page" )));
20
+ int __alloc_bootmem_huge_page (void * h )
21
+ {
22
+ return 1 ;
23
+ }
14
24
#endif
15
25
16
26
int main ()
17
27
{
18
28
#ifdef __GNUC__
29
+ int r = alloc_bootmem_huge_page (0 );
30
+
19
31
static int __attribute__((section (".data.unlikely" ))) __warned ;
20
32
__warned = 1 ;
21
33
return __warned ;
Original file line number Diff line number Diff line change @@ -708,7 +708,12 @@ void c_typecheck_baset::typecheck_declaration(
708
708
709
709
// alias function need not have been declared yet, thus
710
710
// can't lookup
711
- symbol.value =symbol_exprt (full_spec.alias );
711
+ // also cater for renaming/placement in sections
712
+ const auto &renaming_entry = asm_label_map.find (full_spec.alias );
713
+ if (renaming_entry == asm_label_map.end ())
714
+ symbol.value = symbol_exprt (full_spec.alias );
715
+ else
716
+ symbol.value = symbol_exprt (renaming_entry->second );
712
717
symbol.is_macro =true ;
713
718
}
714
719
You can’t perform that action at this time.
0 commit comments