[Termtools] Some concerns about C/AProVE_memory_alloca examples

[Matthias Heizmann]

Hi Thomas,

I am in favor for the rule you proposed.

Best,
Matthias


On Monday, July 27, 2015 13:41:13 Thomas Ströder wrote:
> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part.
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150728/a3c8e85c/attachment-0001.sig>