[Termtools] About memory examples in C category

[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.

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?

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

Thank you very much.

Best Regards,

Le Ton Chanh
Email: chanhle at comp.nus.edu.sg

On Sun, Jul 19, 2015 at 8:19 PM, Akihisa Yamada <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>
>>
>>
>> _______________________________________________
>> 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/ca89cce1/attachment.html>