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

Glad to see #FramaC get a shout out from #AdaCore. #C is one language with tooling for using solvers to prove correctness. Glad to see competition here. They’re moving the whole industry forward.

https://www.adacore.com/uploads/technical-papers/2016-10-SPARK-MisraC-FramaC.pdf

#FramaC WP just threw at me that #ACSL lambdas are not supported yet. How the hell am i supposed to use \numof ?! #framacWP #formalmethods

I have time to figure it out till Dec30

It's of course ”with Frama-C” and let me add a few tags: #FramaC #FormalMethods #DeductiveVerification