0

以下の C 関数では、最新バージョンの Frama-c の Alt-Ergo から構文エラーが発生します。

frama-c -wp -wp-rte -lib-entry  RoundNearestFive.c   -wp-out temp -wp-model="nat, real"

この生成された行の何が問題なのかわかりません:

 ...
      let r_0 = dat_0 / 5.0e0 : real in   /* syntax error here */
    ...

解析中の C 関数

typedef unsigned short int uint16;


/*@
  @ requires 0<=dat<= 300;
*/
uint16 RoundNearestFive(float dat)
{
    uint16 result= 0;
    float fra = 0;

    result = (uint16)(dat/5);

    fra = dat - (float)result*5; // fractional part of the input

    if (fra < 2.5)
        result = (uint16) (dat-fra);
    else
        result = (uint16) (dat+(5-fra));

        return result;
}
4

2 に答える 2

3

以下の式で Alt-Ergo (バージョン 0.95.2 およびトランク) を試しましたが、構文エラーは発生しませんでした。古いバージョンの Alt-Ergo を使用していますか? または、構文エラーが別の場所にある可能性があります。

--

論理 dat_0 : 実数

ゴール g: let r_0 = dat_0 / 5.0e0 : real in (* ここで構文エラー *) false

于 2014-01-08T20:05:09.547 に答える
3

WPのユーザー マニュアルには、Alt-Ergo の 0.95 より前のバージョンはサポートされていないと明記されています (21 ページを参照)。

于 2014-01-09T00:53:05.247 に答える