frama-c

2熱度

1回答

我有一個包含文件數ACSL斷言（file.c）： #include <stdio.h> #include <stdlib.h> void foo() { int a=0; //@ assert(a==0); } void print(const char* text) { int a=0; //@ assert(a==0); print

0熱度

1回答

Frama-C-Plugin：將指針解析爲指針

我正在開發一個frama-c-plugin，我想獲取指針的值（不是指向它們的地址，而是指向該地址的值）。這對於簡單的指針來說工作至今。現在我想處理指針的指針。例如： int k=12; int *l=&k; int **m = &l; int ***n = &m; 在分析這個代碼與我的實際版本，我得到的值： k=12 l=12 m=&k n=&l 但我希望這些值： k=12

2熱度

1回答

Frama-C鋁「未綁定模塊GMenu」

在Fedora 21上，我在安裝完所有必備軟件之後，從源代碼編譯了Frama-C鋁合金發行版。我的OCaml版本是4.02.3。 Frama-C和Frama-C GUI工作正常。我正在嘗試關注Frama-C Plug-In Development Guide的第2.3節「ViewCfg插件」。然而，在第2.3.4節「擴展郵資-C GUI」後，我添加了GUI擴展代碼，並使用「-load腳本」選項運行

2熱度

1回答

frama-clang的實現

到目前爲止，我發現STANCE項目（Stance project website）是一個閱讀器（found on the website）和演示文稿（also found on the website）。另外，顯然6月20日將會有一個frama-c的日子，屆時將引入frama-clang。但是，我想知道是否有一個實現與frama-clang一起玩。

1熱度

2回答

郵資-C插件：解決陣列值

我工作的一個郵資-C插件，應該可以解決各種可變因素的值。我設法取消引用指針和結構和typedefs並打印相應的值。現在我有得到一個數組的值掙扎。這裏是我的方法，到目前爲止，以下的描述： | TArray (typ, exp, bitsSizeofTypCache, attributes) -> ( let len = Cil.lenOfArray exp in let rec

1熱度

1回答

日食的Frama-C開發：自動完成在某些情況下不起作用

我正在開發一個Frama-C插件。我使用Eclipse進行開發。如果我編寫「正常」OCaml函數調用（自己的函數和系統函數），工具提示會顯示我可用的函數。例如：如果我輸入String.i eclipse提供了String.iter和其他函數作爲可能性在一個框中。如果我想調用frama-c函數，如Ast.g對於Ast.get()或Db.Value.，這不起作用，沒有提供匹配函數的信息。是否可

2熱度

1回答

價值分析界定

我用下面的結構分析的控制程序： unsigned int cnt=0; unsigned int inc=3; ... void main(){ int i; int lim; for(i=0;i<100000;i++) { f1(); .... lim = f2(); if(cnt < lim) cnt += inc; .... }

0熱度

2回答

在ubuntu上安裝hello_world插件時出現錯誤16.04

我已經使用opam（在Ubuntu 16.04上）安裝了frama-c。我嘗試使用一個Makefile FRAMAC_SHARE :=$(shell frama-c.byte -print-path) FRAMAC_LIBDIR :=$(shell frama-c.byte -print-libpath) PLUGIN_NAME = Hello PLUGIN_CMO

2熱度

1回答

Frama-c Aluminum-20160501是否提供「\ NearestEven」？

ACSL implementation（Aluminum-20160501版本1.11實施）列出了\NearestEven作爲舍入模式（第23頁）。但是，它似乎在運行時仍然不可用。使用以下命令 /*@ requires 0x1p-967 <= C <= 0x1p970; @ ensures \result == \round_double(\NearestEven, (x+y)/2) ;

1熱度

1回答

Frama-C：使用指針時獲取函數輸出

我需要獲取函數的所有輸出列表。當我使用From -plugin以下代碼 void add(int *sum, int a, int b) { *sum = a + b; } int main() { int result; add(&result, 1, 2); } 它告訴我，result是add函數的輸出。這當然是正確的，但我希望插件在某處提到sum