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] Shouldn't Frama-C assume main's arguments are valid?

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>