Vivien (dentelle & numérique)Jul 17, 2023

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

Show threadniconiconi [MOVED]Feb 27, 2021
#Why3 looks like an interesting platform. Unfortunately, little documentation exists for WhyML as a standalone programming language. Unless you're already have ML/OCaml/F# experience, all can you do is asking "why" 3 times. It comes with a handy IDE that lists all the goals and options you need to prove a program, but something is missing: for newcomers the first goal should always be "close the IDE, go and learn Standard ML for 2 months before you come back..."
xameerJan 10, 2021
#Jessie relies on why or #Why3 back-end to enable #proof obligations to be sent to atp like Z3, Simplify, Alt-Ergo or itp like Coq or Why. Using Jessie, an implementation of #bubblesort can be proved to satisfy their respective specifications. W separation (memory model)-logic