假設我們有下面的C註釋代碼： #define L 3
int a[L] = {0};
/*@ requires \valid(a+(0..(L - 1)));
ensures \forall int j; 0 <= j < L ==> (a[j] == j); */
int main() {
int i = 0;
/*@ loop assigns i, a[
我試圖從Ubuntu 14.04的源代碼安裝frama-c，但這是不可能的。 氟使錯誤： [email protected]:~/Área de Trabalho/frama-c-Fluorine-20130601$ make
Generating src/lib/dynlink_common_interface.ml
Generating src/kernel/config.ml
Gen
相應的局部變量的聲明*我爲了得到這是一點對應的局部變量的聲明節點，在我的情況「VAL」寫這個劇本程序C但我得到錯誤意外的錯誤（Not_found）。我想，我沒有給正確的論點我的方法特別本地化它的類型是Cil_types.localisation如果有人可以幫助我... * let main() =
let memo_debug = Kernel.Debug.get() in
K