frama-c

2熱度

1回答

定義字符串長度的公理時，我需要使用reads子句。 /*@ predicate Length_of_str_is{L}(char *s, integer n) = (0 <= n) && \valid(s+(0..n)) && s[n] == 0 && \forall integer i; 0 <= i < n ==> s[i] != 0; axiomatic LengthAxiomat

3熱度

2回答

我是否在Frama-c

中獲得3地址代碼我剛開始開發一個正在進行某種別名分析的frama-c插件。我正在使用Dataflow.Backwards分析，現在我必須通過不同的賦值語句並收集一些關於左值的內容。 frama-c是否提供給我3地址代碼？我對左值的形狀（或任何內存訪問）有一些保證嗎？我的意思是，就像在菸灰或瓦拉中，最多有一個字段訪問，s.t.，對於a-> b-> c，會有一個臨時變量，如tmp = a-> b; T

2熱度

1回答

郵資-C/WP無法在

證明與\循環不變我無法證明2循環不變：如我所料 loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) ==> ((char*)m2)[i] == \at(((char*)m1)[i], Pre); loop invariant \forall integer i; 0 <= i < (\at(n, Pre) - n) =

4熱度

2回答

獲取導致進入OCaml中

一個字符串變量我有這個功能的工作，其打印出的offsetmap值： let pretty_offsetmap_original lv fmt offsetmap = begin match offsetmap with | None -> Format.fprintf fmt "<BOTTOM>" | Some off -> let typ = Some (

1熱度

1回答

C宏上的ACSL註釋

是否可以使用ACSL註釋C宏？如： /*@ assigns \nothing; behavior xmin: assumes x < y; ensures \result == x; behavior ymin: assumes y <= x; ensures \result == y; disjoin

2熱度

2回答

瞭解Frama-C切片機結果

我想知道是否可以用Frama-C做某種前向條件切片，我正在玩一些示例來了解如何實現這一點。我有這個簡單的例子，這似乎導致了一個不精確的切片，我不明白爲什麼。下面是函數我想切片： int f(int a){ int x; if(a == 0) x = 0; else if(a != 0) x = 1; return x; } 如果使用本說明書中： /*@ requ

3熱度

1回答

獲取數組索引變量及其在值分析中的值（Frama-C）

我想查詢Frama-C中的值分析插件以獲取它們的值。對於每個數組，它返回整個數組的值範圍。例如，如果指令是array[i] = 1;，我從值分析插件獲得了array[i]的結果= {1}。現在，例如， array[i]，我想獲取變量名稱i及其來自價值分析的值。下面是我的代碼示例 class print_VA_result out = object inherit Visitor.frama_c

2熱度

1回答

Frama-C中的條件切片

我最後一個問題（Understanding Frama-C slicer results）是一個精確的例子，但正如我所說的，我的目標是要知道是否有可能用Frama-C做一些條件切片（向前和向後）。可能嗎？更確切地說，我不能獲得此程序的精確切片： /*@ requires a >= b; @ assigns \nothing; @ ensures \result == a;

0熱度

1回答

錯誤，同時在cygwin中安裝frama-c

我想在cygwin中安裝frama-c並獲取以下錯誤，但我無法解釋它們。你能幫我解釋一下嗎？或者給我一個鏈接，告訴我獲取信息的位置？ Preparing Wp-Coq Sources Uncaught exception: Util.UserError("_", _) Makefile:49: recipe for target `depend' failed make[1]: *** [d

3熱度

1回答

驗證問題使用Jessie插件和Frama-C

我是Frama-C的新手，我想正確學習ACSL語法。我有這個虛擬示例，Jessie插件無法驗證第9和第12行。我錯過了什麼嗎？該功能進行驗證（等於）將檢查兩個數組（a和b）具有相同的值或無法在每個索引處： /*@ requires \valid_range(a,0,n-1); requires \valid_range(b,0,n-1); requires n >=