--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on August 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Eva plugin - sscanf function (Andre Maroneze)



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>