Frama-C: Function Contracts and Static Analysis for the C Language (frama-c.com)