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