File tree Expand file tree Collapse file tree 2 files changed +17
-5
lines changed
regression/cbmc/clang_builtins Expand file tree Collapse file tree 2 files changed +17
-5
lines changed Original file line number Diff line number Diff line change 88#define ror (type , x , d ) \
99 ((type)(((x) >> (d)) | ((x) << ((8 * sizeof(type)) - (d)))))
1010
11- #ifdef __clang__
11+ #ifndef __clang__
12+ unsigned char __builtin_rotateleft8 (unsigned char , unsigned char );
13+ unsigned short __builtin_rotateleft16 (unsigned short , unsigned short );
14+ unsigned int __builtin_rotateleft32 (unsigned int , unsigned int );
15+ unsigned long long
16+ __builtin_rotateleft64 (unsigned long long , unsigned long long );
17+
18+ unsigned char __builtin_rotateright8 (unsigned char , unsigned char );
19+ unsigned short __builtin_rotateright16 (unsigned short , unsigned short );
20+ unsigned int __builtin_rotateright32 (unsigned int , unsigned int );
21+ unsigned long long
22+ __builtin_rotateright64 (unsigned long long , unsigned long long );
23+ #endif
24+
1225void check_left8 (void )
1326{
1427 uint8_t op ;
@@ -80,11 +93,9 @@ void check_right64(void)
8093 assert (__builtin_rotateright64 (op , 3 ) == ror (uint64_t , op , 3 ));
8194 assert (__builtin_rotateright64 (op , 4 ) == ror (uint64_t , op , 4 ));
8295}
83- #endif
8496
8597int main (void )
8698{
87- #ifdef __clang__
8899 check_left8 ();
89100 check_left16 ();
90101 check_left32 ();
@@ -93,5 +104,4 @@ int main(void)
93104 check_right16 ();
94105 check_right32 ();
95106 check_right64 ();
96- #endif
97107}
Original file line number Diff line number Diff line change 1- CORE gcc-only
1+ CORE
22rotate.c
33
44^VERIFICATION SUCCESSFUL$
55^EXIT=0$
66^SIGNAL=0$
7+ --
8+ ^warning: ignoring
You can’t perform that action at this time.
0 commit comments