[Cocci] Matching format strings

[julia.lawall@lip6.fr (Julia Lawall)]

> Looking at some of the code (well, comments rather), coccinelle is
> building a CTL formula and a state machine for the C file and tries to
> find the states where it matches? Is that correct?

Yes, this is correct.

> Does it try to compress the state machine based on the predicates
> involved? BDDs tend to be rather helpful with CTL model checking. Not
> sure how useful that is, depending on the information that needs to be
> extracted (and I've not touched model checking in ages).

No, we don't do that.  Basically, the graph itself is pretty small, but
the problem is all of the possible variable bindings.  Our reasoning was
that BDDs would not be helpful.

> Sorry if this is completely wrong.
>
> I vaguely remember seeing something like this somewhere, but can't find
> it anymore. That might simplify the three-pronged construction I use
> into a single patch hunk like the below. Is there a construction like
> that available or have I just dreamed that up?
>
> @@
> (stuff here also contains format1, format2, args_before and others as
> usual)
> identifier merged : python merge_formats(format1, format2, args_before);
> @@
>
> -snprintf( buf, E, format1, args );
> -Debug( L, format2, args_before, buf, args_after );
> +Debug( L, merged, args_before, args, args_after );

You made it up :)  Currently, the only thing you can do with python on the
fly like this is write predicates, not create variable values.  The exact
syntax is, eg

identifier x : script:python(...) { ... }

The first ... is any inherited metavariables that the script code needs,
but variables defined in the same rule are not allowed.  The second ...
needs to look like C code.  Typically, it would be a function call, and
then you would define the function in the

@initialize:python@
@@

code at the beginning of the script, where you can put whatever python
code you want.

julia

> --
> Ond?ej Kuzn?k
> Senior Software Engineer
> Symas Corporation                       http://www.symas.com
> Packaged, certified, and supported LDAP solutions powered by OpenLDAP
>