1

frama-c と why3 をインストールしましたが、frama-c を起動しようとすると、jessie3 でエラーが発生します。

frama-c -verbose 2
[kernel] warning: cannot load plug-in `Jessie3' (incompatible with Neon-20140301).
The exact failure is: error loading shared library:
/usr/local/lib/framac/plugins/Jessie3.cmxs: undefined symbol: camlGzip

camlGzip に関する情報が見つからないため、構成ファイル (camlzip である可能性があります) でエラーになる可能性がありますが、宣言されている場所はわかりません。

編集: Jessie3.cmxs の camlzip で camlGzip を変更しようとしましたが、frama-c を起動するとセグメンテーション違反が発生します

私のframa-cとWhy3のバージョン：

frama-c -version
Version: Neon-20140301

why3 --version
Why3 platform, version 0.85 (build date: Wed Oct 29 10:42:47 CET 2014)

Mint17 仮想マシンで作業していますが、各プログラムの ./configure と make にエラーはありませんでした

誰かがすでにこの問題を抱えていて、私を助けてくれることを願っています

4

1 に答える 1

0

私はちょうどこの問題に遭遇し、それを修正しました。frama-c ライブラリに jessie をインストールするには、Why-2.34 をインストールする必要があります。このリンクからダウンロードしてください: https://opam.ocaml.org/packages/why/why.2.34/

正常にコンパイルするには coq を削除する必要があるため、コンパイルに問題がありました。ところで、coq コンパイル エラーを報告する方法を知っている人は助けてください。

また、Why3.85 を使用している場合は、3.83 にダウングレードすることをお勧めします。Why.2.34 で認識される唯一のバージョンのようです。

乾杯。

于 2014-12-01T00:50:22.050 に答える