Номера строк даны в соответствии с task5.c

Строка:	Был успешный alloc:	Был free:
17	нет			нет
20	нет			нет
22	нет			нет
28	нет			нет
29	нет			нет
31	нет			нет
38	нет			нет
40	да			нет
45	да			нет
46	да			нет
49	да			нет
50	да			нет
51	да			нет
52	да			нет
53	да			нет
140	да			нет

Дошли до конца процедуры, был выполенн alloc, но не было free => cпецификация нарушается, что и было выявлено в процессе верификации модели.