frama-c

1熱度

1回答

在沒有主函數的C文件上運行Frama-C時，出現錯誤。是否有任何選項可以對這些C文件運行Frama-C值分析？

3熱度

1回答

我正在開發Frama-C中的一個插件。我想解析一個xml文件。我安裝了包libxml-light-ocaml-dev，但在編譯時出現「Unbound module Xml」錯誤。我不知道如何着手使包裝對Frama-C可見。或者我應該使用另一個包？

1熱度

1回答

確保證明代碼有缺陷？

在下面，當相關的C代碼被註釋掉時，行爲neg_limit的後置條件如何被證明是真實的？安全 - >檢查算術溢出之一是不可證明的，如預期的，但它似乎像neg_limit也應該是無法證明的。語境：我使用的郵資-C-硼，傑西，並通過gWhy，按住Alt鍵人體工程學，以學習如何編寫規範和證明功能的滿足他們。任何關於規範策略，工具等的提示，RTFMing等也是值得讚賞的。到目前爲止，我正在閱讀ACSL

5熱度

2回答

依賴無符號整數溢出的代碼證明？

我應該如何處理驗證代碼的正確性，以避免效率低下，依賴於模塊化算法？ #include <stdint.h> uint32_t my_add(uint32_t a, uint32_t b) { uint32_t r = a + b; if (r < a) return UINT32_MAX; return r; } 我已經嘗試過WP的「INT」的模

3熱度

1回答

類型檢查和代碼模式檢測，Frama-C

我在發現Frama-C軟件，我想知道是否有可能檢測到一些代碼模式，如加倍測試或例如調用給定函數總是跟着另一個。或者可能使用變量名稱的某些事情，例如檢查具有給定前綴名稱的變量是否屬於某種類型。您認爲Frama-C（使用ACSL或開發新模塊）可能嗎？非常感謝=）

3熱度

1回答

郵資-C禁用WP QED

當使用郵資-C WP與-wp時的選項，例如（使用swap.c示例）： swap.c // File swap.c: /*@ requires \valid(a) && \valid(b); @ ensures A: *a == \old(*b) ; @ ensures B: *b == \old(*a) ; @ assigns *a,*b ; @*/

0熱度

1回答

WP插件與Alt-Ergo - 無法證明？

我正在嘗試使用Alt-Ergo在相當複雜的功能上測試WP插件。不幸的是，我無法弄清楚下面給出的「基本」行爲有什麼問題。此行爲應該爲true，因爲沒有其他地方tenumRMode更新除了第一個條件語句的其他部分。奇怪的是，如果我隨意評論一些行，我總是會從Alt-ergo中獲得「有效」。有何評論？ /*@ behavior basic: @ assumes fRrValue == 0

1熱度

1回答

郵資-C使用7

我已經安裝了Windows安裝程序的硼版本從框架-C網站http://frama-c.com/download.html ，當我嘗試運行VAL插件，我得到有關預處理程序錯誤varaible CPP沒有被設置爲如下： C:\Frama-C\bin>frama-c.exe -val filename.cpp [kernel] user error: failed to run: gcc -C -E

1熱度

2回答

ACSL中的PreCondition或PostCondtion

我無法區分ACSL中的各種先決條件和後置條件。正如我所知道的那樣，要求，終止並承擔前提條件並確保在後置條件下進行分配。但是像減少等的休息是？任何機構都可以幫助我找出？在此先感謝

0熱度

1回答

哪個Frama-C版本最適合開發切片插件？

我想探索Frama-C應用基於斷言的切片（使用ACSL符號）。我發現有幾個不同版本的Frama-C具有一些不同的功能。我的問題是哪個版本最適合爲Frama-C開發切片插件，以及如何操作由Frama-C創建的AST。