@ @ requires 8 <= size <= 1024*1024; @ requires \valid_read(buffer+ (0 .. size-1)); @ requires \initialized(buffer+ (0 .. size-1)); @ requires \valid(ext); @ requires \valid(title + (0 .. 1024-1)); @ requires \valid(file_time); @ requires \valid_read(entry); @ requires \initialized(entry); @ requires *ext == \null || valid_read_string(*ext); @ requires valid_string(title); @
| 1177 | @ assigns *ext, *(title + (0..1023)), *file_time; |
| 1178 | @*/ |
| 1179 | static void OLE_parse_PropertySet_entry(const char *buffer, const unsigned int size, const struct summary_entry *entry, const char **ext, char *title, time_t *file_time) |
| 1180 | { |
| 1181 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1182 | /*@ assert valid_read_string(title); */ |
| 1183 | const unsigned int tag=le32(entry->tag); |
| 1184 | const unsigned int offset=le32(entry->offset); |
| 1185 | unsigned int type; |
| 1186 | if(offset >= size - 4) |
| 1187 | { |
| 1188 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1189 | /*@ assert valid_string(title); */ |
| 1190 | return; |
| 1191 | } |
| 1192 | /*@ assert offset < size - 4; */ |
| 1193 | /*@ assert \valid_read(buffer + (0 .. offset + 4 - 1)); */ |
| 1194 | type=get32u(buffer, offset); |
| 1195 | #ifdef DEBUG_OLE |
| 1196 | log_info("entry: tag 0x%x, offset 0x%x, offset + 4 0x%x, type 0x%x\n", |
| 1197 | tag, offset, offset + 4, type); |
| 1198 | #endif |
| 1199 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1200 | /*@ assert valid_string(title); */ |
| 1201 | /* tag: Software, type: VT_LPSTR */ |
| 1202 | if(tag==0x12 && type==30) |
| 1203 | { |
| 1204 | /*@ assert valid_string(title); */ |
| 1205 | OLE_parse_software_entry(buffer, size, offset, ext); |
| 1206 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1207 | /*@ assert valid_string(title); */ |
| 1208 | return; |
| 1209 | } |
| 1210 | /* tag: Software, type: VT_LPWSTR */ |
| 1211 | if(tag==0x12 && type==31) |
| 1212 | { |
| 1213 | /*@ assert valid_string(title); */ |
| 1214 | OLE_parse_uni_software_entry(buffer, size, offset, ext); |
| 1215 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1216 | /*@ assert valid_string(title); */ |
| 1217 | return; |
| 1218 | } |
| 1219 | /* tag: title, type: VT_LPSTR */ |
| 1220 | if(tag==0x02 && type==30 && title[0]=='\0') |
| 1221 | { |
| 1222 | OLE_parse_title_entry(buffer, size, offset, title); |
| 1223 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1224 | /*@ assert valid_string(title); */ |
| 1225 | return ; |
| 1226 | } |
| 1227 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1228 | /*@ assert valid_string(title); */ |
| 1229 | /* ModifyDate, type=VT_FILETIME */ |
| 1230 | if(tag==0x0d && type==64) |
| 1231 | { |
| 1232 | OLE_parse_filetime_entry(buffer, size, offset, file_time); |
| 1233 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 1234 | /*@ assert valid_string(title); */ |
| 1235 | return; |
| 1236 | } |
no test coverage detected