@ @ requires \valid(ext); @ requires *ext == \null || valid_read_string(*ext); @ requires count > 0; @ requires \valid_read(software + (0 .. count-1)); @ requires \initialized(software + (0 .. count-1)); @ requires \initialized(software + (0 .. count-1)); @ ensures *ext == \null || valid_read_string(*ext); @ assigns *ext; @*/
| 828 | @ assigns *ext; |
| 829 | @*/ |
| 830 | static void software2ext(const char **ext, const char *software, const unsigned int count) |
| 831 | { |
| 832 | /*@ assert *ext == \null || valid_read_string(*ext); */ |
| 833 | if(count>=12) |
| 834 | { |
| 835 | /*@ assert \valid_read(software + (0 .. count-1)); */ |
| 836 | if(memcmp(software, "MicroStation", 12)==0) |
| 837 | { |
| 838 | *ext=extension_dgn; |
| 839 | /*@ assert valid_read_string(*ext); */ |
| 840 | return; |
| 841 | } |
| 842 | } |
| 843 | if(count>=14) |
| 844 | { |
| 845 | /*@ assert \valid_read(software + (0 .. count-1)); */ |
| 846 | if(memcmp(software, "Microsoft Word", 14)==0) |
| 847 | { |
| 848 | *ext=extension_doc; |
| 849 | /*@ assert valid_read_string(*ext); */ |
| 850 | return; |
| 851 | } |
| 852 | } |
| 853 | if(count>=15) |
| 854 | { |
| 855 | /*@ assert \valid_read(software + (0 .. count-1)); */ |
| 856 | if(memcmp(software, "Microsoft Excel", 15)==0) |
| 857 | { |
| 858 | if(*ext==NULL || strcmp(*ext,"sldprt")!=0) |
| 859 | { |
| 860 | *ext=extension_xls; |
| 861 | /*@ assert valid_read_string(*ext); */ |
| 862 | } |
| 863 | return; |
| 864 | } |
| 865 | } |
| 866 | if(count>=20) |
| 867 | { |
| 868 | /*@ assert \valid_read(software + (0 .. count-1)); */ |
| 869 | if(memcmp(software, "Microsoft PowerPoint", 20)==0) |
| 870 | { |
| 871 | *ext=extension_ppt; |
| 872 | /*@ assert valid_read_string(*ext); */ |
| 873 | return; |
| 874 | } |
| 875 | } |
| 876 | if(count>=21) |
| 877 | { |
| 878 | /*@ assert \valid_read(software + (0 .. count-1)); */ |
| 879 | if(memcmp(software, "Microsoft Office Word", 21)==0) |
| 880 | { |
| 881 | *ext=extension_doc; |
| 882 | /*@ assert valid_read_string(*ext); */ |
| 883 | return; |
| 884 | } |
| 885 | } |
| 886 | if(count==21) |
| 887 | { |
no outgoing calls
no test coverage detected