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

  • Subject: [Frama-c-discuss] Eva plugin - sscanf function
  • From: rovedy at gmail.com (Rovedy Silva)
  • Date: Thu, 23 Jul 2020 08:51:40 -0300
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.

----------------------------------------------------------------------------
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200723/c1a845ba/attachment.html>