Плагин WP: ошибка синтаксиса Alt-Ergo

Question

Плагин WP: ошибка синтаксиса Alt-Ergo

Для функции C ниже я получаю синтаксические ошибки от Alt-Ergo для последней версии Frama-c.

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;
}

0

frama-c

Источник

user3150318 08 янв '14 в 18:45

2 ответа

Другие вопросы по тегам frama-c

user1295435 09 янв '14 в 00:53 2014-01-09 00:53 · Answer 1 · 2014-01-09 00:53

В руководстве пользователя WP прямо указано, что версии Alt-Ergo до 0.95 не поддерживаются (см. Стр. 21).

3

Источник

user1295435 09 янв '14 в 00:53

user2513000 08 янв '14 в 20:05 2014-01-08 20:05 · Answer 2 · 2014-01-08 20:05

Я попробовал Alt-Ergo (версия 0.95.2 и транк) по формуле ниже, и я не получил синтаксическую ошибку. Вы используете старую версию Alt-Ergo? Или, может быть, синтаксическая ошибка в другом месте.

-

логика dat_0: реальная

цель g: пусть r_0 = dat_0 / 5.0e0: действительное число (* синтаксическая ошибка здесь *) false