How to make a frama-c WP warning into an error?

user_5022994 0
Viewed 37

This warning is a fairly serious one that I would like to turn into an error. I spent a lot of time puzzling over why a proof was not working before realising that this warning really could not be ignored.

[wp] <my source code>.c:16: Warning: 
  Cast with incompatible pointers types (source: uint8*) (target: sint8*)

I believe that the answer should be something like

-wp-warn-key <category>=error

but I don't know how to find the category of "Cast with incompatible pointers types".

Can anyone help?

frama-c warnings
1 Answers

Unfortunately you can't do that for this particular type of warning. Warning categories are a relatively new addition to Frama-C (appearing in 17.0 Chlorine according to the Changelog, i.e. in 2018), and not all warnings that predate this feature have been given a proper category. Since you can only set the behavior of a warning category, category-less warnings can only be warnings.

Warnings with a category will start with [plugin-category], so that you can easily identify which category they belong to

user_16336650
Related