| 1936 | #if defined(MAIN_doc) |
| 1937 | #define BLOCKSIZE 65536u |
| 1938 | int main() |
| 1939 | { |
| 1940 | const char fn[] = "recup_dir.1/f0000000.doc"; |
| 1941 | unsigned char buffer[BLOCKSIZE]; |
| 1942 | file_recovery_t file_recovery_new; |
| 1943 | file_recovery_t file_recovery; |
| 1944 | file_stat_t file_stats; |
| 1945 | |
| 1946 | /*@ assert \valid(buffer + (0 .. (BLOCKSIZE - 1))); */ |
| 1947 | #if defined(__FRAMAC__) |
| 1948 | Frama_C_make_unknown((char *)buffer, BLOCKSIZE); |
| 1949 | #endif |
| 1950 | |
| 1951 | reset_file_recovery(&file_recovery); |
| 1952 | file_recovery.blocksize=BLOCKSIZE; |
| 1953 | file_recovery_new.blocksize=BLOCKSIZE; |
| 1954 | file_recovery_new.data_check=NULL; |
| 1955 | file_recovery_new.file_stat=NULL; |
| 1956 | file_recovery_new.file_check=NULL; |
| 1957 | file_recovery_new.file_rename=NULL; |
| 1958 | file_recovery_new.calculated_file_size=0; |
| 1959 | file_recovery_new.file_size=0; |
| 1960 | file_recovery_new.location.start=0; |
| 1961 | |
| 1962 | file_stats.file_hint=&file_hint_doc; |
| 1963 | file_stats.not_recovered=0; |
| 1964 | file_stats.recovered=0; |
| 1965 | register_header_check_doc(&file_stats); |
| 1966 | if(header_check_doc(buffer, BLOCKSIZE, 0u, &file_recovery, &file_recovery_new)!=1) |
| 1967 | return 0; |
| 1968 | /*@ assert file_recovery_new.file_size == 0; */ |
| 1969 | /*@ assert file_recovery_new.file_check == &file_check_doc; */ |
| 1970 | /*@ assert file_recovery_new.file_rename == &file_rename_doc; */ |
| 1971 | /*@ assert valid_read_string(file_recovery_new.extension); */ |
| 1972 | /*@ assert \separated(&file_recovery_new, file_recovery_new.extension); */ |
| 1973 | #ifdef __FRAMAC__ |
| 1974 | file_recovery_new.file_size = 512*Frama_C_interval(1, 1000); |
| 1975 | #endif |
| 1976 | /*@ assert valid_read_string((char *)&fn); */ |
| 1977 | memcpy(file_recovery_new.filename, fn, sizeof(fn)); |
| 1978 | /*@ assert valid_read_string((char *)&file_recovery_new.filename); */ |
| 1979 | /*@ assert valid_read_string((char *)file_recovery_new.filename); */ |
| 1980 | /*X TODO assert valid_read_string(file_recovery_new.extension); */ |
| 1981 | file_recovery_new.file_stat=&file_stats; |
| 1982 | if(file_recovery_new.file_stat!=NULL) |
| 1983 | { |
| 1984 | file_recovery_t file_recovery_new2; |
| 1985 | /* Test when another file of the same is detected in the next block */ |
| 1986 | file_recovery_new2.blocksize=BLOCKSIZE; |
| 1987 | file_recovery_new2.file_stat=NULL; |
| 1988 | file_recovery_new2.file_check=NULL; |
| 1989 | file_recovery_new2.location.start=BLOCKSIZE; |
| 1990 | file_recovery_new.handle=NULL; /* In theory should be not null */ |
| 1991 | header_check_doc(buffer, BLOCKSIZE, 0, &file_recovery_new, &file_recovery_new2); |
| 1992 | /*@ assert valid_read_string((char *)file_recovery_new.filename); */ |
| 1993 | } |
| 1994 | /*@ assert valid_read_string((char *)file_recovery_new.filename); */ |
| 1995 | { |
nothing calls this directly
no test coverage detected