--- layout: fc_discuss_archives title: Message 17 from Frama-C-discuss on July 2020 ---
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>