@@ -16,6 +16,7 @@ module Sem = BufferOverrunSemantics
16
16
module Trace = BufferOverrunTrace
17
17
module TraceSet = Trace. Set
18
18
module TypModels = BufferOverrunTypModels
19
+ module BoField = BufferOverrunField
19
20
20
21
module ModelEnv = struct
21
22
type model_env =
@@ -52,14 +53,37 @@ module Exec = struct
52
53
mem
53
54
54
55
55
- let rec decl_local_loc ({tenv} as model_env ) loc typ ~inst_num ~represents_multiple_values
56
+ let rec decl_local_struct_fields_loc : ModelEnv.model_env -> Loc.t -> Struct.fields -> Dom.Mem.t * int -> Dom.Mem.t * int =
57
+ fun model_env loc fields (mem , inst_num ) ->
58
+ match fields with
59
+ | field :: tl -> (
60
+ match field with
61
+ | (fn , typ , _ ) -> (
62
+ match typ.desc with
63
+ | Tarray {elt = _ ; length; stride} ->
64
+ let loc = BoField. Field {prefix= loc; fn; typ = (Some typ)} in
65
+ let stride = Option. map ~f: IntLit. to_int_exn stride in
66
+ let (mem, inst_num) = decl_local_array model_env loc typ ~length ?stride ~inst_num
67
+ ~represents_multiple_values: false ~dimension: 1 mem
68
+ in
69
+ (mem, inst_num)
70
+ | _ -> decl_local_struct_fields_loc model_env loc tl (mem, inst_num)))
71
+ | [] -> (mem, inst_num)
72
+ and decl_local_loc ({tenv} as model_env ) loc typ ~inst_num ~represents_multiple_values
56
73
~dimension mem =
57
74
match typ.Typ. desc with
58
75
| Typ. Tarray {elt = typ ; length; stride} ->
59
76
let stride = Option. map ~f: IntLit. to_int_exn stride in
60
77
decl_local_array model_env loc typ ~length ?stride ~inst_num ~represents_multiple_values
61
78
~dimension mem
62
79
| Typ. Tstruct typname -> (
80
+ let mem = (
81
+ match Tenv. lookup tenv typname with
82
+ | Some {fields} ->
83
+ let (mem, _) = decl_local_struct_fields_loc model_env loc fields (mem, 1 ) in mem
84
+ | None -> mem
85
+ )
86
+ in
63
87
match TypModels. dispatch tenv typname with
64
88
| Some (CArray {element_typ; length} ) ->
65
89
decl_local_array model_env loc element_typ ~length: (Some length) ~inst_num
0 commit comments