[Termtools] Expected result of C/AProVE_memory_alloca/svcomp_PodelskiRybalchenko-2004VMCAI-Ex2_true-alloca.c

[Thomas Ströder]

Dear Le Ton Chanh,

You're correct. This program is non-terminating.

Best regards,

  Thomas


Am 15.07.2015 um 10:41 schrieb Ton-Chanh Le:
> Dear C category participants,
> 
> I think the expected result of 
> 
> C/AProVE_memory_alloca/svcomp_PodelskiRybalchenko-2004VMCAI-Ex2_true-alloca.c 
> 
> should be FALSE (non-terminating).
> 
> Please help me to confirm. 
> 
> 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
> 

-- 
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/20150715/24e4493e/attachment.sig>