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] 'frama-c -wp-msg-key help'

Hello Jens,

Le jeu. 16 janv. 2020 à 15:23, Gerlach, Jens <
jens.gerlach at fokus.fraunhofer.de> a écrit :

> Hello,
>
>
>
> The WP manual mentions on page 41 the option ‘-wp-msg-key ‘
>
> When I type ‘frama-c -wp-msg-key help’ I get a list of roughly 40
> arguments.
>
> Is there any documentation about the purpose of this option?
>
>
>

For any plugin (and the kernel with -kernel-msg-key), this option enables
the output of additional messages on the console during the analysis. Such
messages are grouped into categories that can be enabled independently from
each other (well in fact you can have a hierarchy, but WP does not make use
of it). The name of these categories can be fed to -wp-msg-key. They are
meant to be self-explanatory, even though this might not always be the
case. When a category is activated (e.g. prover for things related to the
provers), corresponding messages will start with [PLUGIN:CATEGORY], making
them easier to spot.
Finally, WP makes use of this mechanism to hide messages: when activated,
the categories that begin with no- will prevent the corresponding messages
to be output. As far as I know, it is the only plug-in that (ab)use the
message category mechanism this way.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20200116/2e2bb2ef/attachment.html>