Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] *p and p[0]

> I'm extremely happy to see such a demonstration of how useful is
> to use type integer instead of int in the annotations. Many thanks!

I would like to emphasize that I just copied the example from the ACSL
tutorial. I would never use "int" when I have a chance to use
"integer" in a property. I like it, it somehow reminds me of COBOL.

> By the way, I have no idea at all why *p versus p[0] makes a difference.
> Is it reproducible ?

I had the problem and the students who arrived that far too, so: yes.

Actually, the same student who also reported an alt-ergo soundness bug
also found that using p[0] was no longer enough to help if he inserted
an irrelevant assignment like:
Global = 402;
at the beginning of the function.

The ways of the automatic prover are unfathomable (when proving
existential formulas anyway).

Pascal

PS: Could we also accept the syntax "INTEGER"? That would be paradise.