Klever

I would like to paraphrase the description. Quite often the same reasons are responsible for a lot of unsafes and there are some simple patterns (probably regular expressions) like for unknowns to classify corresponding unsafes. These patterns should be applied to all potentially visible contents of error traces including notes and warnings (Bridge does not deal with violation witnesses). Maybe this is quite a big deal for Bridge since it will be necessary to have another representation of error traces in addition to currently supported ones.

Let's me be a first user of a new subsection in the developer documentation that Vladimir will write for blocking issue #11514.

Currently related Bridge functionality is not designed in the way to support this easily. So Vladimir will have to enable this first. To ensure that this works, he can also complete the given task. Also, you can see my last note at #11514.

Implemented in branch "bridge-11513".

Tests passed, so I merged the branch to master in aebfa1cd0. Here is a mini how-to. You can create a new unsafe mark with regexp only in the full-weight mode (indeed, this has sense since they are not created by default and they will not be necessary too often). There you should select the regexp_match error traces comparison function. Then you need to specify an appropriate regexp. Take into account that flags re.S and re.M are used, so e.g. "__ab_c_size.*Field with size \d+ bit can't be written at offset \d+ bit of object -\d+ bit size" can match multiple lines where __ab_c_size will correspond to a call of that function and the last part of the regexp will correspond to the warning.

Note that it can take more time to associate unsafe marks using regexps, especially when you create them for the first time (Bridge generates appropriate caches then) and when you unset attribute "Program fragment" so that it is not used at association (this has sense, since regexps can spread across multiple drivers). Another small inconvenience is that you will likely see quite many dissimilar marks for unsafes if you will unset attribute "Program fragment" as suggested above. You can hide these marks by using an appropriate view.