--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on June 2019 ---
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>