File: test-signed.desc

package info (click to toggle)
cbmc 6.6.0-4
  • links: PTS
  • area: main
  • in suites: forky, sid, trixie
  • size: 153,852 kB
  • sloc: cpp: 386,459; ansic: 114,466; java: 28,405; python: 6,003; yacc: 4,552; makefile: 4,041; lex: 2,487; xml: 2,388; sh: 2,050; perl: 557; pascal: 184; javascript: 163; ada: 36
file content (14 lines) | stat: -rw-r--r-- 456 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
 
CORE
test-signed.json
--dump-c
^EXIT=0$
^SIGNAL=0$
signed char ror8=\(unsigned char\)('8'|56) >> 3 % 8 \| \(unsigned char\)('8'|56) << 8 - 3 % 8;
--
irep
--
This tests that the ror goto operation is converted into suitable bit
twiddling operations in C representation. This is also checks that
signed rotations cast to unsigned to perform the shifts to avoid
sign bit problems. Also the negative check for "irep" checks that no
irep is failing conversion.