A ton of comments here talk about arrays and basic preconditions. See frama-c.com. even in c++ where encapsulation helps class/function contracts and unit testi

A ton of comments here talk about arrays and basic preconditions. See frama-c.com. even in c++ where encapsulation helps class/function contracts and unit testing is a must