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] Eva plugin - sscanf function (Andre Maroneze)

  • Subject: [Frama-c-discuss] Eva plugin - sscanf function (Andre Maroneze)
  • From: rovedy at gmail.com (Rovedy Silva)
  • Date: Thu, 6 Aug 2020 08:42:54 -0300
  • In-reply-to: <mailman.5.1596016812.29553.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.5.1596016812.29553.frama-c-discuss@lists.gforge.inria.fr>
Hi Andre,

Thanks a lot! I will think about the stub implementation.

Best regards,
Rovedy

Em qua., 29 de jul. de 2020 às 07:00, <
frama-c-discuss-request at lists.gforge.inria.fr> escreveu:

>
>
> Hello Rovedy,
>
> Currently, sscanf has no built-in, so a C stub would be necessary to get
> a precise result for sscanf.
>
> Knowing exactly which kinds of `%` parameters are needed, it should be
> possible to code a stub that would not be extremely complex and, with
> enough slevel, should improve precision. However, conversion functions
> such as atoi/atof are tricky to code without errors. Some of them could
> benefit from OCaml builtins, which might be easier to code correctly
> than the equivalent C code (i.e. by using OCaml conversion functions to
> do the hard part), but coding Eva built-ins still requires quite some
> knowledge about the underlying representation.
>
> Depending on the use case, manually replacing such calls with function
> prototypes having the appropriate bounds defined in ACSL specifications
> might be the simplest way, even though it's very far from ideal.
>
>
> Best regards,
>
>
> On 23/07/2020 13:51, Rovedy Silva wrote:
> > Hello,
> >
> > Is it possible to get an exact result for the sscanf arguments?
> >
> > I read about variadic functions in the user manual.
> >
> > I am using the Frama-C 20.0 (Calcium). The simplified source code and
> > the analysis are attached below.
> >
> > The real application employs the sscanf function to read 68
> > parameters. Those parameters are used in many equations.
> >
> > If those parameters have a variation domain as [—.—] so all the values
> > computed from those parameters will have this variation domain [—.—] too?
> > Is there a way to increase the precision of variation domain?
> >
> > Best Regards,
> > Rovedy
> > ———————————————— source code ————————
> > #include <stdio.h>
> > int main()
> > {
> > char *s = "20 30";
> > unsigned int d1,d2,result;
> > int len;
> >     len =  sscanf(s,"%u %u",&d1,&d2);
> >     result=d1+d2;
> >     return 0;
> > }
> > ———————————————— complete analysis  ————————
> > [kernel] Parsing sscanf.c (with preprocessing)
> > [eva] Analyzing a complete application starting at main
> > [eva] Computing initial state
> > [eva] Initial state computed
> > [eva:initial-state] Values of globals at initialization
> > [eva] using specification for function sscanf_va_1
> > [eva] done for function main
> > [eva] ====== VALUES COMPUTED ======
> > [eva:final-states] Values at end of function main:
> >   s ∈ {‌{ "20 30" }‌}
> >   d1 ∈ [--..--]
> >   d2 ∈ [--..--]
> >   result ∈ [--..--]
> >   len ∈ [--..--]
> >   __retres ∈ {0}
> > [eva:summary] ====== ANALYSIS SUMMARY ======
> >
> ----------------------------------------------------------------------------
> >   1 function analyzed (out of 1): 100% coverage.
> >   In this function, 5 statements reached (out of 5): 100% coverage.
> >
> ----------------------------------------------------------------------------
> >   No errors or warnings raised during the analysis.
> >
> ----------------------------------------------------------------------------
> >   0 alarms generated by the analysis.
> >
> ----------------------------------------------------------------------------
> >   Evaluation of the logical properties reached by the analysis:
> >     Assertions        0 valid     0 unknown     0 invalid      0 total
> >     Preconditions     4 valid     0 unknown     0 invalid      4 total
> >   100% of the logical properties reached have been proven.
> >
> ----------------------------------------------------------------------------
> >
> >
> > _______________________________________________
> > Frama-c-discuss mailing list
> > Frama-c-discuss at lists.gforge.inria.fr
> > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>
> --
> André Maroneze
> Researcher/Engineer CEA/List
> Software Reliability and Security Laboratory
>
> -------------- next part --------------
> An HTML attachment was scrubbed...
> URL: <
> http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200729/3ccbfdb4/attachment-0001.html
> >
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
>
> ------------------------------
>
> End of Frama-c-discuss Digest, Vol 145, Issue 10
> ************************************************
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200806/55c6b3fc/attachment.html>