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
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 2 of the License, or *)
(* (at your option) any later version. This file is also distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(* Processor-dependent builtin C functions *)
open C
let builtins = {
Builtins.typedefs = [
"__builtin_va_list", TPtr(TVoid [], [])
];
Builtins.functions = [
(* Integer arithmetic *)
"__builtin_bswap",
(TInt(IUInt, []), [TInt(IUInt, [])], false);
"__builtin_bswap32",
(TInt(IUInt, []), [TInt(IUInt, [])], false);
"__builtin_bswap16",
(TInt(IUShort, []), [TInt(IUShort, [])], false);
"__builtin_cntlz",
(TInt(IUInt, []), [TInt(IUInt, [])], false);
(* Float arithmetic *)
"__builtin_fsqrt",
(TFloat(FDouble, []), [TFloat(FDouble, [])], false);
(* Memory accesses *)
"__builtin_read16_reversed",
(TInt(IUShort, []), [TPtr(TInt(IUShort, [AConst]), [])], false);
"__builtin_read32_reversed",
(TInt(IUInt, []), [TPtr(TInt(IUInt, [AConst]), [])], false);
"__builtin_write16_reversed",
(TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false);
"__builtin_write32_reversed",
(TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false);
(* Synchronization *)
"__builtin_dmb",
(TVoid [], [], false);
"__builtin_dsb",
(TVoid [], [], false);
"__builtin_isb",
(TVoid [], [], false);
"__builtin_ldrex",
(TInt(IUInt, []), [TPtr(TInt(IUInt, [AConst]), [])], false);
"__builtin_ldrexb",
(TInt(IUChar, []), [TPtr(TInt(IUChar, [AConst]), [])], false);
"__builtin_ldrexh",
(TInt(IUShort, []), [TPtr(TInt(IUShort, [AConst]), [])], false);
"__builtin_ldrexd",
(TInt(IULongLong, []), [TPtr(TInt(IULongLong, [AConst]), [])], false);
"__builtin_strex",
(TInt(IInt, []), [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false);
"__builtin_strexb",
(TInt(IInt, []), [TPtr(TInt(IUChar, []), []); TInt(IUChar, [])], false);
"__builtin_strexh",
(TInt(IInt, []), [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false);
"__builtin_strexd",
(TInt(IInt, []), [TPtr(TInt(IULongLong, []), []); TInt(IULongLong, [])], false);
]
}
let size_va_list = 4
let va_list_scalar = true
|
