@ @ requires \valid(files_enable); @ requires valid_read_string(*current_cmd); @ requires \separated(files_enable, current_cmd, *current_cmd); @ ensures valid_read_string(*current_cmd); @*/
| 70 | @ ensures valid_read_string(*current_cmd); |
| 71 | @*/ |
| 72 | static int file_select_cli(file_enable_t *files_enable, char**current_cmd) |
| 73 | { |
| 74 | int keep_asking; |
| 75 | log_info("\nInterface File Select\n"); |
| 76 | /*@ loop invariant valid_read_string(*current_cmd); */ |
| 77 | do |
| 78 | { |
| 79 | file_enable_t *file_enable; |
| 80 | keep_asking=0; |
| 81 | skip_comma_in_command(current_cmd); |
| 82 | if(*current_cmd[0]=='\0') |
| 83 | return 0; |
| 84 | if(check_command(current_cmd,"everything",10)==0) |
| 85 | { |
| 86 | int enable_status; |
| 87 | keep_asking=1; |
| 88 | skip_comma_in_command(current_cmd); |
| 89 | if(check_command(current_cmd,"enable",6)==0) |
| 90 | { |
| 91 | enable_status=1; |
| 92 | } |
| 93 | else if(check_command(current_cmd,"disable",7)==0) |
| 94 | { |
| 95 | enable_status=0; |
| 96 | } |
| 97 | else |
| 98 | { |
| 99 | log_critical("Syntax error %s\n",*current_cmd); |
| 100 | return -1; |
| 101 | } |
| 102 | for(file_enable=&files_enable[0];file_enable->file_hint!=NULL;file_enable++) |
| 103 | file_enable->enable=enable_status; |
| 104 | } |
| 105 | else |
| 106 | { |
| 107 | const char *extension=*current_cmd; |
| 108 | unsigned int cmd_length=0; |
| 109 | unsigned int tmp; |
| 110 | unsigned int enable; |
| 111 | while(extension[cmd_length]!='\0' && extension[cmd_length]!=',') |
| 112 | cmd_length++; |
| 113 | tmp=cmd_length; |
| 114 | while(extension[tmp]==',') |
| 115 | tmp++; |
| 116 | if(strncmp(&extension[tmp], "enable", 6) == 0) |
| 117 | { |
| 118 | enable=1; |
| 119 | tmp+=6; |
| 120 | } |
| 121 | else if(strncmp(&extension[tmp], "disable", 7) == 0) |
| 122 | { |
| 123 | enable=0; |
| 124 | tmp+=7; |
| 125 | } |
| 126 | else |
| 127 | return 0; |
| 128 | for(file_enable=&files_enable[0];file_enable->file_hint!=NULL;file_enable++) |
| 129 | { |
no test coverage detected