Я не могу открыть какие-либо файлы .C с помощью Frama-c и получаю только сообщения о недопустимых ошибках пользовательского ввода.

Я новичок в Frama-c и совсем новичок в программировании в целом. Я установил Frama-C на свой Mac. Я использую ОСХ. Из командной строки я ввожу Frama-C-Gui, который открывается нормально, и в это время я выбираю «Новый проект» Графический интерфейс Frama-C, затем добавление нового проекта

Я перемещаюсь по своим файлам, а затем выбираю ОЧЕНЬ простой файл .C, однако, когда я выбираю его, я получаю сообщение об ошибке:

«Прерыватель Frama-C: неверный пользовательский ввод. Возврат к предыдущему состоянию. Посмотрите на консоль дополнительную информацию (если она есть)».

Графический интерфейс Frama-C с сообщением об ошибке

Мой файл очень прост и просто цикл ниже:

for (int j=-100;j<=100;j++){i=j;
    while (i!=0){i=i+2; x=x-5; y=y-y/x;}}

Любая помощь в том, как успешно запускать файлы здесь, будет очень признательна!


frama-c
person Lukas Bell    schedule 04.04.2018    source источник
comment
Это не полная программа на языке C и даже не полная функция на языке C. Что вы ожидаете, что frama-c сделает с этим? Перед проверкой убедитесь, что он компилируется без каких-либо предупреждений.   -  person Jens    schedule 04.04.2018
comment
Мне дали 17 подобных циклов и проинструктировали выполнить для них анализ -val с использованием Frama-c для проверки завершения цикла. Возможно, для этого цикла нужен более крупный файл, который позволил бы ему успешно работать?   -  person Lukas Bell    schedule 04.04.2018
comment
Эти циклы неполные и бесполезные, так как, например, тот, который вы привели, даже не имеет инициализации для переменных x и y. Просто чтобы мы знали ваши навыки C: по шкале от 0 (никогда не писал hello world) до 10 (я выиграл IOCCC), каков ваш опыт C?   -  person Jens    schedule 04.04.2018
comment
Определенно 0. В плане программирования у меня есть некоторый опыт работы с Java и HTML, я понимаю основы и концепции программирования, однако я, конечно, не разработчик и никогда не работал с C.   -  person Lukas Bell    schedule 04.04.2018
comment
Сообщение об ошибке на снимке экрана гласит: Посмотрите на консоль дополнительную информацию (если она есть). Это означает вкладку Консоль в графическом интерфейсе. Если вы щелкнете по нему, оно должно содержать более описательное сообщение об ошибке. Кроме того, если вы начинаете использовать Frama-C/EVA (анализ -val), я рекомендую этот пост из блога Frama-C, который должен помочь с начальной настройкой: blog.frama-c.com/index.php?post/2017/03/07 /   -  person anol    schedule 05.04.2018
comment
(Хотя, как заметил Йенс, использование Frama-C требует некоторого знания языка C, оно не поможет вам изучить основы языка и не очень удобно для полных новичков в языке C.)   -  person anol    schedule 05.04.2018

Ответы (1)


arrow_upward
2
arrow_downward

Может быть, полная программа на C продвинет вас дальше. Для данного цикла сохраните его в foo.c желательно со строчными буквами .c.

int main(void) {
    int i, x = 0, y = 0;

    for (int j = -100; j <= 100; j++) {
         i = j;
         while (i != 0) {
              i = i + 2;
              x = x - 5;
              y = y - y / x;
         }
    }
    return 0;
}
person Jens    schedule 04.04.2018