Exponenta Banner
exponenta event banner

polyspace-configure Синтаксис выбора исходных файлов

Когда вы создаете проекты при помощи polyspace-configure, можно включать или исключить исходные файлы, пути которых совпадают с шаблоном, что вы передаете опциям -include-sources или -exclude-sources. Можно задать эти две опции многократно и объединить их в командной строке.

Эта структура папок применяется к этим примерам.

Чтобы попробовать эти примеры, используйте демонстрационные файлы в polyspaceroot\help\toolbox\polyspace_code_prover_server\examples\sources-выбрать. polyspaceroot папка установки Polyspace®.

Запустите эту команду:

polyspace-configure -allow-overwrite -include-sources "glob_pattern" \
-print-excluded-sources -print-included-sources make -B
glob_pattern шаблон шарика, который вы используете, чтобы совпадать с путями файлов, которые вы хотите включать или исключить из вашего проекта. Гарантировать интерпретатор не расширяет шаблоны шарика, которые вы передаете polyspace-configure, заключите их в двойные кавычки.

В таблице примеры принимают тот sources папка верхнего уровня.

Синтаксис шаблона шарикаПример

Никакие специальные символы, наклонные черты (' / '), или обратные косые черты (' \').

Шаблон совпадает с соответствующими файлами, но не папками.

-include-sources "main.c" соответствия:

/sources/app/main.c

Шаблон содержит '*' или '?' специальные символы.

'*' нуль соответствий или больше символов в имени файла или имени папки.

'?' соответствия один символ в имени файла или имени папки.

Соответствия не включают диафрагмы пути.

-include-sources "b?.c" соответствия:

/sources/lib/b/b1.c

/sources/lib/b/b2.c

-include-sources "app/*.c" соответствия:

/sources/app/main.c

Шаблон начинает с наклонной черты '/' (UNIX®) или буква диска (Windows®).

Шаблон совпадает с абсолютным путем только.

-include-sources "/a" ни с чем не совпадает.

-include-sources "/sources/app" соответствия:

/sources/app/main.c

Шаблон заканчивается наклонной чертой (UNIX), обратная косая черта (Windows) или '**'.

Шаблон совпадает со всеми файлами под заданной папкой.

'**' проигнорирован, если это в начале шаблона.

-include-sources "a/" соответствия

/sources/lib/a/a1.c

/sources/lib/a/a2.c

Шаблон содержит '/**/' (UNIX) или '\**\' Windows. Шаблон совпадает с нулем или большим количеством папок в заданном пути.

-include-sources "lib/**/?1.c" соответствия:

/sources/lib/a/a1.c

/sources/lib/b/b1.c

Шаблон запускается с '.' или '..'.

Шаблон совпадает с путями относительно пути, куда вы запускаете команду.

Если при запуске polyspace-configure от /sources/lib/a,

-include-sources "../lib/**/b?.c" соответствия:

/sources/lib/b/b1.c

/sources/lib/b/b2.c

Шаблон является путем UNC на Windows.

Если ваши файлы находятся на сервере myServer:

\\myServer\sources\lib\b\** соответствия:

\\myServer\sources\lib\b\b1.c

\\myServer\sources\lib\b\b2.c

polyspace-configure не поддерживает эти шаблоны шарика:

  • Абсолютные пути относительно текущего диска на Windows.

    Например, \foo\bar.

  • Относительные пути к текущей папке.

    Например, C:foo\bar.

  • Расширенные пути к длине в Windows.

    Например, \\?\foo.

  • Пути, которые содержат '.' или '..' кроме в начале шаблона.

    Например, /foo/bar/../a?.c.

  • '*' символ отдельно.

Документация Polyspace Code Prover Server

Поддержка