Верификация кода с помощью frama-c

Есть код на Си (шейкер сортировка - по сути пузырьковая в обе стороны),

необходимо доказать полную корректность с помощью инструмента Frama-c с плагином jessie