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