[Termtools] About memory examples in C category

[Akihisa Yamada]

Dear all,

> - Although "allocation of memory always succeeds", how about the
> value of the allocated memory cell? Is it a non-deterministic value?

it seems natural that neither YES or NO is correct in such cases, since
the C standard identifies the case "The value of the object allocated
by the malloc function is used" in Annex J.2 "Undefined Behavior",
not just "Unspecified".
Cf. http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1570.pdf

Of course I have no request on how these will be treated in the
coming competition, since I'm not involved in the category. :)

But as a former C developer, I personally feel having "defined" C
category is nice in the future, since undefined behavior can be
eliminated by coding rules etc.

Best regards,
Akihisa

On 2015/07/19 19:51, Thomas Ströder wrote:
> Dear all,
>
> Am 19.07.2015 um 16:33 schrieb Ton-Chanh Le:
>> Dear Yamada,
>>
>> Thank you very much for pointing out the rule.
>>
>> We asked the question as the rule also mentioned
>> that "we could also offer an additional category where
>> memory safety can be assumed" and we did not know
>> whether that category is implemented in this competition
>> or not.
>
> Currently, there is no additional category where memory safety can be
> assumed. If there is enough interest in it, we could build up such a
> category for the next competition (we would need to gather suitable
> examples and/or check existing ones).
>
>> Regarding to the rule for C programs, we would like to
>> clarify some points:
>>
>> - The rule says that "neither YES nor NO is a correct result
>> for programs violating memory safety", does this mean
>> the expected result in this case is MAYBE?
>
> Yes. Such examples won't yield any points, but can lead to a penalty if
> claimed to be proven to (non-)terminate. Together with some people from
> SV-COMP, I had a little discussion about this rule. The question is
> whether the property "non-termination" means that you can definitely
> reach a non-terminating run or whether it is the negation of the
> property "termination". Another related question is whether undefined
> behavior means that everything counts as definitely reachable behavior.
> Both answers to these questions have their pros and cons. Currently, the
> interpretation at termCOMP is that "non-termination" means that a
> non-terminating run can definitely be reached and undefined behavior
> does not give you any guarantee of what can be reached. Hence, only
> MAYBE is a correct answer for memory-unsafe examples (but since MAYBE
> does not require any proof, this answer gives no points).
>
> I would neither vote for nor against changing this rule, but if the
> majority of participants would be in favor of changing the rule such
> that violation of memory-safety implies non-termination, I think we
> could do this (not sure whether this would already work for the current
> competition, but it would definitely be possible for future editions).
> However, violation of memory-safety would not include memory leaks as
> these do not lead to undefined behavior and, thus, do not influence
> termination behavior.
>
>> - Although "allocation of memory always succeeds", how about the
>> value of the allocated memory cell? Is it a non-deterministic value?
>
> Yes.
>
>> Thank you very much.
>>
>> Best Regards,
>>
>> Le Ton Chanh
>> Email: chanhle at comp.nus.edu.sg <http://comp.nus.edu.sg>
>
> Best regards,
>
>    Thomas
>
>
>> On Sun, Jul 19, 2015 at 8:19 PM, Akihisa Yamada
>> <akihisa.yamada at uibk.ac.at <mailto:akihisa.yamada at uibk.ac.at>> wrote:
>>
>>      Dear Le Ton Chanh,
>>
>>      your question seems to be discussed in the competition rule:
>>      http://termination-portal.org/wiki/C_Programs
>>
>>      Best regards,
>>      Akihisa
>>
>>
>>      On 2015/07/16 4:36, Ton-Chanh Le wrote:
>>
>>          Dear PC members,
>>
>>          I would like to ask whether we have the assumption
>>          that the pointer examples in the C category is
>>          memory safe or we need to prove memory safety
>>          prior to termination proofs.
>>
>>          Thank you.
>>
>>          Best Regards,
>>
>>          Le Ton Chanh
>>          Email: chanhle at comp.nus.edu.sg <http://comp.nus.edu.sg>
>>          <http://comp.nus.edu.sg>
>>
>>
>>          _______________________________________________
>>          Termtools mailing list
>>          Termtools at lists.lri.fr <mailto:Termtools at lists.lri.fr>
>>          http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>>
>>
>>
>>
>> _______________________________________________
>> Termtools mailing list
>> Termtools at lists.lri.fr
>> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>>
>