Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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