什麼是Splint中的「Fresh Storage」？

Question

我已經搜索了「新鮮存儲」的Splint文檔，並且發現了它，但沒有正式的定義。其他修飾符，如null或only，我理解並正在使用。我只是不確定什麼是新鮮的存儲空間。

的情況是這樣的：

void output_system_information(unsigned int frequency, unsigned int duration) { 

    unsigned int intervals = duration/frequency;         

    /* here I allocate some storage */                    
    System * my_system = malloc(sizeof(System));         

    SystemInfo* current, * total;             

    if (my_system == NULL) {              
    fprintf(stderr, "%s\n", "Aborting: failed malloc in output_system_informatioin"); 
    exit(EXIT_FAILURE);               
    }                    

    /* and here I initialize is in that function */            
    init_system(my_system);  
    total = tally_system_info(frequency, duration, my_system);      
    current = my_system->get_system_info();          

    /* Here I've removed a ton of print-line statements so that you don't have to see them */ 

    /* then the members and the struct get freed in this here dtor */ 
    delete_system(my_system);              
    free(current);                 
    free(total);                 

    return;                  
}    

這是一個家庭作業，但這個問題並沒有直接與功課要做。這是一個夾板問題。

Answer 1

術語新鮮存儲是指一個內存緩衝區，其中剛分配給您的程序。

警告「沒有公佈貯藏保鮮」是只是一個特例「只有存儲沒有公佈」，當緩衝區是由無法釋放它同樣的功能分配。