From: Markus Elfring <Markus.Elfring@web.de>
To: cocci@inria.fr
Subject: [cocci] Improving handling of position information for SmPL?
Date: Sun, 28 Sep 2025 11:22:30 +0200 [thread overview]
Message-ID: <61f326c5-7c60-4390-bcb7-20707fc68b6f@web.de> (raw)
Hello,
A bit of information is provided in the manual of the semantic patch language
also for the usage of position metavariables.
https://gitlab.inria.fr/coccinelle/coccinelle/-/blob/7674e29155d23846c41504948f4e4b1e796d07ec/docs/manual/cocci_syntax.tex#L420-432
Some data processing results can be observed then also according to
the software combination “Coccinelle 1.3.0”.
Source file example:
void my_test_number(void)
{
123;
}
A)
find_special_number_without_position.cocci:
@find@
@@
-123;
Markus_Elfring@Sonne:…/Projekte/Coccinelle/Probe> /usr/bin/spatch --show-ctl-text test_special_number.c find_special_number_without_position.cocci
…
Let _r_0 = (EX^((TrueBranch v InLoop)) v EX^(EX^(FalseBranch))) in
((_r_0 & (Ex _v . 123;)) v (!_r_0 & (Ex _v . 123;)))
…
B)
find_special_number_with_position.cocci:
@find@
position place;
@@
-123@place;
Markus_Elfring@Sonne:…/Projekte/Coccinelle/Probe> /usr/bin/spatch --show-ctl-text test_special_number.c find_special_number_with_position.cocci
…
Let _r_0 = (EX^((TrueBranch v InLoop)) v EX^(EX^(FalseBranch))) in
((_r_0 & (Ex_ place . (Ex _v . 123@place ;))) v
(!_r_0 & (Ex_ place . (Ex _v . 123@place ;))))
…
A corresponding computation tree formula is generated.
But it contains still references to an extra position metavariable despite of
the implementation detail that it might not be needed here.
C)
find_special_number_with_reused_position.cocci:
@start@
position place;
@@
123@place;
@reusing@
position start.place;
@@
123@place;
@script:python@
p << start.place;
@@
print(f"file: {p[0].file}\nfunction: {p[0].current_element}\nline: {p[0].line}")
Markus_Elfring@Sonne:…/Projekte/Coccinelle/Probe> /usr/bin/spatch --show-ctl-text test_special_number.c find_special_number_with_reused_position.cocci
…
start =
…
CTL =
(Ex place . (Ex _v . 123@place ;))
…
reusing =
…
CTL =
123@place ;
…
How do you think about to clarify the shown differences in the generated terms?
Will any improvements become helpful for involved software components?
Regards,
Markus
next reply other threads:[~2025-09-28 9:22 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2025-09-28 9:22 Markus Elfring [this message]
2025-09-29 14:18 ` [cocci] Improving handling of position information for SmPL? Markus Elfring
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=61f326c5-7c60-4390-bcb7-20707fc68b6f@web.de \
--to=markus.elfring@web.de \
--cc=cocci@inria.fr \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).