source: Deliverables/D2.2/8051/src/clight/clightUtils.ml @ 486

Last change on this file since 486 was 486, checked in by ayache, 9 years ago

Deliverable D2.2

File size: 2.2 KB
Line 
1
2open Clight
3
4
5(* TODO: Alignment constraints? *)
6let rec size_of_ctype = function
7  | Tvoid               -> 0
8  | Tint (I8,_)         -> 1
9  | Tint (I16,_)        -> 2
10  | Tint (I32,_)        -> 4
11  | Tfloat _            -> assert false (* Not supported *)
12  | Tpointer (sp,_)     -> Memory.size_of_region sp
13  | Tarray (sp,t,s)     -> s*(size_of_ctype t)
14  | Tfunction (_,_)     -> assert false (* Not supported *) 
15  | Tstruct (_,lst)     -> 
16      List.fold_left (fun n (_,ty) -> n + (size_of_ctype ty)) 0 lst
17  | Tunion (_,lst)      -> 
18      List.fold_left
19        (fun n (_,ty)   -> 
20           let sz = (size_of_ctype ty) in (if n>sz then n else sz)
21        ) 0 lst
22  | Tcomp_ptr (sp,_)    -> Memory.size_of_region sp
23
24
25let rec memory_q_of_ctype = function
26  | Tvoid               -> assert false
27  | Tint (I8,Signed)    -> Memory.MQ_int8signed 
28  | Tint (I8,Unsigned)  -> Memory.MQ_int8unsigned
29  | Tint (I16,Signed)   -> Memory.MQ_int16signed
30  | Tint (I16,Unsigned) -> Memory.MQ_int16unsigned
31  | Tint (I32,Signed)   -> Memory.MQ_int32
32  | Tint (I32,Unsigned) -> assert false (* Not supported *)
33  | Tfloat _            -> assert false (* Not supported *)
34  | Tpointer (sp,_)     -> Memory.mq_of_region sp
35  | Tarray (sp,c,s)     -> Memory.mq_of_region sp
36  | Tfunction (_,_)     -> assert false (* should not happen thanks to CIL *)
37  | Tstruct (_,_)       -> assert false (* should not happen thanks to CIL *)
38  | Tunion (_,_)        -> assert false (* should not happen thanks to CIL *)
39  | Tcomp_ptr (sp,_)    -> Memory.mq_of_region sp
40
41
42let is_int_type = function
43  | Tint (_,_)    -> true
44  | _ -> false
45
46let is_float_type = function
47  | Tfloat _  -> true
48  | _ -> false
49
50let is_pointer_type = function
51  | Tpointer _ | Tarray _ | Tcomp_ptr _ -> true
52  | _ -> false
53
54let is_stack_type = function
55  | Tarray _ | Tstruct _ | Tunion _ -> true
56  | _ -> false
57
58let is_struct = function
59  | Tstruct _ | Tunion _ -> true
60  | _ -> false
61
62let is_ptr_to_struct = function
63  | Tpointer (_,t) when is_struct t -> true
64  | Tcomp_ptr _ -> true
65  | _ -> false 
66
67let is_function = function
68  | Tfunction _ -> true
69  | _ -> false
70
71let region_of_pointer_type = function
72  | Tpointer (sp,_) | Tarray (sp,_,_) | Tcomp_ptr (sp,_) -> sp
73  | _ -> assert false (* do not use on those arguments *)
Note: See TracBrowser for help on using the repository browser.