-
Notifications
You must be signed in to change notification settings - Fork 38
Open
Labels
technical debtSomething for internal cleanupSomething for internal cleanup
Description
The following are added regardless of whether they are called or not, and it makes the output messy.
-- C function types
ffs_proxy: 'signed int (signed int)'
ffsl_proxy: 'signed int (signed long)'
ffsll_proxy: 'signed int (signed long_long)'
ctz_proxy: 'signed int (unsigned int)'
bswap16_proxy: 'uint16_t (uint16_t)'
bswap32_proxy: 'uint32_t (uint32_t)'
bswap64_proxy: 'uint64_t (uint64_t)'
unreachable_proxy: 'void ()'
__builtin_ctzl: 'signed int (unsigned long)'
__builtin_ctzll: 'signed int (unsigned long_long)'
tester: 'void (struct cluster_t*)'
-- Fun map
proc __builtin_ffs (loaded integer)
proc __builtin_ffsl (loaded integer)
proc __builtin_ffsll (loaded integer)
proc __builtin_ctz (loaded integer)
proc __builtin_ctzl (loaded integer)
proc __builtin_ctzll (loaded integer)
proc __builtin_bswap16 (loaded integer)
proc __builtin_bswap32 (loaded integer)
proc __builtin_bswap64 (loaded integer)
proc __builtin_unreachable ()
After this is done, the CN code below needs to be updated as well:
https://github.com/rems-project/cn/blob/7244b9f9c63d877326ee76394815c1eda886cb73/lib/check.ml#L2686-L2719
Metadata
Metadata
Assignees
Labels
technical debtSomething for internal cleanupSomething for internal cleanup