frama-c

2熱度

1回答

我使用frama-C WP並希望調試我的ACSL註釋（瞭解爲什麼證明者說我「不知道」）。我有一些綠色或橙色的結果。我打開why3 IDE並查看生成的腳本。然後我從列表中選擇一個理論/目標，並能夠啓動Alt-Ergo或Coq IDE。我想在Coq IDE中使用生成的代碼。我看到一些公理定理，然後WP 然後，例如： intros a a_1 i_3 i_2 i_1 i t_2 t_1 t t_8 t

1熱度

1回答

WP全球不變

我已經在Linux上安裝了最新的frama-c發行版（磷），，並試圖定義一個全局不變量，但得到了WP尚不支持的消息。那是什麼狀態？是否有關於ACSL語言支持的文檔？謝謝。

0熱度

2回答

斷言上指針陣列

我已經定義下面的函數，其是公由郵資-C證明： //ensures array <= \result < array+length && *\result == element; /*@ requires 0 < length; requires \valid_read(array + (0 .. length-1)); assigns \nothing;

3熱度

1回答

如何在frama-c中調試ACSL？

我在努力學習ACSL，但是試圖編寫一個完整的規範時磕磕絆絆。我的代碼 #include <stdint.h> #include <stddef.h> #define NUM_ELEMS (8) /*@ requires expected != test; @ requires \let n = NUM_ELEMS; @ \valid_read(expected +

0熱度

2回答

如何強制內存位置在ACSL中有效？

我定義設備訪問如從而 volatile struct mydevice * const dev = (struct mydevice *)MY_DEVICE_ADDRESS; 我建模使用 @ volatile dev->somereg reads somereg_read writes somereg_write; 現在的問題是，當我使RTE檢查，所產生的有效性檢查不能證明的訪問 /*@

1熱度

1回答

郵資-C，非確定性的浮點值

作爲例子，我使用下面的函數： float nondet_float(){ float x; return x; } int main(){ float x = nondet_float(); if(isnan(x)){ some_error(); } } 我不知道如何必須使用郵資-C，來模擬非確定性浮動。我想要的是，變量x被

1熱度

1回答

可溼性粉劑困惑指針結構

我努力讓WP驗證交換2結構的函數的後置條件。 typedef struct { int x; int y; } pair; /*@ requires \valid({p, q}); assigns *p, *q; ensures *p == \old(*q); ensures *q == \old(*p); */ void swap(pair *p,

3熱度

1回答

如何在Ubuntu 14.04上爲Frama-c安裝影響分析插件？

我安裝郵資-C在Ubuntu 14.04，使用下列命令： sudo apt-get install frama-c 然而，當我使用下面的命令打開郵資-C的GUI： frama-c-gui 我無法找到左側窗口中的「Impact Analysis」插件。此圖顯示了我的郵資-C的當前可用的插件：我也提到了Frama-c web page卻找不到任何聯繫我下載或安裝的影響分析插件。如何在Ub

0熱度

1回答

Frama-c生成一個圖形對象，而不是點文件

我試圖找到兩個程序是否是gamma-isomorphic或不是我正在使用Jgrapht庫的幫助。現在，我必須生成程序的程序依賴圖並將其作爲圖對象捕獲。使用frama-c我們可以生成pdgs。我使用frama-c -pdg -pdg-dot graph -pdg-print program.c來生成程序的pdg，輸出是點格式。我必須解析點格式來獲取圖表。取而代之的是，我能否像圖形對象那樣獲得圖形數據

1熱度

1回答

使用Frama-Clang插件時的錯誤

鑑於插件https://frama-c.com/frama-clang.html被認爲處於開發的「早期階段」，或許我目前運氣不佳。但是，如果任何人遇到了一個問題，像這樣的疑惑： [email protected]:~/code/c$ frama-c max.cpp [kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.