[cocci] Checking CTL code?

[cocci] Checking CTL code?

[Markus Elfring]

Hello,

The Coccinelle software supports a computation tree logic variant.
Can CTL code be directly passed to a corresponding tool for further analyses
and system tests?

Regards,
Markus

Re: [cocci] Checking CTL code?

[Julia Lawall]

On Tue, 14 May 2024, Markus Elfring wrote:

> Hello,
>
> The Coccinelle software supports a computation tree logic variant.
> Can CTL code be directly passed to a corresponding tool for further analyses
> and system tests?

Not sure what you are asking.  You can print the CTL code with
--verbose-ctl-option.  There might be a way to get it printed in latex as
well.

On the other hand, you can also hand write CTL formulas and pass them to
Coccinelle.  I think that can be done in some way with the --test options.

julia


>
> Regards,
> Markus
>

Re: [cocci] Checking CTL code?

[Markus Elfring]

>> The Coccinelle software supports a computation tree logic variant.
>> Can CTL code be directly passed to a corresponding tool for further analyses
>> and system tests?
>
> Not sure what you are asking.

I hope that adjustments can be achieved also for another clarification approach.

Determination of CTL code without C file name
2019-01-09
https://github.com/coccinelle/coccinelle/issues/156


> On the other hand, you can also hand write CTL formulas and pass them to
> Coccinelle.  I think that can be done in some way with the --test options.

It seems that I am still missing corresponding software documentation.

Regards,
Markus

Re: [cocci] Checking CTL code?

[Markus Elfring]

> On the other hand, you can also hand write CTL formulas and pass them to Coccinelle.

Would you like to extend descriptions anyhow for program parameters
which would be relevant for the handling of computation tree logic variants?

Regards,
Markus