--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on July 2010 ---
[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.