frama-c

3熱度

1回答

-rte選項不健全的行爲我現在面臨與鎂版（直接從Ubuntu的安裝）-rte選項不連貫的行爲。我想知道是否有人知道這個問題，或者如果我做錯了什麼。我有一個陣列外部的不正確的存取權限的程序。在啓動frama-c-gui時，如果沒有選項和值分析，則會檢測出界限訪問，並用橙色圓圈顯示相應的註釋。使用-rte選項時，會顯示兩個註釋（數組的下限和上限），並顯示兩個綠色圓圈（這是不正確的）。 /*@ ass

3熱度

1回答

溢出無效斷言檢查郵資-C

當檢查用於加法運算short和char數據類型的溢流，通過郵資-C插入斷言是似乎是不正確的：對於char和短數據的最大正值和負值是整型數據類型。這可能是什麼原因？

4熱度

1回答

如何在Frama-C中定製機器依賴性？

我有一個16位的微處理器，這是不同於x86_16大小size_t,ptrdiff_t等不同大小的任何人可以給我詳細信息和明確的指示，如何定製在我的MPU的Frama-C的機器依賴項？

1熱度

1回答

由於自定義machdep在Frama-C中的語法錯誤

我正在爲我的應用程序使用MPLAB XC16 C編譯器。如果我使用machdep x86_16，則Frama-C正常工作。例如，我可以用這種方式啓動Frama-C： $ frama-c-gui machdep x86_16 -cpp-command 'C:\\"Program Files (x86)"\\Microchip\\xc16\\v1.26\\bin\\xc16-gcc.exe -E' -

2熱度

1回答

Db.Value.AfterTable.find更改爲Frama-C鋁

我正在嘗試將Frama-C氟版插件遷移到Frama-C鋁。這樣做時，我無法找到功能Db.Value.AfterTable.find的適當替代品，我找到的最接近的替代品是Db.Value.AfterTable_By_Callstack.find。但是，該功能現在返回不同類型，即Db.Value.AfterTable_By_Callstack.data = Db.Value.state Value_t

1熱度

1回答

是否可以在frama-c中指定緩衝區訪問子句？

假設我有以下功能： void process_data(uint32_t * data, size_t length) { for (size_t i = 0; i < length; i++) { foo(data[i]); } } 我怎麼能告訴郵資-C「這個功能，確保每次訪問data[i]滿足條件i < length」？據我所知，我可以在每行代碼data附

2熱度

1回答

將C源文件合併爲CIL

我想合併C源文件，就像我在CIL和cilly腳本中一樣。 Frama-c是否提供這種腳本功能？

0熱度

1回答

郵資-C界面警告MIME類型 '文本/ X-CSRC' 未找到

雖然上open suse 13.1運行 frama-c-gui aluminium 給出警告消息： [GUI]警告：MIME類型「文本/ x-csrc'找不到這是什麼原因和解決方案？

1熱度

1回答

Jessie插件與Frama-c鋁的集成

如何集成 Jessie外部插件（爲什麼2.36）與 Frama-c鋁？

0熱度

1回答

甚至對「死枝」做Frama-c顯示依賴關係

我正在使用frama-c鋁-20160502版本，我想在大型程序中找到依賴關係。在命令行中使用選項-deps時，我發現缺少一些依賴關係。特別是當幾個條件加入一個條件時，只要一個條件爲假，依賴性分析就會停止。在這個例子中的位置： #include<stdio.h> #include<stdbool.h> /*Global variable definitions*/ bool A = tru