Exponenta Banner
exponenta event banner

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

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

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

Чтобы попробовать эти примеры, используйте демонстрационные файлы в polyspaceroot\help\toolbox\codeprover\examples\sources-select. 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
Поддержка