пытается сделать работу frama-c на Windows 7, используя Perl или MinGW или

Question

Я хочу использовать frama-c для статического анализа кода C. Мне уже потребовалось некоторое время, чтобы установить его (надеюсь) правильно. Файлы находятся по адресу C:\CodeAnalysis\frama-c. Я хочу, чтобы применить его с помощью консоли Windows, например:

C:\CodeAnalysis\frama-c\bin\frama-c hello.c

hello.c только простой привет-мир-программа (я нет C программист кстати и новичок в программировании)

#include <stdio.h> 

main() 
{ 
printf("Hello World \n"); 
} 

Так при выполнении указанной выше команды есть следующий вывод:

[kernel] preprocessing with "gcc -C -E -I. hello.c" 
C:/Strawberry/c/x86_64-w64-mingw32/include/stdio.h:141:[kernel] user error: syntax error 
[kernel] user error: skipping file "hello.c" that has errors. 
[kernel] Frama-C aborted: invalid user input 

Да, у меня установлен Perl, но понятия не имею, почему Frama использует его. Мне кажется, что что-то не так с stdio.h. Может ли это быть? Но я могу успешно скомпилировать свою программу.

C:\Strawberry\c\bin\gcc hello.c производит хорошо работающий файл exe.

При удалении оператора включить из файла, есть следующий вывод:

[kernel] preprocessing with "gcc -C -E I. hello.c" 
hello.c:5:[kernel] warning: Calling undeclared function printf. Old style K&R code? 

Так Frama себе делает работу, и это своего рода выход я ожидал получить.

Я также установил MinGW и попытался использовать Frama для компиляции. Поэтому я удалил записи Strawberry на моем пути к Windows. После этого вызов frama-c производит одинаковый вывод.

Когда полностью удаляется Strawberry Perl, frama не работает (указывая gcc - неизвестная команда), хотя C:\MinGW\mingw64\bin также добавлен в мой путь к Windows, даже в качестве первой записи.

C:\MinGW\mingw64\bin\gcc hello.c работ, gcc hello.c нет.

Когда установлен Perl gcc hello.c работает, даже когда я удаляю части клубники из переменной пути Windows. WTF?

Как я могу заставить все работать правильно?

Answer 1

Здесь есть несколько вопросов, и мы должны их изолировать, чтобы исправить ситуацию.

1. Strawberry Perl устанавливает свой собственный GCC (на основе MinGW), Binutils заголовки C и т.д., по умолчанию в директории C:\Strawberry\c\bin. Он добавляет этот каталог (среди прочих) в переменную Windows Path. Frama-C ожидает, что gcc будет в пути, и именно Windows решает, какой gcc выбрать, если в пути есть несколько каталогов, содержащих двоичный код gcc. Вот почему Frama-C, похоже, использует его.

2. Одна из распространенных ошибок (не зависящих от Windows, но чаще всего возникающих в Windows из-за характера ее графических приложений) заключается в изменении переменных среды и забывании перезапуска процессов, которые по-прежнему имеют старые копии (такие в командной строке). echo %path% должен подтвердить, какие каталоги присутствуют в пути для текущей командной строки, если есть какие-либо сомнения относительно его значения.

3. В случае echo %path% содержит ожидаемое значение, это то, что могло бы произойти (к сожалению, я не могу воспроизвести конфигурацию, чтобы проверить его тщательно): во время установки Фрама-C, он может использовать параметры, присутствующие во время установки выбрать, какой каталог содержит gcc (в вашем случае, C:\Strawberry\c\bin), а затем hardcode этот каталог в его скриптах.

   Это может объяснить, почему после удаления Strawberry Perl, даже если другой gcc находился на пути, он не рассматривался Frama-C. В идеале, переустановка Frama-C с одним gcc в пути может позволить ему найти нужную версию на этот раз. Обратите внимание, что это всего лишь гипотеза, я могу быть совершенно неправой.

   В любом случае основная проблема, с которой вы сталкиваетесь, заключается не в самой gcc, а в заголовках, входящих в состав Strawberry Perl, как объясняется в следующем элементе.

4. Что касается сообщений об ошибке:

   C:/Strawberry/c/x86_64-w64-mingw32/include/stdio.h:141:[kernel] user error: syntax error 
   [kernel] user error: skipping file "hello.c" that has errors. 
   

   Это действительно не очень информативен и может измениться в будущих версиях, но это не указует на исходную строку, которая вызывает ошибку (файл stdio.h, строка 141):

   int __cdecl __mingw_vsscanf (const char * __restrict__ _Str, 
       const char * __restrict__ Format,va_list argp); 
   

   В частности, представляется, что __restrict__ является источником ошибки здесь (Frama-C Натрий принимает restrict и __restrict, но не __restrict__ ; это может измениться в будущих версиях).

   К сожалению, даже фиксируя это (путем добавления, например, #define __restrict__ restrict перед тем #include <stdio.h> в файле) не гарантирует, что остальная часть файла будет анализироваться, так как, кажется, Windows, специфическим, C++ - склонный заголовок, вероятно, содержит другие определения/расширения C, которые не входят в стандарт C99 и, возможно, не принимаются Frama-C.

Лучшим решением было бы обеспечить Frama-C использует свой собственный stdio.h заголовок, вместо клубники в Perl. Обычно он устанавливается в share/frama-c/libc (то есть он может быть в C:\CodeAnalysis\frama-c\share\frama-c\libc в вашей установке), но в зависимости от вашей конфигурации заголовки, возможно, не были найдены во время выполнения, а заголовки Strawberry Perl были включены.

Быстрый хак для этого конкретного случая может быть замена:

#include <stdio.h> 

с:

#include "C:\CodeAnalysis\frama-c\share\frama-c\libc\stdio.h" 

Но это далеко от идеала и может привести к другим ошибкам.

Если вам удастся выяснить, как предотвратить включение заголовков Strawberry Perl, и вместо этого включить заголовочные файлы Frama-C, вы сможете запустить Frama-C.

Примечание о пути Cygwin/MinGW вопросы

У меня были некоторые проблемы при использовании компилятора MinGW и Cygwin построить (что не обязательно хорошая идея), так вот некоторые краткие инструкции о том, как построить Frama-C натрия с MinGW на основе OCaml компилятором, используя оболочку Cygwin (но не Cygwin на основе OCaml компилятор), в случае, если это может помочь кому-то:

1. при запуске ./configure, вам нужно для указания --prefix с использованием пути на базе Windows вместо базы Cygwin d один, таких как:

   ./configure --prefix="C:/CodeAnalysis/build"

   Если вы этого не сделаете, при запуске FRAMA-C (после make/make install) он не сможет найти файл libc/__fc_builtin_for_normalization.i, потому что он будет пытаться использовать Cygwin на основе пути, который не будет работать с компилятором OCaml на основе MinGW.

   Обратите внимание, что при указании пути префикса вы не можете использовать обратную косую черту (\), так как они не будут корректно преобразованы позже.

2. мне пришлось использовать следующую команду, чтобы обеспечить Makefile работал правильно:

   make FRAMAC_TOP_SRCDIR="$(cygpath -a -m $PWD)"

   Опять же, это связано с путями Cygwin не признаваемых компилятором MinGW (в частности, абсолютные пути используемые плагинами).

3. Предыдущих шагов достаточно для компиляции и запуска Frama-C (плюс GUI, если у вас установлены lablgtk и другие зависимости). Однако все еще есть некоторые проблемы, например. абсолютные имена файлов Windows не всегда обрабатываются правильно. Этого часто можно избежать, указав имена файлов непосредственно в командной строке с относительными путями (например, frama-c-gui -val hello.c), но в общем случае MinGW + Cygwin не является очень надежной комбинацией, и могут возникнуть другие проблемы.

В целом, смешивание Cygwin и MinGW это не очень хорошая идея из-за проблем пути, но тем не менее, можно скомпилировать и запустить FRAMA-C в таких условиях.