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 (116 lines) | stat: -rw-r--r-- 19,686 bytes parent folder | download | duplicates (2)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
// Debian package iaxmodem, spandsp

#ifdef __GNUC__
extern float fabsf (float __x);
extern float cabsf (float _Complex __z);
extern long double fabsl (long double __x);
extern double cabs (double _Complex __z);
extern double fabs (double __x);
extern long double cabsl (long double _Complex __z);

#  define CONCAT(a, b) a##b
#  define CONCAT2(a, b) CONCAT(a, b)

#  define STATIC_ASSERT(condition)                                             \
    int CONCAT2(some_array, __LINE__)[(condition) ? 1 : -1]
#endif

int main()
{
  #ifdef __GNUC__
  // expansion of fabs
  double damp;
  (void)(__extension__(__builtin_classify_type (__real__ ((__typeof__ (damp)) 0)) == 8));
  float famp;
  (void)(__extension__(
      __typeof__(__real__(
          __typeof__(*(
              (__typeof__(
                  (__typeof__(
                      (__typeof__ (famp)) 0) *) 0 ))
              0)))
        0)) famp);

  float v1;
  STATIC_ASSERT(
    __builtin_classify_type((__typeof__ (*(0 ?
                                           (__typeof__ (0 ?
                                                        (double *) 0 :
                                                        (void *) ((__builtin_classify_type ((__typeof__ (famp)) 0) == 8 ||
                                                                   (__builtin_classify_type ((__typeof__ (famp)) 0) == 9 &&
                                                                    __builtin_classify_type (__real__ ((__typeof__ (famp)) 0)) == 8))))) 0 :
                                           (__typeof__ (0 ?
                                                        (__typeof__ ((__typeof__ (famp)) 0) *) 0 :
                                                        (void *) (!((__builtin_classify_type ((__typeof__ (famp)) 0) == 8 ||
                                                                     (__builtin_classify_type ((__typeof__ (famp)) 0) == 9 &&
                                                                      __builtin_classify_type (__real__ ((__typeof__ (famp)) 0)) == 8)))))) 0)))0)
    ==
    __builtin_classify_type((float)0));

  v1 = (__extension__ ((sizeof (__real__ (famp)) == sizeof (double) ||
                        __builtin_classify_type (__real__ (famp)) != 8) ?
                       ((sizeof (__real__ (famp)) == sizeof (famp)) ?
                        (__typeof__ (__real__ (
                              /* type of this subexpression should be float,
                               * according to the STATIC_ASSERT above */
                              __typeof__ (*(0 ?
                                            (__typeof__ (0 ?
                                                         (double *) 0 :
                                                         (void *) ((__builtin_classify_type ((__typeof__ (famp)) 0) == 8 ||
                                                                    (__builtin_classify_type ((__typeof__ (famp)) 0) == 9 &&
                                                                     __builtin_classify_type (__real__ ((__typeof__ (famp)) 0)) == 8))))) 0 :
                                            (__typeof__ (0 ?
                                                         (__typeof__ ((__typeof__ (famp)) 0) *) 0 :
                                                         (void *) (!((__builtin_classify_type ((__typeof__ (famp)) 0) == 8 ||
                                                                      (__builtin_classify_type ((__typeof__ (famp)) 0) == 9 &&
                                                                       __builtin_classify_type (__real__ ((__typeof__ (famp)) 0)) == 8)))))) 0))) 0)) fabs (famp) :
                        (__typeof__ (__real__ (__typeof__ (*(0 ?
                                                             (__typeof__ (0 ?
                                                                          (double *) 0 :
                                                                          (void *) ((__builtin_classify_type ((__typeof__ (famp)) 0) == 8 ||
                                                                                     (__builtin_classify_type ((__typeof__ (famp)) 0) == 9 &&
                                                                                      __builtin_classify_type (__real__ ((__typeof__ (famp)) 0)) == 8))))) 0 : (__typeof__ (0 ?
                                                                                                                                                                            (__typeof__ ((__typeof__ (famp)) 0) *) 0 : (void *) (!((__builtin_classify_type ((__typeof__ (famp)) 0) == 8 ||
                                                                                                                                                                                                                                    (__builtin_classify_type ((__typeof__ (famp)) 0) == 9 &&
                                                                                                                                                                                                                                     __builtin_classify_type (__real__ ((__typeof__ (famp)) 0)) == 8)))))) 0))) 0)) cabs (famp)) :
                                                                                                                                                                                                                                    (sizeof (__real__ (famp)) == sizeof (float)) ?
                                                                                                                                                                                                                                    ((sizeof (__real__ (famp)) == sizeof (famp)) ?
                                                                                                                                                                                                                                     (__typeof__ (__real__ (__typeof__ (*(0 ?
                                                                                                                                                                                                                                                                          (__typeof__ (0 ?
                                                                                                                                                                                                                                                                                       (double *) 0 :
                                                                                                                                                                                                                                                                                       (void *) ((__builtin_classify_type ((__typeof__ (famp)) 0) == 8 ||
                                                                                                                                                                                                                                                                                                  (__builtin_classify_type ((__typeof__ (famp)) 0) == 9 &&
                                                                                                                                                                                                                                                                                                   __builtin_classify_type (__real__ ((__typeof__ (famp)) 0)) == 8))))) 0 :
                                                                                                                                                                                                                                                                          (__typeof__ (0 ?
                                                                                                                                                                                                                                                                                       (__typeof__ ((__typeof__ (famp)) 0) *) 0 : (void *) (!((__builtin_classify_type ((__typeof__ (famp)) 0) == 8 ||
                                                                                                                                                                                                                                                                                                                                               (__builtin_classify_type ((__typeof__ (famp)) 0) == 9 &&
                                                                                                                                                                                                                                                                                                                                                __builtin_classify_type (__real__ ((__typeof__ (famp)) 0)) == 8)))))) 0))) 0)) fabsf (famp) :
                                                                                                                                                                                                                                     (__typeof__ (__real__ (__typeof__ (*(0 ?
                                                                                                                                                                                                                                                                          (__typeof__ (0 ?
                                                                                                                                                                                                                                                                                       (double *) 0 : (void *) ((__builtin_classify_type ((__typeof__ (famp)) 0) == 8 ||
                                                                                                                                                                                                                                                                                                                 (__builtin_classify_type ((__typeof__ (famp)) 0) == 9 &&
                                                                                                                                                                                                                                                                                                                  __builtin_classify_type (__real__ ((__typeof__ (famp)) 0)) == 8))))) 0 : (__typeof__ (0 ?
                                                                                                                                                                                                                                                                                                                                                                                                                                                                (__typeof__ ((__typeof__ (famp)) 0) *) 0 : (void *) (!((__builtin_classify_type ((__typeof__ (famp)) 0) == 8 ||
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        (__builtin_classify_type ((__typeof__ (famp)) 0) == 9 &&
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         __builtin_classify_type (__real__ ((__typeof__ (famp)) 0)) == 8)))))) 0))) 0)) cabsf (famp)) :
                                                                                                                                                                                                                                    ((sizeof (__real__ (famp)) == sizeof (famp)) ?
                                                                                                                                                                                                                                     (__typeof__ (__real__ (__typeof__ (*(0 ?
                                                                                                                                                                                                                                                                          (__typeof__ (0 ?
                                                                                                                                                                                                                                                                                       (double *) 0 : (void *) ((__builtin_classify_type ((__typeof__ (famp)) 0) == 8 ||
                                                                                                                                                                                                                                                                                                                 (__builtin_classify_type ((__typeof__ (famp)) 0) == 9 &&
                                                                                                                                                                                                                                                                                                                  __builtin_classify_type (__real__ ((__typeof__ (famp)) 0)) == 8))))) 0 : (__typeof__ (0 ?
                                                                                                                                                                                                                                                                                                                                                                                                                                                                (__typeof__ ((__typeof__ (famp)) 0) *) 0 : (void *) (!((__builtin_classify_type ((__typeof__ (famp)) 0) == 8 ||
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        (__builtin_classify_type ((__typeof__ (famp)) 0) == 9 &&
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         __builtin_classify_type (__real__ ((__typeof__ (famp)) 0)) == 8)))))) 0))) 0)) fabsl (famp) :
                                                                                                                                                                                                                                     (__typeof__ (__real__ (__typeof__ (*(0 ?
                                                                                                                                                                                                                                                                          (__typeof__ (0 ?
                                                                                                                                                                                                                                                                                       (double *) 0 : (void *) ((__builtin_classify_type ((__typeof__ (famp)) 0) == 8 ||
                                                                                                                                                                                                                                                                                                                 (__builtin_classify_type ((__typeof__ (famp)) 0) == 9 &&
                                                                                                                                                                                                                                                                                                                  __builtin_classify_type (__real__ ((__typeof__ (famp)) 0)) == 8))))) 0 : (__typeof__ (0 ?
                                                                                                                                                                                                                                                                                                                                                                                                                                                                (__typeof__ ((__typeof__ (famp)) 0) *) 0 : (void *) (!((__builtin_classify_type ((__typeof__ (famp)) 0) == 8 ||
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                        (__builtin_classify_type ((__typeof__ (famp)) 0) == 9 &&
                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                         __builtin_classify_type (__real__ ((__typeof__ (famp)) 0)) == 8)))))) 0))) 0)) cabsl (famp))));
  #endif

  return 0;
}