frama-c

    2

    1答えて

    Fedora 21では、すべての前提条件をインストールした後に、ソースからFrama-Cアルミニウムディストリビューションをコンパイルしました。 OCamlの私のバージョンは4.02.3です。 Frama-CとFrama-CのGUIはうまく動作します。私はFrama-C Plug-In Development Guideのセクション2.3、 "ViewCfgプラグイン"に従おうとしています。しかし

    1

    1答えて

    統合の仕方 Jessieの外部プラグイン(なぜ2.36)を Frama-cで表示しますか?

    2

    1答えて

    これまでのところ、STANCEプロジェクト(Stance project website)の読者(found on the website)とプレゼンテーション(also found on the website)が見つかりました。また、6月20日にframa-cangが開催され、frama-clangが導入される予定です。 しかし、私はframa-clangで遊ぶ実装があるかどうか疑問に思ってい

    1

    2答えて

    私はすべての種類の変数の値を解決するはずのframa-cプラグインに取り組んでいます。私はポインタと構造体とtypedefを逆参照し、対応する値を出力しました。 今、私は配列の値を得るのに苦労しています。 | TArray (typ, exp, bitsSizeofTypCache, attributes) -> ( let len = Cil.lenOfArray exp in

    3

    1答えて

    追加操作用shortとcharデータ型のオーバーフローを確認しながら、FRAMA-Cによって挿入されたアサーションがあるが正しくないと思われる:charの と短いデータでは正の最大値と負の値は整数データ型です。 この理由は何ですか?

    1

    1答えて

    CTRLスライスの取得に問題があります。 私はこれを実行して、OpenSSLを分析しようとしている: コードは何も生じない int dtls1_process_heartbeat(SSL *s) { unsigned char *p = &s->s3->rrec.data[0], *pl; unsigned short hbtype; unsigned i

    0

    2答えて

    私はopam(Ubuntu 16.04上)を使ってframa-cをインストールしました。私はこのエラーを解決するにはどうすればよい /home/amira/.opam/system/share/frama-c/Makefile.dynamic:295: .depend: Aucun fichier ou dossier de ce type /home/amira/.opam/syst

    2

    1答えて

    ACSL implementation(アルミニウムのバージョン1.11実装 - 20160501)には、丸めモードとして\NearestEvenが記載されています(23ページ)。ただし、実行時にまだ利用可能ではないようです。次のコマンドを使用して /*@ requires 0x1p-967 <= C <= 0x1p970; @ ensures \result == \round_dou

    2

    1答えて

    Frama-Cフッ素版のプラグインをFrama-Cアルミニウムに移行しようとしています。そうすると、機能Db.Value.AfterTable.findの適切な置き換えが見つからない。私が見つけた最も近いものはDb.Value.AfterTable_By_Callstack.findである。しかし、この関数はFrama-Cフッ素にDb.Value.stateではなく、Db.Value.AfterT

    2

    1答えて

    私はいくつかのACSLアサーション(file.c)を含むファイルを持っている:私はコマンドを使用して、すべてのアサーションのためにスライスしたい #include <stdio.h> #include <stdlib.h> void foo() { int a=0; //@ assert(a==0); } void print(const char* text) {