--- layout: fc_discuss_archives title: Message 99 from Frama-C-discuss on September 2013 ---
On Sat, Sep 14, 2013 at 2:55 AM, Steven Stewart-Gallus < sstewartgallus00 at mylangara.bc.ca> wrote: > Shouldn't Frama-C assume main's arguments are valid (there are argc c > strings in argv, and one null pointer?) It seems not to trust main's > arguments by default. Is there an option to enable this? > The two families of plug-ins that work at this level at the weakest-precondition plug-ins and the value analysis plug-in. Weakest precondition plug-ins use main's pre-condition. The value analysis plug-ins has rough options -context-width, -context-depth and -context-valid-pointers (citing the manual from memory), that are not subtle enough to express ?a NULL-terminated array of null-terminated strings, with matching length. The solution is to write your own analysis entry point and to build your ideal arguments in C: void analysis_main(void){ char arg0[] = "myprogram"; char arg1[] = ? ? char **argv[] = {arg0, arg1, ?}; int result = main(4, argv); } You may find that this allows to express simply that the program expects a numeric string as its first argument (or anyway that that is the usage for which you want to verify it), and that you can begin to annotate the construction of the arguments with hints such as ?the cases where there are 2 and 3 arguments are interesting to study separately?, or even ?the cases where the length of argv[1] is 5 and 6 are interesting to study separately?). Pascal -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130914/f703b7a9/attachment-0001.html>