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 - шаблон glob, который используется для соответствия путям файлов, которые необходимо включить или исключить из проекта. Чтобы убедиться, что интерпретатор не расширяет шаблоны glob, которые вы передаете polyspace-configure, заключайте их в двойные кавычки.

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

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

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

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

-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.

  • The '*' символ сам по себе.

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

Поддержка