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

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.html>