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] Question on new -eva-precision option in 19

Hello,

Indeed, the manuals have not been entirely updated for the beta 
releases. That said, the help message of `frama-c -eva-help` does resume 
its behavior most succinctly:

-eva-precision <n>  Meta-option that automatically sets up some Eva
                     parameters for a quick configuration of an 
analysis, from
                     0 (fastest but rather imprecise analysis) to 11 
(accurate
                     but potentially slow analysis).

In practice, running `frama-c -eva -eva-precision <N>`, even without a 
program to analyze, displays its effect. For instance, when n = 0, we have:

[eva] Option -eva-precision 0 detected, automatic configuration of the 
analysis:
   option -eva-min-loop-unroll set to 0 (default value).
   option -eva-slevel set to 0 (default value).
   option -eva-widening-delay set to 1.
   option -eva-ilevel set to 8 (default value).
   option -eva-plevel set to 10.
   option -eva-subdivide-non-linear set to 0 (default value).
   option -eva-remove-redundant-alarms set to false.
   option -eva-symbolic-locations-domain set to false (default value).
   option -eva-equality-domain set to false (default value).
   option -eva-equality-through-calls set to 'none'.
   option -eva-gauges-domain set to false (default value).
   option -eva-split-return set to '' (default value).

What the option does is simply set a bunch of precision-related options 
to a set of predefined values. The idea is to help users quickly 
determine an acceptable trade-off between precision and speed in their 
analysis, especially when they don't know which options may impact it.

In the above example, the only values that are really affected by the 
option are `-eva-widening-delay`, which is set to 1 instead of 3; 
`-eva-plevel`, which is set to 10 instead of 200; and 
`-eva-remove-redundant-alarms`, which is set to false. (There is also an 
option related to the equality domain, but it is not activated by 
default anyway.)

Note that manually-specified options take priority over -eva-precision, 
so if I had set `-eva-plevel 100`, for instance, I would have got:

option -eva-plevel already set to 100 (not modified).

This is all the option does. It does not offer new mechanisms, just 
simplifies their usage.

Note that the default value for -eva-precision is "-1", not because it 
is "faster" than 0, but simply because it does not correspond to one of 
the predefined sets. So `-eva-precision 0` should be faster (and less 
precise) than not using the option at all.


Best regards,


On 10/06/2019 15:05, Roderick Chapman wrote:
>
> Hello,
>
>  I am just starting out using Frama-C on a new project.
>
> First question: The announcement (in this list) of release 19 
> mentioned a new option "-eva-precision", but I cannot find any mention 
> of it in the EVA manual that accompanied the second beta release. Am I 
> missing something?
>
>  Many thanks,
>
>   Rod Chapman, Protean Code Limited
>
>
>
> _______________________________________________
> 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/20190610/a42c0f81/attachment.html>