Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays.