[Termtools] Some concerns about C/AProVE_memory_alloca examples

[Ton-Chanh Le]

Dear all,

I have some concerns about some examples in the
C/AProVE_memory_alloca folder

1. Expected result of svcomp_BradleyMannaSipma-2005ICALP-Fig1_true-alloca
is not correct

The program does not terminate, e.g. when y1 > 0 and y2 = 0.

2. In
svcomp_Urban-2013WST-Fig1_false-unreach-label-termination-alloca.c,
svcomp_Velroyen_false-unreach-label-termination-alloca.c
and some others, can we assume that the single statement

int* x = alloca(sizeof(int));

is equivalent to

int* x = alloca(sizeof(int));
*x = __VERIFIER_nondet_int();

or could we make it explicitly like
svcomp_Ben-Amram-2010LMCS-Ex2.3_true-alloca.c
svcomp_BradleyMannaSipma-2005CAV-Fig1_true-alloca.c
etc.

Thank you.

Best Regards,

Le Ton Chanh
Email: chanhle at comp.nus.edu.sg
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150716/a76dda02/attachment.html>