File: enum2.c

package info (click to toggle)
frama-c 20161101%2Bsilicon%2Bdfsg-5
  • links: PTS, VCS
  • area: main
  • in suites: stretch
  • size: 42,324 kB
  • ctags: 35,695
  • sloc: ml: 200,142; ansic: 31,465; makefile: 2,334; sh: 1,643; lisp: 259; python: 85; asm: 26
file content (37 lines) | stat: -rw-r--r-- 1,058 bytes parent folder | download
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
/* run.config*
  GCC:
  OPT: -cpp-gnu-like -cpp-command "gcc -C -E -I. %1 -o %2" -val @VALUECONFIG@ -deps -out -input -journal-disable
*/

/* This test of enums doubles with a test of the % syntax in -cpp-command */
//@ assigns \result \from \nothing;
int printf(const char*, ...);

#define BIT_DE_SIGNE_1 (0x98765432)
#define BIT_DE_SIGNE_0 (0x12345678)
typedef enum {
  E1_MOINS1 = -1,
  E1_SGN1 = BIT_DE_SIGNE_1,
  E1_SGN0 = BIT_DE_SIGNE_0
  } E1 ;

E1 f(E1 x) { E1 y = x; return x; }

unsigned char enum1_sgn1_positif (void) {
  unsigned char res = (f((E1)E1_SGN1)) > 0;
  printf ("enum1_sgn1_positif = %d\n", res);
  return res; /* WARN : ppc->0 ; gcc->1 */
}
unsigned char enum1_sgn1_inf_sgn0 (void) {
  unsigned char res = E1_SGN1 < E1_SGN0;
  printf ("enum1_sgn1_inf_sgn0 = %d\n", res);
  return res; /* WARN : ppc->1 ; gcc->0 */
}
unsigned char must_be_one, must_be_zero;
int main (void) {
  int res = sizeof (E1);
  must_be_zero = enum1_sgn1_inf_sgn0();
  must_be_one = enum1_sgn1_positif();
  printf ("sizeof_enum1 = %d\n", res);
  return res; 
}