J’ai enfin réussi à installer frama-c depuis guix (avec le micro-patch 64675), sans alt-ergo qui est propriétaire, mais avec Z3 qui est libre.

Votre .why3.conf doit contenir la section suivante :

[detected_binary]
exec_name = "/…/bin/z3"
name = "Z3"
version = "4.8.17"

Attention, il faut bien une majuscule à Z3, sinon why3 est perdu.

Il faut bien spécifier à frama-c-wp qu’on utilise Z3 :

frama-c-gui -wp -rte -wp-prover Z3 main.c

#guix #why3 #z3 #framaC