[Termtools] Some concerns about C/AProVE_memory_alloca examples

[Thomas Ströder]

Dear all,

I would vote for an additional rule "defining" the behavior of programs
in such cases:

"Read access to allocated, but uninitialized memory is assumed to just
return a non-deterministic value."

Would all participants of the C category be fine with this rule or does
some tool treat this as undefined behavior and consider the program not
to be memory-safe? In the former case, this would solve the problem for
now and I would add the rule to the ones on termination-portal. In the
latter case, I fear that there is no other fair solution than patching
or removing the examples as their intention is definitely not to expose
undefined behavior.

Best regards,

  Thomas


Am 23.07.2015 um 10:58 schrieb Akihisa Yamada:
> Dear C category participants and SC members,
> 
> Ton-Chanh kindly gave me a list of the benchmarks that has the
> initialization problem. But unfortunately, the list was far bigger
> than I expected (containing ca. 140 benchmarks) and I don't think
> they can be corrected before the next competition.
> 
> Could you discuss for a feasible solution, e.g., would you ask
> participants to accept uninitialized memory access (though it is
> not standard-compliant)?
> 
> (In fact, some in the list don't seem to have the problem. But
>  filtering them out also seems impossible.)
> 
> Best regards,
> Akihisa
> 
> On 2015/07/23 4:56, Ton-Chanh Le wrote:
>> Dear Akihisa,
>>
>> Please find the list of examples with uninitialized variables
>> in the attached file.
>>
>> 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
> 

-- 
Thomas Ströder        mailto:stroeder at informatik.rwth-aachen.de
LuFG Informatik 2     http://verify.rwth-aachen.de/stroeder
RWTH Aachen           phone: +49 241 80-21241

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150727/747f22ac/attachment.sig>