--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on November 2016 ---
Le 2016-11-24 à 21:35, David MENTRà a écrit : > What do you want to prove? Oops, I obviously missed this part of your email: "I want to prove that serializing then deserializing produces an identical struct regardless of what's in the input struct's fields." In that case you'll need WP. You'd rather start with very simplified code at first. An easier security property that you can prove (only using Value analysis) is that deserializing arbitrary input never produces run-time error. Best regards, david