[Termtools] About memory examples in C category
Akihisa Yamada
akihisa.yamada at uibk.ac.at
Tue Jul 28 14:32:47 CEST 2015
Dear Matthias,
I agree that it is hard to state precisely. On the other hand, gcc has
"-Wsequence-point" option to detect this kind of issues. I checked:
for f in */*.c
do gcc -c -std=c99 -Wsequence-point -Wno-int-to-pointer-cast
-Wno-implicit-function-declaration -o /dev/null $f
done
and found only one warning related to this:
SV-COMP_Termination_Category/joey_false-termination.c: In function ‘rec’:
SV-COMP_Termination_Category/joey_false-termination.c:15:18: warning:
operation on ‘x’ may be undefined [-Wsequence-point]
return rec(++x) + rec(--x);
^
Best regards,
Akihisa
On 2015/07/28 5:00, Matthias Heizmann wrote:
> Hi Thomas, hi all,
>
> On Monday, July 27, 2015 13:29:34 Thomas Ströder wrote:
>> "Programs where the evaluation order of operations is not defined
>> according to the C standard are not allowed. As an example, the program
>>
>> int main(){
>> int x = 0;
>> while( x++ == x );
>> }
>>
>> is not allowed since the evaluation order between ++ and == is not
>> defined according to the C standard."
>
> I like the idea of "a rule like this". However, yet I do not have an idea how
> we can state such a rule precisely.
>
> I see two problems with your suggestion.
> 1. What exactly is an operation? The C standard uses the term "operation" but
> I think it is never defined.
>
> 2. According to my notion of 'operation' your rule also forbids programs that
> contain the expression
> f1() + f2()
> because the C standard does not define whether 'f1()' or 'f2()' is evaluated
> first. Is that you intension?
> If yes, this is fine for me, but I guess then we have several programs (at
> least MutualRecursion_1a_false-termination.c) that have to be excluded from
> the competition.
>
> Furthermore, I think it is a problem that we do not have a tool that can check
> compliance with your rule. We would have to check all programs manually.
>
> Best,
> Matthias
>
>
> PS: Sorry for the delayed response. In the next days I will be able to respond
> more quickly.
>
>
>
>
>
>
>
> On Monday, July 27, 2015 13:29:34 Thomas Ströder wrote:
>> Dear Akihisa,
>>
>> I agree with you. What about the following additional rule:
>>
>> "Programs where the evaluation order of operations is not defined
>> according to the C standard are not allowed. As an example, the program
>>
>> int main(){
>> int x = 0;
>> while( x++ == x );
>> }
>>
>> is not allowed since the evaluation order between ++ and == is not
>> defined according to the C standard."
>>
>> Would all participants of the C category be fine with that rule or do
>> you see problems with it? If all participants agree, I would add it to
>> the rules on termination-portal.
>>
>> Best regards,
>>
>> Thomas
>>
>>
>> _______________________________________________
>> Termtools mailing list
>> Termtools at lists.lri.fr
>> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
--
Akihisa Yamada, Ph.D.
Computational Logic Group, Institute of Computer Science,
University of Innsbruck
http://cl-informatik.uibk.ac.at/~ayamada/
-------------- next part --------------
AProVE_memory_alloca/svcomp_a.01-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_a.01-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.01-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.01-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.04-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_a.04-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.04-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.04-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.05-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_a.05-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.05-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.05-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.06-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_a.06-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.06-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.06-alloca.c:9:18: warning: initialization makes pointer from integer without a cast
int* z_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.06-alloca.c:10:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.07-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_a.07-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.07-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.07-alloca.c:9:18: warning: initialization makes pointer from integer without a cast
int* z_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.07-alloca.c:10:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.08-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_a.08-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.08-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.08-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.09_assume-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_a.09_assume-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.09_assume-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.09_assume-alloca.c:9:18: warning: initialization makes pointer from integer without a cast
int* z_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.10-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_a.10-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.10-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_a.10-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_add_last_alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_add_last_alloca.c:8:14: warning: initialization makes pointer from integer without a cast
int *arr = alloca(length*sizeof(int));
^
AProVE_memory_alloca/svcomp_Avery-2006FLOPS-Tabel1_true-alloca.c: In function ‘subxy’:
AProVE_memory_alloca/svcomp_Avery-2006FLOPS-Tabel1_true-alloca.c:6:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Avery-2006FLOPS-Tabel1_true-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Avery-2006FLOPS-Tabel1_true-alloca.c:8:14: warning: initialization makes pointer from integer without a cast
int* z = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Avery-2006FLOPS-Tabel1_true-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* i = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_aviad_true-alloca.c: In function ‘f’:
AProVE_memory_alloca/svcomp_aviad_true-alloca.c:6:18: warning: initialization makes pointer from integer without a cast
int* a_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_aviad_true-alloca.c:7:16: warning: initialization makes pointer from integer without a cast
int* tmp = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_aviad_true-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* count = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.01-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.01-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.01-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.01-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.02-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.02-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.02-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.02-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.03_assume-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.03_assume-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.03_assume-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.03-no-inv_assume-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.03-no-inv_assume-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.03-no-inv_assume-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.04-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.04-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.04-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.04-alloca.c:9:20: warning: initialization makes pointer from integer without a cast
int* tmp_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.05-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.05-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.05-alloca.c:8:20: warning: initialization makes pointer from integer without a cast
int* tmp_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.06-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.06-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.06-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.06-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.07-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.07-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.07-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.07-alloca.c:9:18: warning: initialization makes pointer from integer without a cast
int* z_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.07-alloca.c:10:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.09_assume-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.09_assume-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.09_assume-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.09_assume-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.09-no-inv_assume-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.09-no-inv_assume-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.09-no-inv_assume-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.09-no-inv_assume-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.10-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.10-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.10-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.10-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.11-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.11-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.11-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.11-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.12-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.12-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.12-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.12-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.13-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.13-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.13-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.13-alloca.c:9:18: warning: initialization makes pointer from integer without a cast
int* z_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.13-alloca.c:10:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.14-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.14-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.14-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.14-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.15-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.15-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.15-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.15-alloca.c:9:18: warning: initialization makes pointer from integer without a cast
int* z_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.15-alloca.c:10:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.16-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.16-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.16-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.16-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.17-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.17-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.17-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.17-alloca.c:9:18: warning: initialization makes pointer from integer without a cast
int* z_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.17-alloca.c:10:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.18-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_b.18-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_b.18-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Ben-Amram-2010LMCS-Ex2.3_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_Ben-Amram-2010LMCS-Ex2.3_true-alloca.c:16:18: warning: initialization makes pointer from integer without a cast
int *x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Ben-Amram-2010LMCS-Ex2.3_true-alloca.c:17:18: warning: initialization makes pointer from integer without a cast
int *y = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Ben-Amram-2010LMCS-Ex2.3_true-alloca.c:18:18: warning: initialization makes pointer from integer without a cast
int *z = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_BradleyMannaSipma-2005CAV-Fig1_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_BradleyMannaSipma-2005CAV-Fig1_true-alloca.c:16:18: warning: initialization makes pointer from integer without a cast
int *x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_BradleyMannaSipma-2005CAV-Fig1_true-alloca.c:17:11: warning: initialization makes pointer from integer without a cast
int *y = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_BradleyMannaSipma-2005CAV-Fig1_true-alloca.c:18:11: warning: initialization makes pointer from integer without a cast
int *N = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_BradleyMannaSipma-2005CAV-Fig1-modified_false-termination.c: In function ‘main’:
AProVE_memory_alloca/svcomp_BradleyMannaSipma-2005CAV-Fig1-modified_false-termination.c:29:19: warning: initialization makes pointer from integer without a cast
int *y1 = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_BradleyMannaSipma-2005CAV-Fig1-modified_false-termination.c:30:12: warning: initialization makes pointer from integer without a cast
int *y2 = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_BradleyMannaSipma-2005ICALP-Fig1_true-alloca.c: In function ‘gcd’:
AProVE_memory_alloca/svcomp_BradleyMannaSipma-2005ICALP-Fig1_true-alloca.c:6:19: warning: initialization makes pointer from integer without a cast
int* y1_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_BradleyMannaSipma-2005ICALP-Fig1_true-alloca.c:7:19: warning: initialization makes pointer from integer without a cast
int* y2_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_BrockschmidtCookFuhs-2013CAV-Fig1_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_BrockschmidtCookFuhs-2013CAV-Fig1_true-alloca.c:4:14: warning: initialization makes pointer from integer without a cast
int* i = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_BrockschmidtCookFuhs-2013CAV-Fig1_true-alloca.c:5:14: warning: initialization makes pointer from integer without a cast
int* j = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_BrockschmidtCookFuhs-2013CAV-Fig1_true-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* n = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_BrockschmidtCookFuhs-2013CAV-Introduction_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_BrockschmidtCookFuhs-2013CAV-Introduction_true-alloca.c:4:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_BrockschmidtCookFuhs-2013CAV-Introduction_true-alloca.c:5:14: warning: initialization makes pointer from integer without a cast
int* y = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.01_assume-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_c.01_assume-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.01_assume-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.01-no-inv-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_c.01-no-inv-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.01-no-inv-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.01-no-inv-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.02-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_c.02-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.02-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.02-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.03-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_c.03-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.03-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.03-alloca.c:9:18: warning: initialization makes pointer from integer without a cast
int* z_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.03-alloca.c:10:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.07-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_c.07-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* i_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.07-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* j_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.07-alloca.c:9:18: warning: initialization makes pointer from integer without a cast
int* k_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.07-alloca.c:10:20: warning: initialization makes pointer from integer without a cast
int* tmp_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.07-alloca.c:11:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.08-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_c.08-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* i_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.08-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* j_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_c.08-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_ChenFlurMukhopadhyay-2012SAS-Fig1_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_ChenFlurMukhopadhyay-2012SAS-Fig1_true-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_ChenFlurMukhopadhyay-2012SAS-Fig1_true-alloca.c:7:14: warning: initialization makes pointer from integer without a cast
int* y = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_ChenFlurMukhopadhyay-2012SAS-Fig1_true-alloca.c:8:14: warning: initialization makes pointer from integer without a cast
int* z = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_CookSeeZuleger-2013TACAS-Fig3_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_CookSeeZuleger-2013TACAS-Fig3_true-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_CookSeeZuleger-2013TACAS-Fig3_true-alloca.c:7:14: warning: initialization makes pointer from integer without a cast
int* y = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_CookSeeZuleger-2013TACAS-Fig7a_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_CookSeeZuleger-2013TACAS-Fig7a_true-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_CookSeeZuleger-2013TACAS-Fig7a_true-alloca.c:7:14: warning: initialization makes pointer from integer without a cast
int* y = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_CookSeeZuleger-2013TACAS-Fig7a_true-alloca.c:8:14: warning: initialization makes pointer from integer without a cast
int* d = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_CookSeeZuleger-2013TACAS-Fig7b_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_CookSeeZuleger-2013TACAS-Fig7b_true-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_CookSeeZuleger-2013TACAS-Fig7b_true-alloca.c:7:14: warning: initialization makes pointer from integer without a cast
int* y = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_CookSeeZuleger-2013TACAS-Fig7b_true-alloca.c:8:14: warning: initialization makes pointer from integer without a cast
int* z = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_count_down_alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_count_down_alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int *arr = alloca(length*sizeof(int));
^
AProVE_memory_alloca/svcomp_easySum-alloca.c: In function ‘iterate’:
AProVE_memory_alloca/svcomp_easySum-alloca.c:7:22: warning: initialization makes pointer from integer without a cast
int* bound_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_easySum-alloca.c:8:14: warning: initialization makes pointer from integer without a cast
int* i = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_easySum-alloca.c:9:16: warning: initialization makes pointer from integer without a cast
int* sum = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_ex1-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_ex1-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_ex1-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_ex1-alloca.c:9:18: warning: initialization makes pointer from integer without a cast
int* r_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_ex2-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_ex2-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_ex2-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_ex2-alloca.c:9:18: warning: initialization makes pointer from integer without a cast
int* z_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_ex2-alloca.c:10:21: warning: initialization makes pointer from integer without a cast
int* flag_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_ex2-alloca.c:11:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_ex3a-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_ex3a-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_ex3a-alloca.c:8:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_ex3b-alloca.c: In function ‘test_fun’:
AProVE_memory_alloca/svcomp_ex3b-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_ex3b-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_ex3b-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_fermat-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_fermat-alloca.c:5:16: warning: initialization makes pointer from integer without a cast
int* MAX = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_fermat-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* a = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_fermat-alloca.c:7:14: warning: initialization makes pointer from integer without a cast
int* b = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_fermat-alloca.c:8:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_flag-alloca.c: In function ‘f’:
AProVE_memory_alloca/svcomp_flag-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_flag-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_flag-alloca.c:9:17: warning: initialization makes pointer from integer without a cast
int* flag = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_flag-alloca.c:10:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_gcd1_true-alloca.c: In function ‘gcd’:
AProVE_memory_alloca/svcomp_gcd1_true-alloca.c:6:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_gcd1_true-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_gcd1_true-alloca.c:8:14: warning: initialization makes pointer from integer without a cast
int* r = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_genady_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_genady_true-alloca.c:4:14: warning: initialization makes pointer from integer without a cast
int* i = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_genady_true-alloca.c:5:14: warning: initialization makes pointer from integer without a cast
int* j = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_GulwaniJainKoskinen-2009PLDI-Fig1_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_GulwaniJainKoskinen-2009PLDI-Fig1_true-alloca.c:6:15: warning: initialization makes pointer from integer without a cast
int* id = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_GulwaniJainKoskinen-2009PLDI-Fig1_true-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* maxId = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_GulwaniJainKoskinen-2009PLDI-Fig1_true-alloca.c:12:20: warning: initialization makes pointer from integer without a cast
int* tmp = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_HarrisLalNoriRajamani-2010SAS-Fig1_true-alloca.c: In function ‘f’:
AProVE_memory_alloca/svcomp_HarrisLalNoriRajamani-2010SAS-Fig1_true-alloca.c:6:18: warning: initialization makes pointer from integer without a cast
int* d_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_HarrisLalNoriRajamani-2010SAS-Fig1_true-alloca.c:7:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_HarrisLalNoriRajamani-2010SAS-Fig1_true-alloca.c:8:14: warning: initialization makes pointer from integer without a cast
int* y = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_HarrisLalNoriRajamani-2010SAS-Fig1_true-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* k = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_HarrisLalNoriRajamani-2010SAS-Fig1_true-alloca.c:10:14: warning: initialization makes pointer from integer without a cast
int* z = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_HarrisLalNoriRajamani-2010SAS-Fig2_false-unreach-label-termination-alloca.c: In function ‘foo’:
AProVE_memory_alloca/svcomp_HarrisLalNoriRajamani-2010SAS-Fig2_false-unreach-label-termination-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* y = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_HarrisLalNoriRajamani-2010SAS-Fig2_false-unreach-label-termination-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_HarrisLalNoriRajamani-2010SAS-Fig2_false-unreach-label-termination-alloca.c:39:14: warning: initialization makes pointer from integer without a cast
int* d = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_HarrisLalNoriRajamani-2010SAS-Fig2_false-unreach-label-termination-alloca.c:40:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_HarrisLalNoriRajamani-2010SAS-Fig3_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_HarrisLalNoriRajamani-2010SAS-Fig3_true-alloca.c:12:7: warning: assignment makes pointer from integer without a cast
x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_java_AG313-alloca.c: In function ‘quot’:
AProVE_memory_alloca/svcomp_java_AG313-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_java_AG313-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* y_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_java_AG313-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* i = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_java_Break-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_java_Break-alloca.c:5:14: warning: initialization makes pointer from integer without a cast
int* i = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_java_Break-alloca.c:6:13: warning: initialization makes pointer from integer without a cast
int* c= alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_java_Continue1-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_java_Continue1-alloca.c:5:14: warning: initialization makes pointer from integer without a cast
int* i = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_java_Continue1-alloca.c:6:13: warning: initialization makes pointer from integer without a cast
int* c= alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_java_LogBuiltIn-alloca.c: In function ‘mlog’:
AProVE_memory_alloca/svcomp_java_LogBuiltIn-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* x_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_java_LogBuiltIn-alloca.c:8:16: warning: initialization makes pointer from integer without a cast
int* res = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_java_Nested-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_java_Nested-alloca.c:5:14: warning: initialization makes pointer from integer without a cast
int* i = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_java_Nested-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* j = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_java_Nested-alloca.c:7:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_java_Sequence-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_java_Sequence-alloca.c:5:14: warning: initialization makes pointer from integer without a cast
int* i = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_java_Sequence-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* j = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_java_Sequence-alloca.c:7:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1_true-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1_true-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* debug = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_LarrazOliverasRodriguez-CarbonellRubio-2013FMCAD-Fig1_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_LarrazOliverasRodriguez-CarbonellRubio-2013FMCAD-Fig1_true-alloca.c:4:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_LarrazOliverasRodriguez-CarbonellRubio-2013FMCAD-Fig1_true-alloca.c:5:14: warning: initialization makes pointer from integer without a cast
int* y = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_LarrazOliverasRodriguez-CarbonellRubio-2013FMCAD-Fig1_true-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* z = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Masse_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_Masse_true-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_min_rf_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_min_rf_true-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_min_rf_true-alloca.c:7:14: warning: initialization makes pointer from integer without a cast
int* y = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_min_rf_true-alloca.c:8:14: warning: initialization makes pointer from integer without a cast
int* z = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_mult_array_alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_mult_array_alloca.c:10:14: warning: initialization makes pointer from integer without a cast
int *arr = alloca(length*sizeof(int));
^
AProVE_memory_alloca/svcomp_mult_array_alloca.c:11:15: warning: initialization makes pointer from integer without a cast
int *arr2 = alloca(fac*length*sizeof(int));
^
AProVE_memory_alloca/svcomp_NoriSharma-2013FSE-Fig7_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_NoriSharma-2013FSE-Fig7_true-alloca.c:4:14: warning: initialization makes pointer from integer without a cast
int* a = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_NoriSharma-2013FSE-Fig7_true-alloca.c:5:14: warning: initialization makes pointer from integer without a cast
int* i = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_NoriSharma-2013FSE-Fig7_true-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* b = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_NoriSharma-2013FSE-Fig7_true-alloca.c:7:14: warning: initialization makes pointer from integer without a cast
int* j = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_NoriSharma-2013FSE-Fig7_true-alloca.c:8:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_NoriSharma-2013FSE-Fig7_true-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* M = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_NoriSharma-2013FSE-Fig7_true-alloca.c:10:14: warning: initialization makes pointer from integer without a cast
int* N = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_NoriSharma-2013FSE-Fig8_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_NoriSharma-2013FSE-Fig8_true-alloca.c:4:14: warning: initialization makes pointer from integer without a cast
int* u = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_NoriSharma-2013FSE-Fig8_true-alloca.c:5:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_NoriSharma-2013FSE-Fig8_true-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* v = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_NoriSharma-2013FSE-Fig8_true-alloca.c:7:14: warning: initialization makes pointer from integer without a cast
int* y = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_NoriSharma-2013FSE-Fig8_true-alloca.c:8:14: warning: initialization makes pointer from integer without a cast
int* w = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_NoriSharma-2013FSE-Fig8_true-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* z = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_NoriSharma-2013FSE-Fig8_true-alloca.c:10:14: warning: initialization makes pointer from integer without a cast
int* c = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_openbsd_cstrstr_alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_openbsd_cstrstr_alloca.c:69:5: warning: return makes integer from pointer without a cast
return cstrstr(nondetString1,nondetString2);
^
AProVE_memory_alloca/svcomp_PodelskiRybalchenko-2004VMCAI-Ex2_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_PodelskiRybalchenko-2004VMCAI-Ex2_true-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_stroeder1_alloca.c: In function ‘sumOfThirdBytes’:
AProVE_memory_alloca/svcomp_stroeder1_alloca.c:11:11: warning: assignment from incompatible pointer type
p = &(numbers[i]);
^
AProVE_memory_alloca/svcomp_stroeder2_alloca.c: In function ‘sumOfThirdBytes’:
AProVE_memory_alloca/svcomp_stroeder2_alloca.c:11:11: warning: assignment from incompatible pointer type
p = &(numbers[i]);
^
AProVE_memory_alloca/svcomp_TelAviv-Amir-Minimum_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_TelAviv-Amir-Minimum_true-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_TelAviv-Amir-Minimum_true-alloca.c:7:14: warning: initialization makes pointer from integer without a cast
int* y = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Toulouse-BranchesToLoop_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_Toulouse-BranchesToLoop_true-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Toulouse-BranchesToLoop_true-alloca.c:7:14: warning: initialization makes pointer from integer without a cast
int* y = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Toulouse-BranchesToLoop_true-alloca.c:8:14: warning: initialization makes pointer from integer without a cast
int* z = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Toulouse-BranchesToLoop_true-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* m = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Toulouse-BranchesToLoop_true-alloca.c:10:14: warning: initialization makes pointer from integer without a cast
int* n = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Toulouse-MultiBranchesToLoop_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_Toulouse-MultiBranchesToLoop_true-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Toulouse-MultiBranchesToLoop_true-alloca.c:7:14: warning: initialization makes pointer from integer without a cast
int* y = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Toulouse-MultiBranchesToLoop_true-alloca.c:8:14: warning: initialization makes pointer from integer without a cast
int* z = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Toulouse-MultiBranchesToLoop_true-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* m = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Toulouse-MultiBranchesToLoop_true-alloca.c:10:14: warning: initialization makes pointer from integer without a cast
int* n = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_twisted-alloca.c: In function ‘f’:
AProVE_memory_alloca/svcomp_twisted-alloca.c:7:18: warning: initialization makes pointer from integer without a cast
int* k_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_twisted-alloca.c:8:18: warning: initialization makes pointer from integer without a cast
int* l_ref = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_twisted-alloca.c:9:14: warning: initialization makes pointer from integer without a cast
int* i = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_twisted-alloca.c:10:14: warning: initialization makes pointer from integer without a cast
int* j = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Urban_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_Urban_true-alloca.c:6:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Urban_true-alloca.c:7:14: warning: initialization makes pointer from integer without a cast
int* y = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Urban-2013WST-Fig1_false-unreach-label-termination-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_Urban-2013WST-Fig1_false-unreach-label-termination-alloca.c:4:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Urban-2013WST-Fig2_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_Urban-2013WST-Fig2_true-alloca.c:4:15: warning: initialization makes pointer from integer without a cast
int* x1 = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Urban-2013WST-Fig2_true-alloca.c:5:15: warning: initialization makes pointer from integer without a cast
int* x2 = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Urban-2013WST-Fig2-modified1000_true-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_Urban-2013WST-Fig2-modified1000_true-alloca.c:4:15: warning: initialization makes pointer from integer without a cast
int* x1 = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Urban-2013WST-Fig2-modified1000_true-alloca.c:5:15: warning: initialization makes pointer from integer without a cast
int* x2 = alloca(sizeof(int));
^
AProVE_memory_alloca/svcomp_Velroyen_false-unreach-label-termination-alloca.c: In function ‘main’:
AProVE_memory_alloca/svcomp_Velroyen_false-unreach-label-termination-alloca.c:4:14: warning: initialization makes pointer from integer without a cast
int* x = alloca(sizeof(int));
^
AProVE_memory_unsafe/svcomp_add_last_unsafe.c: In function ‘main’:
AProVE_memory_unsafe/svcomp_add_last_unsafe.c:8:14: warning: initialization makes pointer from integer without a cast
int *arr = alloca(length);
^
AProVE_memory_unsafe/svcomp_count_down_unsafe.c: In function ‘main’:
AProVE_memory_unsafe/svcomp_count_down_unsafe.c:9:14: warning: initialization makes pointer from integer without a cast
int *arr = alloca(length);
^
AProVE_memory_unsafe/svcomp_mult_array_unsafe.c: In function ‘main’:
AProVE_memory_unsafe/svcomp_mult_array_unsafe.c:10:14: warning: initialization makes pointer from integer without a cast
int *arr = alloca(length);
^
AProVE_memory_unsafe/svcomp_mult_array_unsafe.c:11:15: warning: initialization makes pointer from integer without a cast
int *arr2 = alloca(fac*length);
^
AProVE_memory_unsafe/svcomp_reverse_array_alloca_unsafe.c: In function ‘main’:
AProVE_memory_unsafe/svcomp_reverse_array_alloca_unsafe.c:10:14: warning: initialization makes pointer from integer without a cast
int *arr = alloca(length*sizeof(int));
^
AProVE_memory_unsafe/svcomp_reverse_array_unsafe.c: In function ‘main’:
AProVE_memory_unsafe/svcomp_reverse_array_unsafe.c:10:14: warning: initialization makes pointer from integer without a cast
int *arr = alloca(length);
^
AProVE_memory_unsafe/svcomp_stroeder1_unsafe.c: In function ‘sumOfThirdBytes’:
AProVE_memory_unsafe/svcomp_stroeder1_unsafe.c:9:11: warning: assignment from incompatible pointer type
p = &(numbers[i]);
^
AProVE_memory_unsafe/svcomp_stroeder2_unsafe.c: In function ‘sumOfThirdBytes’:
AProVE_memory_unsafe/svcomp_stroeder2_unsafe.c:9:11: warning: assignment from incompatible pointer type
p = &(numbers[i]);
^
AProVE_numeric/LogRecursive_true.c:16:5: warning: conflicting types for built-in function ‘log’
int log(int x, int y);
^
SV-COMP_Termination_Category/joey_false-termination.c: In function ‘rec’:
SV-COMP_Termination_Category/joey_false-termination.c:15:18: warning: operation on ‘x’ may be undefined [-Wsequence-point]
return rec(++x) + rec(--x);
^
Ultimate/4BitCounterPointer_true-termination.c: In function ‘main’:
Ultimate/4BitCounterPointer_true-termination.c:8:12: warning: initialization makes pointer from integer without a cast
int* x0 = alloca(sizeof(int));
^
Ultimate/4BitCounterPointer_true-termination.c:9:12: warning: initialization makes pointer from integer without a cast
int* x1 = alloca(sizeof(int));
^
Ultimate/4BitCounterPointer_true-termination.c:10:12: warning: initialization makes pointer from integer without a cast
int* x2 = alloca(sizeof(int));
^
Ultimate/4BitCounterPointer_true-termination.c:11:12: warning: initialization makes pointer from integer without a cast
int* x3 = alloca(sizeof(int));
^
More information about the Termtools
mailing list