--- layout: fc_discuss_archives title: Message 80 from Frama-C-discuss on November 2013 ---
Hello, On Tue, Nov 12, 2013 at 1:17 AM, Claude Marche <Claude.Marche at inria.fr>wrote: > > I'm not sure Jessie is the right tool for that, The Value plugin or the > WP plugin might do better. > The value analysis plug-in is not designed to verify properties expressed as equations between argument and result, such as: ensures x <= INT32_MAX ==> \result == 2 * x ; At the time John posted about saturating arithmetic functions that he gave to implement in standard C to his students ( http://blog.regehr.org/archives/277 , http://blog.regehr.org/archives/392), I tried to verify my own solutions (correct ones, obviously) in Frama-C. Not much was missing in order to be able to do the exercise in Jessie. This time, what the value analysis plug-in was missing was the ability to hold relational information between the two inputs. The documentation recommends case analysis for this situation. The value analysis plug-in typically required the O(n^2) input space (with n the number of values each of the arguments could take) to be sub-divided by hand into O(n) cases for separate analysis. That was tedious for 32-bit integer inputs and impossible for 64-bit integer inputs. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131112/98ed50a8/attachment.html>