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
- Subject: [Frama-c-discuss] Question on new -eva-precision option in 19
- From: Andre.MARONEZE at cea.fr (Andre Maroneze)
- Date: Mon, 10 Jun 2019 15:35:11 +0200
- In-reply-to: <9aba8653-5b0d-a837-83f5-e4c42fef0b0c@proteancode.com>
- References: <9aba8653-5b0d-a837-83f5-e4c42fef0b0c@proteancode.com>
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>
- Follow-Ups:
- [Frama-c-discuss] Question on new -eva-precision option in 19
- From: rod at proteancode.com (Roderick Chapman)
- [Frama-c-discuss] Question on new -eva-precision option in 19
- References:
- [Frama-c-discuss] Question on new -eva-precision option in 19
- From: rod at proteancode.com (Roderick Chapman)
- [Frama-c-discuss] Question on new -eva-precision option in 19
- Prev by Date: [Frama-c-discuss] Question on new -eva-precision option in 19
- Next by Date: [Frama-c-discuss] Question on new -eva-precision option in 19
- Previous by thread: [Frama-c-discuss] Question on new -eva-precision option in 19
- Next by thread: [Frama-c-discuss] Question on new -eva-precision option in 19
- Index(es):