Commit 56a347e3 authored by Valentin Perrelle's avatar Valentin Perrelle

[Cil] Use forder as part of the key in in Cil_datatype.Fieldinfo

parent e436d980
...@@ -5528,10 +5528,10 @@ and makeCompType ghost (isstruct: bool) ...@@ -5528,10 +5528,10 @@ and makeCompType ghost (isstruct: bool)
let flds = Extlib.filter_map_opt to_field nglist in let flds = Extlib.filter_map_opt to_field nglist in
let flds = List.rev (fold addFieldGroup [] flds) in let flds = List.rev (fold addFieldGroup [] flds) in
let fld_table = Cil_datatype.Fieldinfo.Hashtbl.create 17 in let fld_table = Hashtbl.create 17 in
let check f = let check f =
try try
let oldf = Cil_datatype.Fieldinfo.Hashtbl.find fld_table f in let oldf = Hashtbl.find fld_table f.fname in
let source = fst f.floc in let source = fst f.floc in
Kernel.error ~source Kernel.error ~source
"field %s occurs multiple times in aggregate %a. \ "field %s occurs multiple times in aggregate %a. \
...@@ -5540,7 +5540,7 @@ and makeCompType ghost (isstruct: bool) ...@@ -5540,7 +5540,7 @@ and makeCompType ghost (isstruct: bool)
(fst oldf.floc).Filepath.pos_lnum (fst oldf.floc).Filepath.pos_lnum
with Not_found -> with Not_found ->
(* Do not add unnamed bitfields: they can share the empty name. *) (* Do not add unnamed bitfields: they can share the empty name. *)
if f.fname <> "" then Cil_datatype.Fieldinfo.Hashtbl.add fld_table f f if f.fname <> "" then Hashtbl.add fld_table f.fname f
in in
List.iter check flds; List.iter check flds;
if comp.cfields <> [] then begin if comp.cfields <> [] then begin
......
...@@ -822,7 +822,7 @@ module Fieldinfo = struct ...@@ -822,7 +822,7 @@ module Fieldinfo = struct
Typ.reprs) Typ.reprs)
[] []
Compinfo.reprs Compinfo.reprs
let fid fi = fi.fcomp.ckey, fi.fname let fid fi = fi.fcomp.ckey, fi.forder
let compare f1 f2 = Extlib.compare_basic (fid f1) (fid f2) let compare f1 f2 = Extlib.compare_basic (fid f1) (fid f2)
let hash f1 = Hashtbl.hash (fid f1) let hash f1 = Hashtbl.hash (fid f1)
let equal f1 f2 = (fid f1) = (fid f2) let equal f1 f2 = (fid f1) = (fid f2)
......
...@@ -516,8 +516,8 @@ ...@@ -516,8 +516,8 @@
"startLine": 168, "startLine": 168,
"startColumn": 4, "startColumn": 4,
"endLine": 170, "endLine": 170,
"endColumn": 82, "endColumn": 75,
"byteLength": 146 "byteLength": 132
} }
} }
} }
...@@ -587,8 +587,8 @@ ...@@ -587,8 +587,8 @@
"startLine": 240, "startLine": 240,
"startColumn": 4, "startColumn": 4,
"endLine": 244, "endLine": 244,
"endColumn": 70, "endColumn": 63,
"byteLength": 180 "byteLength": 173
} }
} }
} }
...@@ -1151,7 +1151,7 @@ ...@@ -1151,7 +1151,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 121, "endLine": 121,
"endColumn": 77, "endColumn": 77,
"byteLength": 155 "byteLength": 148
} }
} }
} }
...@@ -1266,7 +1266,7 @@ ...@@ -1266,7 +1266,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 125, "endLine": 125,
"endColumn": 77, "endColumn": 77,
"byteLength": 156 "byteLength": 149
} }
} }
} }
...@@ -1455,7 +1455,7 @@ ...@@ -1455,7 +1455,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 109, "endLine": 109,
"endColumn": 59, "endColumn": 59,
"byteLength": 125 "byteLength": 118
} }
} }
} }
...@@ -1992,8 +1992,8 @@ ...@@ -1992,8 +1992,8 @@
"startLine": 89, "startLine": 89,
"startColumn": 4, "startColumn": 4,
"endLine": 90, "endLine": 90,
"endColumn": 79, "endColumn": 72,
"byteLength": 108 "byteLength": 101
} }
} }
} }
...@@ -2202,8 +2202,8 @@ ...@@ -2202,8 +2202,8 @@
"startLine": 143, "startLine": 143,
"startColumn": 4, "startColumn": 4,
"endLine": 147, "endLine": 147,
"endColumn": 70, "endColumn": 63,
"byteLength": 177 "byteLength": 170
} }
} }
} }
...@@ -2439,7 +2439,7 @@ ...@@ -2439,7 +2439,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 59, "endLine": 59,
"endColumn": 62, "endColumn": 62,
"byteLength": 148 "byteLength": 134
} }
} }
} }
...@@ -2788,7 +2788,7 @@ ...@@ -2788,7 +2788,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 185, "endLine": 185,
"endColumn": 63, "endColumn": 63,
"byteLength": 150 "byteLength": 143
} }
} }
} }
...@@ -3563,7 +3563,7 @@ ...@@ -3563,7 +3563,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 202, "endLine": 202,
"endColumn": 22, "endColumn": 22,
"byteLength": 120 "byteLength": 113
} }
} }
} }
...@@ -3655,7 +3655,7 @@ ...@@ -3655,7 +3655,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 269, "endLine": 269,
"endColumn": 29, "endColumn": 29,
"byteLength": 167 "byteLength": 153
} }
} }
} }
...@@ -3958,7 +3958,7 @@ ...@@ -3958,7 +3958,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 97, "endLine": 97,
"endColumn": 58, "endColumn": 58,
"byteLength": 127 "byteLength": 120
} }
} }
} }
...@@ -4431,7 +4431,7 @@ ...@@ -4431,7 +4431,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 59, "endLine": 59,
"endColumn": 62, "endColumn": 62,
"byteLength": 148 "byteLength": 134
} }
} }
} }
...@@ -4826,7 +4826,7 @@ ...@@ -4826,7 +4826,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 105, "endLine": 105,
"endColumn": 51, "endColumn": 51,
"byteLength": 115 "byteLength": 108
} }
} }
} }
...@@ -4849,7 +4849,7 @@ ...@@ -4849,7 +4849,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 135, "endLine": 135,
"endColumn": 38, "endColumn": 38,
"byteLength": 192 "byteLength": 185
} }
} }
} }
...@@ -5078,8 +5078,8 @@ ...@@ -5078,8 +5078,8 @@
"startLine": 68, "startLine": 68,
"startColumn": 4, "startColumn": 4,
"endLine": 70, "endLine": 70,
"endColumn": 70, "endColumn": 63,
"byteLength": 156 "byteLength": 135
} }
} }
} }
...@@ -5269,8 +5269,8 @@ ...@@ -5269,8 +5269,8 @@
"startLine": 252, "startLine": 252,
"startColumn": 4, "startColumn": 4,
"endLine": 256, "endLine": 256,
"endColumn": 60, "endColumn": 53,
"byteLength": 208 "byteLength": 194
} }
} }
} }
...@@ -5364,7 +5364,7 @@ ...@@ -5364,7 +5364,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 269, "endLine": 269,
"endColumn": 29, "endColumn": 29,
"byteLength": 167 "byteLength": 153
} }
} }
} }
...@@ -5573,7 +5573,7 @@ ...@@ -5573,7 +5573,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 101, "endLine": 101,
"endColumn": 59, "endColumn": 59,
"byteLength": 124 "byteLength": 117
} }
} }
} }
...@@ -5739,7 +5739,7 @@ ...@@ -5739,7 +5739,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 113, "endLine": 113,
"endColumn": 51, "endColumn": 51,
"byteLength": 118 "byteLength": 111
} }
} }
} }
...@@ -5948,7 +5948,7 @@ ...@@ -5948,7 +5948,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 117, "endLine": 117,
"endColumn": 62, "endColumn": 62,
"byteLength": 157 "byteLength": 143
} }
} }
} }
...@@ -6636,7 +6636,7 @@ ...@@ -6636,7 +6636,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 130, "endLine": 130,
"endColumn": 38, "endColumn": 38,
"byteLength": 191 "byteLength": 184
} }
} }
} }
...@@ -6731,8 +6731,8 @@ ...@@ -6731,8 +6731,8 @@
"startLine": 39, "startLine": 39,
"startColumn": 4, "startColumn": 4,
"endLine": 42, "endLine": 42,
"endColumn": 77, "endColumn": 70,
"byteLength": 184 "byteLength": 170
} }
} }
} }
...@@ -6800,8 +6800,8 @@ ...@@ -6800,8 +6800,8 @@
"startLine": 155, "startLine": 155,
"startColumn": 4, "startColumn": 4,
"endLine": 159, "endLine": 159,
"endColumn": 60, "endColumn": 53,
"byteLength": 205 "byteLength": 191
} }
} }
} }
...@@ -7177,8 +7177,8 @@ ...@@ -7177,8 +7177,8 @@
"startLine": 143, "startLine": 143,
"startColumn": 4, "startColumn": 4,
"endLine": 147, "endLine": 147,
"endColumn": 70, "endColumn": 63,
"byteLength": 177 "byteLength": 170
} }
} }
} }
...@@ -7246,8 +7246,8 @@ ...@@ -7246,8 +7246,8 @@
"startLine": 240, "startLine": 240,
"startColumn": 4, "startColumn": 4,
"endLine": 244, "endLine": 244,
"endColumn": 70, "endColumn": 63,
"byteLength": 180 "byteLength": 173
} }
} }
} }
...@@ -7362,7 +7362,7 @@ ...@@ -7362,7 +7362,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 82, "endLine": 82,
"endColumn": 40, "endColumn": 40,
"byteLength": 183 "byteLength": 169
} }
} }
} }
...@@ -7500,7 +7500,7 @@ ...@@ -7500,7 +7500,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 135, "endLine": 135,
"endColumn": 38, "endColumn": 38,
"byteLength": 192 "byteLength": 185
} }
} }
} }
...@@ -7592,7 +7592,7 @@ ...@@ -7592,7 +7592,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 197, "endLine": 197,
"endColumn": 41, "endColumn": 41,
"byteLength": 188 "byteLength": 174
} }
} }
} }
...@@ -7614,8 +7614,8 @@ ...@@ -7614,8 +7614,8 @@
"startLine": 155, "startLine": 155,
"startColumn": 4, "startColumn": 4,
"endLine": 159, "endLine": 159,
"endColumn": 60, "endColumn": 53,
"byteLength": 205 "byteLength": 191
} }
} }
} }
...@@ -8124,8 +8124,8 @@ ...@@ -8124,8 +8124,8 @@
"startLine": 252, "startLine": 252,
"startColumn": 4, "startColumn": 4,
"endLine": 256, "endLine": 256,
"endColumn": 60, "endColumn": 53,
"byteLength": 208 "byteLength": 194
} }
} }
} }
...@@ -8267,7 +8267,7 @@ ...@@ -8267,7 +8267,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 185, "endLine": 185,
"endColumn": 63, "endColumn": 63,
"byteLength": 150 "byteLength": 143
} }
} }
} }
...@@ -8595,8 +8595,8 @@ ...@@ -8595,8 +8595,8 @@
"startLine": 39, "startLine": 39,
"startColumn": 4, "startColumn": 4,
"endLine": 42, "endLine": 42,
"endColumn": 77, "endColumn": 70,
"byteLength": 184 "byteLength": 170
} }
} }
} }
...@@ -8738,7 +8738,7 @@ ...@@ -8738,7 +8738,7 @@
"startColumn": 4, "startColumn": 4,
"endLine": 87, "endLine": 87,
"endColumn": 22, "endColumn": 22,
"byteLength": 116 "byteLength": 109
} }
} }
} }
...@@ -8829,8 +8829,8 @@ ...@@ -8829,8 +8829,8 @@
"startLine": 68, "startLine": 68,
"startColumn": 4, "startColumn": 4,
"endLine": 70, "endLine": 70,
"endColumn": 70, "endColumn": 63,
"byteLength": 156 "byteLength": 135
} }
} }
} }
...@@ -9538,8 +9538,8 @@ ...@@ -9538,8 +9538,8 @@
"startLine": 168, "startLine": 168,
"startColumn": 4, "startColumn": 4,
"endLine": 170, "endLine": 170,
"endColumn": 82, "endColumn": 75,
"byteLength": 146 "byteLength": 132
} }
} }
} }
......
...@@ -49,7 +49,7 @@ theory S1_S ...@@ -49,7 +49,7 @@ theory S1_S
(* use map.Map *) (* use map.Map *)
type S1_S = type S1_S =
| S1_S1 (F1_S_a:int -> int) (F1_S_b:int -> int) (F1_S_f:int) | S1_S1 (F1_S_f:int) (F1_S_a:int -> int) (F1_S_b:int -> int)
(* use Matrix *) (* use Matrix *)
...@@ -98,9 +98,9 @@ theory Compound ...@@ -98,9 +98,9 @@ theory Compound
(* use S1_S *) (* use S1_S *)
function Load_S1_S (p:addr) (mint:addr -> int) (mint1:addr -> int) : S1_S = function Load_S1_S (p:addr) (mint:addr -> int) (mint1:addr -> int) : S1_S =
S1_S1 (Array_uint32 (shiftfield_F1_S_a p) 5 mint) S1_S1 (get mint1 (shiftfield_F1_S_f p))
(Array_uint32 (shiftfield_F1_S_a p) 5 mint)
(Array_sint32 (shiftfield_F1_S_b p) 5 mint1) (Array_sint32 (shiftfield_F1_S_b p) 5 mint1)
(get mint1 (shiftfield_F1_S_f p))
Q_Array_uint32_access : Q_Array_uint32_access :
forall mint:addr -> int, i:int, n:int, p:addr forall mint:addr -> int, i:int, n:int, p:addr
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment