File: main.c

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 (20 lines) | stat: -rw-r--r-- 627 bytes parent folder | download | duplicates (3) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
 
typedef unsigned char u1;
typedef unsigned short u2;
typedef unsigned long long u4;

// Not resolved (as expected)
u4 B[( (u1)( ( (u1)15 ) / ( ( (((sizeof(u4))/(sizeof(u1)))*((u1)15)) > ((u1)64)) ? (0) : (1) ) ) )];

// Correctly resolved
u2 C[( (u1)( ( (u1)11 ) / ( ( (((sizeof(u2))/(sizeof(u1)))*((u1)11)) > ((u1)64)) ? (0) : (1) ) ) )];

int main()
{
  // Correctly resolved
  u2 A[( (u1)( ( (u1)1 ) / ( ( (((sizeof(u2))/(sizeof(u1)))*((u1)1)) > ((u1)64)) ? (0) : (1) ) ) )];

  // Correctly resolved
  static u4 D[( (u1)( ( (u1)4 ) / ( ( (((sizeof(u4))/(sizeof(u1)))*((u1)4)) > ((u1)64)) ? (0) : (1) ) ) )];

  return 0;
}