@ @ requires count > 0; @ requires \valid_read(software + (0 .. 2*count-1)); @ ensures \result == \null || \result == extension_et || \result == extension_psmodel; @ ensures \result == \null || valid_read_string(\result); @ assigns \nothing; @*/
| 915 | @ assigns \nothing; |
| 916 | @*/ |
| 917 | static const char *software_uni2ext(const char *software, const unsigned int count) |
| 918 | { |
| 919 | if(count>=15) |
| 920 | { |
| 921 | /*@ assert \valid_read(software + (0 .. 2*count-1)); */ |
| 922 | if(memcmp(software, "M\0i\0c\0r\0o\0s\0o\0f\0t\0 \0E\0x\0c\0e\0l\0", 30)==0) |
| 923 | { |
| 924 | /*@ assert valid_read_string(extension_et); */ |
| 925 | return extension_et; |
| 926 | } |
| 927 | } |
| 928 | if(count>=17) |
| 929 | { |
| 930 | /*@ assert \valid_read(software + (0 .. 2*count-1)); */ |
| 931 | if(memcmp(software, "D\0e\0l\0c\0a\0m\0 \0P\0o\0w\0e\0r\0S\0H\0A\0P\0E\0", 34)==0) |
| 932 | { |
| 933 | /*@ assert valid_read_string(extension_psmodel); */ |
| 934 | return extension_psmodel; |
| 935 | } |
| 936 | } |
| 937 | return NULL; |
| 938 | } |
| 939 | |
| 940 | struct summary_entry |
| 941 | { |
no outgoing calls
no test coverage detected