--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on November 2016 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Some newbie questions about frama-c



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