Frama-C: компиляция в Cygwin / Windows 8.1

Легкий вопрос для тех, кто компилирует C для windows!

Я хочу использовать последнюю версию статического анализатора Frama-C C и его графический интерфейс в Windows 8. Пока Насколько я могу судить, самая последняя версия, в которой есть установщик Windows, - это Boron, которой около 3-4 лет. Похоже, мне нужно самому скомпилировать его (версия фтор 3). Однако я спотыкаюсь на первых шагах.

Инструкции по быстрой компиляции для Frama-C Fluorine 3: здесь.

  • Шаг 1. Установите OCaml. Я установил версию для Windows с здесь.

  • Шаг 1b: я считаю, что шаг 1 установил Gtk и так далее.

  • Шаг 2b: Запустите:

    ./configure --prefix C:/windows/path/with/direct/slash && make && make install

4 вещи в этих инструкциях сбивают меня с толку:

  1. Какой configure файл это должен быть? Если я открываю терминал Cygwin, он попадает в домашний каталог пользователя, а если я запускаю ./configure, он говорит, что такого файла или каталога нет. Я думаю, это означает ссылку на один из файлов конфигурации в источнике, но их более 10.

  2. На что именно указывает C:/windows/path/with/direct/slash? Пожалуйста, не мог бы кто-нибудь дать мне реальный пример с хорошим объяснением?

  3. В каком каталоге мне следует запускать указанную выше команду (шаг 2b)?

  4. В какой каталог мне поместить извлеченный исходный код Frama-C? (И мне просто извлечь каталог src из архива, или мне понадобится все содержимое?)

Все, что я пытаюсь сделать, это следовать их краткому примеру, на который есть ссылка на их домашней странице , используя последнюю версию в Windows 8.1, и для этого мне нужно руководство Absolute Dummies!

Большое спасибо


c windows compilation windows-8.1 frama-c
person CL22    schedule 19.02.2014    source источник
comment
Если у вас есть дисковое пространство + пропускная способность интернета, простейшая установка - это дистрибутив Linux внутри виртуальной машины. В последней версии Ubuntu, «дерзкой», есть пакет frama-c (20111001 + азот). Это уже лучше, чем последний двоичный файл Windows Frama-C. Вы можете улучшить это, указав диспетчеру пакетов Ubuntu установить все зависимости времени компиляции пакета Frama-C Nitrogen, как если бы вы хотели его скомпилировать самостоятельно, и скомпилировать последний Frama-C из исходного кода (зависимости меняются очень мало от одной версии Frama-C к другой).   -  person Pascal Cuoq    schedule 19.02.2014
comment
Магическая команда: apt-get build-dep frama-c (ссылка: lists.gforge .inria.fr / pipermail / frama-c-Discuss / 2013-август /).   -  person Pascal Cuoq    schedule 19.02.2014

Ответы (3)


arrow_upward
1
arrow_downward

Я наткнулся на ваш вопрос, потому что меня тоже смутила инструкция «with / direct / slash». По крайней мере, я могу помочь с другими вашими вопросами:

  1. По соглашению, это всегда файл конфигурации в корневом каталоге тарбола. Итак, извлеките файл tar.gz, а затем перейдите в каталог, который создает и запускает ./configure оттуда.

  2. --prefix определяет путь установки, поэтому я предполагаю, что эта опция должна поместить исполняемый файл в какой-то каталог, легко доступный из Windows (например, каталог Program Files). Я не уверен, что такое «прямая косая черта». Обычно корневой каталог Cygwin на самом деле представляет собой некоторый каталог на диске C: (например, C: \ cygwin), поэтому для доступа к остальной части файловой иерархии обычно в корневом каталоге Cygwin есть подключенное монтирование под названием «cygdrive». Таким образом, вы можете перейти к широкой иерархии из Cygwin, используя что-то вроде '/ cygdrive / c / path / to / windows / directory'. Использование «C: /» в Cygwin немного странно. Что бы это ни стоило, я бы просто принял значение по умолчанию (без флага --prefix) или указал бы что-то в иерархии Cygwin, например '/ usr / local / bin', и просто запустил бы его оттуда.

  3. Из указанного вами каталога '--prefix', потому что там будет исполняемый файл. Если вы оставите одно из значений по умолчанию, вы можете запускать исполняемый файл из любого места, потому что он будет где-то в вашем PATH.

  4. Распакуйте все это в какой-нибудь рабочий каталог в вашей домашней папке. После того, как вы его установили (что и делает ./configure && make && make install), вы можете выбросить извлеченный архив.

person Heath Raftery    schedule 02.06.2014

arrow_upward
0
arrow_downward

Обновленные инструкции по компиляции Frama-C в Windows доступны на вики-странице Frama-C, протестированы как на Windows 7, так и на Windows 8.1.

Эти инструкции официально не поддерживаются, но они должны помочь пользователям скомпилировать и установить Frama-C с помощью OPAM (диспетчера пакетов OCaml).

Кроме того, поскольку между последними версиями Windows нет существенных различий в процедуре, некоторые ответы на этот вопрос также могут быть применимы к вашему кейс.

person anol    schedule 04.02.2016

arrow_upward
-1
arrow_downward

В Windows 10 для успешной установки frama-c выполнялись следующие инструкции:

  1. Включение WSL в Windows 10

https://docs.microsoft.com/en-us/windows/wsl/install-win10

Ubuntu теперь должен быть доступен в меню Windows. Запустите его и следуйте инструкциям по созданию пользователя.

  1. Для установки opam,

    1. sudo add-apt-repository -y ppa:snwh/ppa
    2. sudo apt update
    3. sudo apt upgrade
    4. sudo apt install make m4 gcc opam

  2. opam можно настроить с помощью:

    1. opam init --disable-sandboxing -c 4.07.0 --shell-setup

      Если есть ошибка переключателя opam, выполните эту команду:

      opam switch create 4.07.0

      Это загрузит и установит версию компилятора ocaml 4.07.0.

    2. eval $(opam env)

    3. opam install -y depext

  3. Для установки Frama-C выполните следующие команды:

    1. opam depext --install -y lablgtk3 lablgtk3-sourceview3
    2. opam depext conf-gnomecanvas
    3. opam depext conf-gtksourceview
    4. opam depext --install -y frama-c

    Это должно обработать около 70 файлов, и потребуется некоторое время для установки.

    1. eval $(opam config env)

    Снова перезапустите Ubuntu и, если возникла проблема с не найденной командой, снова выполните команду eval $ (opam config env) и используйте frama-c.

  4. После установки Frama-c 21.1 протестируйте:

    1. which frama-c
    2. which frama-c-gui

    Если обе команды показывают правильный каталог для установки, они будут выполнены успешно.

  5. После установки frama-c-gui, поскольку WSL не поддерживает графический интерфейс, я использовал mobaXterm.

    1. Install MobaXterm. Xserver comes by default with MobaXterm.
    2. Когда вы запускаете MobaXterm, справа вверху появляется значок Xserver. Щелкните это, чтобы начать.
    3. После запуска Xserver наведите указатель мыши на значок, чтобы увидеть IP-адрес графического интерфейса пользователя. Например, он покажет: 172.19.64.1:0.0. Обратите внимание на это.
    4. В Ubuntu export DISPLAY="172.19.64.1:0.0"
    5. Затем запустите frama-c-gui. Он откроется с использованием графического интерфейса Xserver.

Если вы используете Virtual Box и дистрибутив Linux, установленный в виртуальном боксе, выполните шаги 2–5 для установки. Для успешной установки выделите виртуальному ящику не менее 20 ГБ. frama-c-gui будет установлен, только если на диске выделено достаточно места.

person Rajathilagam    schedule 12.10.2020
comment
Windows 8.1 не поддерживает WSL. - person Mahler; 23.04.2021