[Termtools] About memory examples in C category

[Juergen Giesl]

Dear all,

I'm not really convinced by the argument that memory unsafety can be
eliminated by coding rules. This is an undecidable property, just like
termination. Thus, it makes sense to check this property automatically, I
think. But of course there could also be an additional category where
memory safety can be assumed.

Best Regards
Juergen
Am 19.07.2015 20:43 schrieb "Akihisa Yamada" <akihisa.yamada at uibk.ac.at>:

> 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
>>>
>>>
>>  _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150719/f842b5d6/attachment.html>