diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-10-21 10:34:06 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-10-21 10:34:06 +0200 |
| commit | e4c28e18228a6adf7d354059200ced5cee53e8c0 (patch) | |
| tree | 3c4d870d8253cdd23e8c79cd8e26f75cf790c259 /debug | |
| parent | 6c228c9ac5ddd93d02698e7da4c4cba053c6a1ca (diff) | |
| download | compcert-e4c28e18228a6adf7d354059200ced5cee53e8c0.tar.gz compcert-e4c28e18228a6adf7d354059200ced5cee53e8c0.zip | |
Fixed smaller mistakes.
Diffstat (limited to 'debug')
| -rw-r--r-- | debug/DwarfTypes.ml | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/debug/DwarfTypes.ml b/debug/DwarfTypes.ml index caa6435c..1cb3f6ee 100644 --- a/debug/DwarfTypes.ml +++ b/debug/DwarfTypes.ml @@ -200,7 +200,7 @@ type dw_tag_subprogram = dw_at_inline: inline option; dw_at_low_pc: address; dw_at_name: string; - dw_at_prototyped: flag + dw_at_prototyped: flag; dw_at_sibling: reference option; dw_at_type: reference; } @@ -233,22 +233,20 @@ type dw_tag_union_type = dw_at_byte_size: constant; dw_at_name: string; dw_at_sibling: reference option; - dw_at_start_scope: constant option; - dw_at_type: reference option; } type dw_tag_unspecified_parameter = { - dw_at_decl_file: constant option; - dw_at_decl_line: constant option; + dw_at_decl_file: constant option; + dw_at_decl_line: constant option; dw_at_artificial: flag option; dw_at_sibling: reference option; } type dw_tag_variable = { - dw_at_decl_file: constant option; - dw_at_decl_line: constant option; + dw_at_decl_file: constant option; + dw_at_decl_line: constant option; dw_at_declaration: flag option; dw_at_external: flag option; dw_at_location: location_value option; @@ -261,5 +259,6 @@ type dw_tag_variable = type dw_tag_volatile_type = { dw_at_sibling: reference option; - dw_at_type: reference option; + dw_at_type: reference; } + |