Les logiques de programmes à l'épreuve du réel : tours et détours avec Frama-C/WP