Выкарыстанне Splint для праверки зыходнага коду ўбудаванага праграмнага забеспячэння

Кошт выпраўлення памылак залежыць ад этапу жыцця праграмы, на якім гэту памылку знайшлі. Чым раней знойдзена памылка - тым танней абыходзіцца яе выпраўленне. Такім чынам усе зацікаўлены не тварыць памылкі, пры тым, чым раней, тым лепш. У нашым неідэальным свеце праграмісты імкнуцца паменшыць верагоднасць памылак у праграмным забеспячэнні. Для гэтага існуе тэсціраванне ўжо канчатковага коду на адпаведнасць спецыфікацыі (так званае распрацоўка праз тэсціраванне, або TDD - Test Driven Development). Але на якасць праверкі уплывае дакладнасць праверак.

Дадаткова да тэстаў існуе статычны аналіз коду. Ён не правярае логіку працы, для гэтай мэты ёсць TDD, а дазваляе знайсці месцы, якія кампілятар і праграміст разумеюць па рознаму.

Існуе не шмат, але нейкая колькасць статычных аналізатараў, як камерцыйных, так і адкрытых. Спіс аналізатараў можна знайсці ў Вікіпедыі.

Зараз гаворка пойдзе пра Splint, а таксама пра яго выкарыстанне для праверкі ўбудаванага праграмнага забеспячэння.


Нажаль, Splint годны для праверкі толькі зыходнага коду, адпавядаючага стандарту C89, C99 ён не разумее і лічыць што код з памылкамі.

Аналізатар нічога не ведае пра ядро, на якім будзе выконвацца код, таксама нічога ён не ведае пра кампілятар. Такім чынам, перад намі стаіць задача зрабіць аналізатару асяроддзе, максімальна набліжанае да таго, якое робіць кампілятар.

Калі проста выканаць:

splint *.c

аналізатар будзе лічыць што мы карыстаемся стандартным сістэмным кампілятарам і стандартнай сістэмнай бібліятэкай.

Але наш кампілятар жа іншы, таму трэба задаць пераменную асяроддзя CPATH, якая змяшчае шлях да загаловачных файлаў. Самы просты спосаб атрымаць яго - запытаць у кампілятара:

CPATH = `$(CC) -print-file-name=include`

Наступным чынам трэба аб'явіць усе макрасы, якімі карыстаецца праграма, напрыклад парадак байтаў і гэтак далей. Трэба ўважліва сачыць, каб выкарысталіся аднолькавыя макрасы як для кампіляцыі, так і для праверкі:

LINTFLAGS += -D'__RX_LITTLE_ENDIAN__'

Атрымаць спіс усіх макрасаў кампілятара можна так:

$(CC) -E -dM $(CFLAGS) - < /dev/null

Для апісання асаблівасцяў убудаваных праграм ёсць пашырэнні для мовы Сі, але не пра ўсе пашырэнні ведае аналізатар, таму трэба іх схаваць. Таксама трэба схаваць асэмблер:

LINTFLAGS += -D'__volatile__='
LINTFLAGS += -D'__asm__(a)='

Калі ў вашай праграме ёсць устаўкі асэмблера, трэба іх рабіць так:

__asm__ __volatile__ (
        "rte"
        );

Падкрэслівання патрэбны, каб адрозніваць розныя выкарыстанні слова volatile: пры аб'яўленні пераменных і пры стварэнні асэмблерных уставак. У аб'яўленні пераменных volatile выдаляць нельга.

Таксама трэба дадаць шляхі пошука загаловачных файлаў:

INCLUDE = \
    -I. \
    -Ibsp \
    $(END)

LINTFLAGS += $(INCLUDE)

Асяродзе гатова, можна сабраць усё ў Makefile:

LINT = splint

INCLUDE = \
    -I. \
    -Ibsp \
    $(END)

CPATH = `$(CC) -print-file-name=include`

LINTFLAGS += -D'__RX_LITTLE_ENDIAN__'
LINTFLAGS += -D'__volatile__='
LINTFLAGS += -D'__asm__(a)='
LINTFLAGS += $(INCLUDE)

check: $(SRC)
    CPATH=$(CPATH) $(LINT) $(LINTFLAGS) $^

Ну а далей:

make check

і спрабуеце ці выправіць код, ці выключыць праверкі аналізатара.

Памятайце: статычны аналіз не замяняе праверкі кампілятара. Я прапаную карыстацца абодвума, пры тым, выставіць як мага больш высокі узровень паранойі абодвух. Зручны узровень знойдзеце з павелічэннем досведу пры карыстанні аналізатара.