Skip to content
Snippets Groups Projects
Commit e0c1813d authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[tests] expected oracles

parent 1d043d3d
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 359 additions and 360 deletions
src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle
+ 13
− 13
View file @ e0c1813d
......@@ -7,12 +7,12 @@
out of bounds read. assert \valid_read((int *)*list);
[eva:alarm] sum_with_unspecified_sequence.c:14: Warning:
signed overflow.
assert -2147483648 ≤ ret + tmp_unroll_5;
(tmp_unroll_5 from vararg)
assert -2147483648 ≤ ret + tmp_unfold_5;
(tmp_unfold_5 from vararg)
[eva:alarm] sum_with_unspecified_sequence.c:14: Warning:
signed overflow.
assert ret + tmp_unroll_5 ≤ 2147483647;
(tmp_unroll_5 from vararg)
assert ret + tmp_unfold_5 ≤ 2147483647;
(tmp_unfold_5 from vararg)
[eva:alarm] sum_with_unspecified_sequence.c:14: Warning:
out of bounds read. assert \valid_read(list);
[eva:alarm] sum_with_unspecified_sequence.c:14: Warning:
......@@ -43,20 +43,20 @@ int sum(int n, void * const *__va_params)
int ret = 0;
list = __va_params;
i = 0;
if (! (i < n)) goto unrolling_2_loop;
if (! (i < n)) goto unfolding_2_loop;
{
int tmp_unroll_5;
int tmp_unfold_5;
/*@ assert Eva: mem_access: \valid_read(list); */
/*@ assert Eva: mem_access: \valid_read((int *)*list); */
tmp_unroll_5 = *((int *)*list);
tmp_unfold_5 = *((int *)*list);
list ++;
/*@ assert Eva: signed_overflow: -2147483648 ≤ ret + tmp_unroll_5; */
/*@ assert Eva: signed_overflow: ret + tmp_unroll_5 ≤ 2147483647; */
ret += tmp_unroll_5;
/*@ assert Eva: signed_overflow: -2147483648 ≤ ret + tmp_unfold_5; */
/*@ assert Eva: signed_overflow: ret + tmp_unfold_5 ≤ 2147483647; */
ret += tmp_unfold_5;
}
i ++;
unrolling_3_loop: ;
/*@ loop pragma UNROLL "done", 1; */
unfolding_3_loop: ;
/*@ loop unfold "done", 1; */
while (i < n) {
{
int tmp;
......@@ -70,7 +70,7 @@ int sum(int n, void * const *__va_params)
}
i ++;
}
unrolling_2_loop: ;
unfolding_2_loop: ;
return ret;
}
......
src/plugins/wp/tests/wp_plugin/doomed_unroll.i
+ 1
− 1
View file @ e0c1813d
......@@ -10,7 +10,7 @@ void foo(void)
{
int n = 3 ;
/*@
loop pragma UNROLL "completely", 4 ;
loop unfold "completely", 4 ;
*/
while (n>0) n--;
}
src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle
+ 11
− 11
View file @ e0c1813d
......@@ -45,24 +45,24 @@ Prove: true.
void foo(void)
{
int n = 3;
if (! (n > 0)) goto unrolling_2_loop;
if (! (n > 0)) goto unfolding_2_loop;
n --;
unrolling_6_loop: ;
if (! (n > 0)) goto unrolling_2_loop;
unfolding_6_loop: ;
if (! (n > 0)) goto unfolding_2_loop;
n --;
unrolling_5_loop: ;
if (! (n > 0)) goto unrolling_2_loop;
unfolding_5_loop: ;
if (! (n > 0)) goto unfolding_2_loop;
n --;
unrolling_4_loop: ;
if (! (n > 0)) goto unrolling_2_loop;
unfolding_4_loop: ;
if (! (n > 0)) goto unfolding_2_loop;
n --;
unrolling_3_loop: ;
unfolding_3_loop: ;
/*@ loop invariant \false;
loop pragma UNROLL "completely", 4;
loop pragma UNROLL "done", 4;
loop unfold "completely", 4;
loop unfold "done", 4;
*/
while (n > 0) n --;
unrolling_2_loop: ;
unfolding_2_loop: ;
return;
}
......
src/plugins/wp/tests/wp_plugin/repeat.c
+ 4
− 4
View file @ e0c1813d
......@@ -43,7 +43,7 @@ void master(void)
*/
void unroll(void)
{
/*@ loop pragma UNROLL "completely", U; */
/*@ loop unfold "completely", U; */
for (int i = 0; i < N; i++)
{ f(); g(); }
return;
......@@ -57,7 +57,7 @@ void unroll(void)
*/
void induction(int n)
{
/*@
/*@
loop invariant 0 <= i <= n;
loop invariant CALL == [| F , G |] *^ i;
loop assigns i,calls;
......@@ -77,8 +77,8 @@ void induction(int n)
void shifted(int n)
{
f();
/*@
/*@
loop invariant 0 <= i <= n;
loop invariant CALL == ([| F , G |] *^ i ^ [| F |]);
loop assigns i,calls;
......
src/plugins/wp/tests/wp_plugin/unroll.i
+ 1
− 1
View file @ e0c1813d
......@@ -17,6 +17,6 @@ enum {Max = 16};
@ ensures zero: zeroed(t,0,Max-1);
*/
void unrolled_loop(unsigned *t){
//@ loop pragma UNROLL "completely", Max+1;
//@ loop unfold "completely", Max+1;
for (unsigned i=0; i<Max; i++) t[i] = 0;
}
tests/cil/comments.c
+ 1
− 1
View file @ e0c1813d
......@@ -19,7 +19,7 @@ int bts_2176() {
1 */
r = /* comment 2 */ 1;
//@ loop pragma UNROLL 10;
//@ loop unfold 10;
for(i=0; i<10; i++) {
r += 1;
}
......
tests/cil/oracle/comments.res.oracle
+ 23
− 23
View file @ e0c1813d
......@@ -30,53 +30,53 @@ int bts_2176(void)
// comment 2
r = 1;
i = 0;
if (! (i < 10)) goto unrolling_2_loop;
if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
unrolling_12_loop: ;
if (! (i < 10)) goto unrolling_2_loop;
unfolding_12_loop: ;
if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
unrolling_11_loop: ;
if (! (i < 10)) goto unrolling_2_loop;
unfolding_11_loop: ;
if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
unrolling_10_loop: ;
if (! (i < 10)) goto unrolling_2_loop;
unfolding_10_loop: ;
if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
unrolling_9_loop: ;
if (! (i < 10)) goto unrolling_2_loop;
unfolding_9_loop: ;
if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
unrolling_8_loop: ;
if (! (i < 10)) goto unrolling_2_loop;
unfolding_8_loop: ;
if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
unrolling_7_loop: ;
if (! (i < 10)) goto unrolling_2_loop;
unfolding_7_loop: ;
if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
unrolling_6_loop: ;
if (! (i < 10)) goto unrolling_2_loop;
unfolding_6_loop: ;
if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
unrolling_5_loop: ;
if (! (i < 10)) goto unrolling_2_loop;
unfolding_5_loop: ;
if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
unrolling_4_loop: ;
if (! (i < 10)) goto unrolling_2_loop;
unfolding_4_loop: ;
if (! (i < 10)) goto unfolding_2_loop;
r ++;
i ++;
unrolling_3_loop: ;
/*@ loop pragma UNROLL 10;
loop pragma UNROLL "done", 10; */
unfolding_3_loop: ;
/*@ loop unfold 10;
loop unfold "done", 10; */
while (i < 10) {
r ++;
i ++;
}
unrolling_2_loop: ;
unfolding_2_loop: ;
// comment 3
return r;
}
......
tests/float/round10d.i
+ 4
− 4
View file @ e0c1813d
......@@ -7,12 +7,12 @@ int main()
double t=0.0;
int i;
Frama_C_show_each_dixieme(0.1);
//@ loop pragma UNROLL 10;
for(i=0;i<10;i++)
{
//@ loop unfold 10;
for(i=0;i<10;i++)
{
t = t + 0.1;
Frama_C_show_each_t(t);
}
}
//@ assert t>=1.0;
return 0;
}
tests/idct/ieee_1180_1990.c
+ 2
− 2
View file @ e0c1813d
......@@ -173,7 +173,7 @@ int main()
long i, j, k, m1[8][8], m2[8][8], m3[8][8], m4[8][8], succ, omse, ome, err;
succ = 1;
/*@ loop pragma UNROLL 7; */
/*@ loop unfold 7; */
for(i = 0; i < 6; i++)
for(j = 0; j < 8; j++)
for(k = 0; k < 8; k++)
......@@ -198,7 +198,7 @@ int main()
}
/*fprintf(stderr, "------------------------------------------------->\n");*/
/* loop pragma UNROLL 0 */
/* loop unfold 0 */
for(i = 0; i < 10000; i++)
{
if((i + 1) % 200 == 0)
......
tests/metrics/cabs.i
+ 1
− 1
View file @ e0c1813d
......@@ -4,7 +4,7 @@
void main() {
int j = 1;
//@ loop pragma UNROLL 6;
//@ loop unfold 6;
for (int i=0; i<6; i++) {
j += 2;
}
......
tests/misc/oracle/bts1135_ulevel.res.oracle
+ 12
− 12
View file @ e0c1813d
......@@ -4,23 +4,23 @@ int X;
void main(int c)
{
int i = 0;
if (! (i < 10)) goto unrolling_2_loop;
if (! (i < 10)) goto unfolding_2_loop;
if (c)
/*@ ensures \false; */
goto there_unrolling_6_loop;
goto there_unfolding_6_loop;
X ++;
there_unrolling_6_loop: i ++;
/*@ assert c ≡ 0 ⇒ \at(X,there_unrolling_6_loop) ≡ i + 1; */ ;
unrolling_5_loop: ;
if (! (i < 10)) goto unrolling_2_loop;
there_unfolding_6_loop: i ++;
/*@ assert c ≡ 0 ⇒ \at(X,there_unfolding_6_loop) ≡ i + 1; */ ;
unfolding_5_loop: ;
if (! (i < 10)) goto unfolding_2_loop;
if (c)
/*@ ensures \false; */
goto there_unrolling_4_loop;
goto there_unfolding_4_loop;
X ++;
there_unrolling_4_loop: i ++;
/*@ assert c ≡ 0 ⇒ \at(X,there_unrolling_4_loop) ≡ i + 1; */ ;
unrolling_3_loop: ;
/*@ loop pragma UNROLL "done", 2; */
there_unfolding_4_loop: i ++;
/*@ assert c ≡ 0 ⇒ \at(X,there_unfolding_4_loop) ≡ i + 1; */ ;
unfolding_3_loop: ;
/*@ loop unfold "done", 2; */
while (i < 10) {
if (c)
/*@ ensures \false; */
......@@ -29,7 +29,7 @@ void main(int c)
there: i ++;
/*@ assert c ≡ 0 ⇒ \at(X,there) ≡ i + 1; */ ;
}
unrolling_2_loop: ;
unfolding_2_loop: ;
return;
}
......
tests/misc/ulevel.i
+ 1
− 1
View file @ e0c1813d
......@@ -8,7 +8,7 @@
void main(void) {
int i, j;
/*@ loop pragma UNROLL 1; */
/*@ loop unfold 1; */
for(i = 0; i < 4; i++)
for(j = 0; j < 3; j++)
;
......
tests/slicing/oracle/adpcm.res.oracle
+ 6
− 7
View file @ e0c1813d
......@@ -1531,6 +1531,12 @@ Slicing project worklist [default] =
[pdg] computing for function logscl
[pdg] done for function logscl
[slicing] applying actions: 3/3...
[slicing] tests/test/adpcm.c:277: Warning: Dropping unsupported ACSL annotation
[slicing] tests/test/adpcm.c:288: Warning: Dropping unsupported ACSL annotation
[slicing] tests/test/adpcm.c:418: Warning: Dropping unsupported ACSL annotation
[slicing] tests/test/adpcm.c:453: Warning: Dropping unsupported ACSL annotation
[slicing] tests/test/adpcm.c:506: Warning: Dropping unsupported ACSL annotation
[slicing] tests/test/adpcm.c:512: Warning: Dropping unsupported ACSL annotation
[slicing] tests/test/adpcm.c:607: Warning: Dropping unsupported ACSL annotation
[sparecode] remove unused global declarations from project 'Sliced code tmp'
[sparecode] removed unused global declarations in new project 'Sliced code'
......@@ -1822,7 +1828,6 @@ void encode_slice_1(int xin1, int xin2)
h_ptr ++;
xb = (long)*tmp_1 * (long)*tmp_2;
i = 0;
/*@ loop pragma UNROLL 11; */
while (i < 10) {
{
int *tmp_3;
......@@ -1851,7 +1856,6 @@ void encode_slice_1(int xin1, int xin2)
xb += (long)*tqmf_ptr * (long)*tmp_9;
tqmf_ptr1 = tqmf_ptr - 2;
i = 0;
/*@ loop pragma UNROLL 23; */
while (i < 22) {
int *tmp_10;
int *tmp_11;
......@@ -1921,7 +1925,6 @@ int filtez_slice_1(int *bpl, int *dlt_0)
dlt_0 ++;
zl = (long)*tmp * (long)*tmp_0;
i = 1;
/*@ loop pragma UNROLL 7; */
while (i < 6) {
int *tmp_1;
int *tmp_2;
......@@ -1958,7 +1961,6 @@ int quantl_slice_1(int el_0, int detl_0)
wd = (long)abs_slice_1(el_0);
mil = 0;
decis = (long)decis_levl[mil] * (long)detl_0 >> 15L;
/*@ loop pragma UNROLL 30; */
while (1) {
if (wd <= decis) {
if (! (mil < 29)) break;
......@@ -2001,7 +2003,6 @@ void upzero_slice_1(int dlt_0, int *dlti, int *bli)
int wd3;
if (dlt_0 == 0) {
i = 0;
/*@ loop pragma UNROLL 7; */
while (i < 6) {
*(bli + i) = (int)(255L * (long)*(bli + i) >> 8L);
i ++;
......@@ -2009,7 +2010,6 @@ void upzero_slice_1(int dlt_0, int *dlti, int *bli)
}
else {
i = 0;
/*@ loop pragma UNROLL 7; */
while (i < 6) {
if ((long)dlt_0 * (long)*(dlti + i) >= (long)0) wd2 = 128;
else wd2 = -128;
......@@ -2071,7 +2071,6 @@ void main(void)
{
int i;
i = 0;
/*@ loop pragma UNROLL 11; */
while (i < 10) {
encode_slice_1(test_data[i],test_data[i + 1]);
i += 2;
......
tests/slicing/oracle/bts1768.res.oracle
+ 1
− 1
View file @ e0c1813d
......@@ -163,6 +163,7 @@
[slicing] exporting project to 'Slicing export'...
[slicing] applying all slicing requests...
[slicing] applying 0 actions...
[slicing] bts1768.i:44: Warning: Dropping unsupported ACSL annotation
[sparecode] remove unused global declarations from project 'Slicing export tmp'
[sparecode] removed unused global declarations in new project 'Slicing export'
/* Generated by Frama-C */
......@@ -226,7 +227,6 @@ void main(void)
lecture_slice_1();
fsm_transition_slice_1();
step ++;
/*@ loop pragma UNROLL "done", 10; */
while (1) {
lecture_slice_1();
fsm_transition_slice_1();
......
tests/spec/breaks_continues_unroll.i
+ 3
− 3
View file @ e0c1813d
......@@ -3,13 +3,13 @@
// Semantics of unrolling
int unroll (int c) {
int x = 0;
//@ loop pragma UNROLL 1;
//@ loop unfold 1;
while (1) {
/*@ breaks \false;
continues x == \old(x) + 1; */
switch (x) {
/*@ breaks x == 13; */
{
{
case 11: x++; continue;
case 12: x++;
case 13: break;
......@@ -24,4 +24,4 @@ int unroll (int c) {
}
}
return x;
}
}
tests/spec/loop_labels_unroll.i
+ 2
− 2
View file @ e0c1813d
......@@ -2,8 +2,8 @@ int main () {
int x = 0;
/*@
loop pragma UNROLL 4;
/*@
loop unfold 4;
loop invariant \at(x,LoopEntry) == 0;
loop invariant \at(x,LoopCurrent) <= 15;
*/
......
tests/spec/oracle/breaks_continues_unroll.res.oracle
+ 7
− 7
View file @ e0c1813d
......@@ -7,7 +7,7 @@ int unroll(int c)
/*@ breaks x ≡ 13; */
{
case 11: x ++;
goto unrolling_3_loop;
goto unfolding_3_loop;
case 12: x ++;
case 13: break;
default: ;
......@@ -15,12 +15,12 @@ int unroll(int c)
}
if (x < c) {
x ++;
goto unrolling_3_loop;
goto unfolding_3_loop;
}
goto unrolling_2_loop;
unrolling_3_loop: ;
/*@ loop pragma UNROLL 1;
loop pragma UNROLL "done", 1; */
goto unfolding_2_loop;
unfolding_3_loop: ;
/*@ loop unfold 1;
loop unfold "done", 1; */
while (1) {
/*@ breaks \false;
continues x ≡ \old(x) + 1; */
......@@ -44,7 +44,7 @@ int unroll(int c)
break;
}
}
unrolling_2_loop: ;
unfolding_2_loop: ;
return x;
}
......
tests/spec/oracle/loop_labels_unroll.res.oracle
+ 40
− 40
View file @ e0c1813d
......@@ -4,63 +4,63 @@ int main(void)
{
int __retres;
int x = 0;
unrolling_7_loop: ;
if (! (x < 15)) goto unrolling_2_loop;
unfolding_7_loop: ;
if (! (x < 15)) goto unfolding_2_loop;
{
x ++;
/*@ assert x ≡ \at(x,unrolling_7_loop) + 1; */ ;
int i_unroll_32 = 0;
/*@ loop invariant \at(i_unroll_32,LoopEntry) ≡ 0; */
while (i_unroll_32 < 4) {
i_unroll_32 ++;
/*@ assert \at(i_unroll_32,LoopCurrent) ≡ i_unroll_32 - 1; */ ;
/*@ assert x ≡ \at(x,unfolding_7_loop) + 1; */ ;
int i_unfold_32 = 0;
/*@ loop invariant \at(i_unfold_32,LoopEntry) ≡ 0; */
while (i_unfold_32 < 4) {
i_unfold_32 ++;
/*@ assert \at(i_unfold_32,LoopCurrent) ≡ i_unfold_32 - 1; */ ;
}
/*@ assert i_unroll_32 > 0; */ ;
/*@ assert i_unfold_32 > 0; */ ;
}
unrolling_6_loop: ;
if (! (x < 15)) goto unrolling_2_loop;
unfolding_6_loop: ;
if (! (x < 15)) goto unfolding_2_loop;
{
x ++;
/*@ assert x ≡ \at(x,unrolling_6_loop) + 1; */ ;
int i_unroll_24 = 0;
/*@ loop invariant \at(i_unroll_24,LoopEntry) ≡ 0; */
while (i_unroll_24 < 4) {
i_unroll_24 ++;
/*@ assert \at(i_unroll_24,LoopCurrent) ≡ i_unroll_24 - 1; */ ;
/*@ assert x ≡ \at(x,unfolding_6_loop) + 1; */ ;
int i_unfold_24 = 0;
/*@ loop invariant \at(i_unfold_24,LoopEntry) ≡ 0; */
while (i_unfold_24 < 4) {
i_unfold_24 ++;
/*@ assert \at(i_unfold_24,LoopCurrent) ≡ i_unfold_24 - 1; */ ;
}
/*@ assert i_unroll_24 > 0; */ ;
/*@ assert i_unfold_24 > 0; */ ;
}
unrolling_5_loop: ;
if (! (x < 15)) goto unrolling_2_loop;
unfolding_5_loop: ;
if (! (x < 15)) goto unfolding_2_loop;
{
x ++;
/*@ assert x ≡ \at(x,unrolling_5_loop) + 1; */ ;
int i_unroll_16 = 0;
/*@ loop invariant \at(i_unroll_16,LoopEntry) ≡ 0; */
while (i_unroll_16 < 4) {
i_unroll_16 ++;
/*@ assert \at(i_unroll_16,LoopCurrent) ≡ i_unroll_16 - 1; */ ;
/*@ assert x ≡ \at(x,unfolding_5_loop) + 1; */ ;
int i_unfold_16 = 0;
/*@ loop invariant \at(i_unfold_16,LoopEntry) ≡ 0; */
while (i_unfold_16 < 4) {
i_unfold_16 ++;
/*@ assert \at(i_unfold_16,LoopCurrent) ≡ i_unfold_16 - 1; */ ;
}
/*@ assert i_unroll_16 > 0; */ ;
/*@ assert i_unfold_16 > 0; */ ;
}
unrolling_4_loop: ;
if (! (x < 15)) goto unrolling_2_loop;
unfolding_4_loop: ;
if (! (x < 15)) goto unfolding_2_loop;
{
x ++;
/*@ assert x ≡ \at(x,unrolling_4_loop) + 1; */ ;
int i_unroll_8 = 0;
/*@ loop invariant \at(i_unroll_8,LoopEntry) ≡ 0; */
while (i_unroll_8 < 4) {
i_unroll_8 ++;
/*@ assert \at(i_unroll_8,LoopCurrent) ≡ i_unroll_8 - 1; */ ;
/*@ assert x ≡ \at(x,unfolding_4_loop) + 1; */ ;
int i_unfold_8 = 0;
/*@ loop invariant \at(i_unfold_8,LoopEntry) ≡ 0; */
while (i_unfold_8 < 4) {
i_unfold_8 ++;
/*@ assert \at(i_unfold_8,LoopCurrent) ≡ i_unfold_8 - 1; */ ;
}
/*@ assert i_unroll_8 > 0; */ ;
/*@ assert i_unfold_8 > 0; */ ;
}
unrolling_3_loop: ;
unfolding_3_loop: ;
/*@ loop invariant \at(x,LoopEntry) ≡ 0;
loop invariant \at(x,LoopCurrent) ≤ 15;
loop pragma UNROLL 4;
loop pragma UNROLL "done", 4;
loop unfold 4;
loop unfold "done", 4;
*/
while (x < 15) {
x ++;
......@@ -73,7 +73,7 @@ int main(void)
}
/*@ assert i > 0; */ ;
}
unrolling_2_loop: ;
unfolding_2_loop: ;
__retres = 0;
return __retres;
}
......
tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle
+ 63
− 63
View file @ e0c1813d
......@@ -174,61 +174,61 @@ void main(void)
tmp_0 = gen_nondet(68);
if (tmp_0) goto L1;
{
int tmp_1_unroll_41;
case 1: tmp_1_unroll_41 = gen_nondet(71);
if (tmp_1_unroll_41) goto L1_unrolling_11_loop;
L_unrolling_8_loop: x = y;
int tmp_1_unfold_41;
case 1: tmp_1_unfold_41 = gen_nondet(71);
if (tmp_1_unfold_41) goto L1_unfolding_11_loop;
L_unfolding_8_loop: x = y;
case 2:
{
int j_unroll_40;
int i_unroll_40 = 0;
if (! (i_unroll_40 < 4)) goto unrolling_2_loop_unrolling_12_loop;
int j_unfold_40;
int i_unfold_40 = 0;
if (! (i_unfold_40 < 4)) goto unfolding_2_loop_unfolding_12_loop;
{
int tmp_2_unroll_12_unroll_26;
int tmp_3_unroll_12_unroll_26;
int tmp_4_unroll_12_unroll_26;
int tmp_5_unroll_12_unroll_26;
L1_unrolling_4_loop_unrolling_9_loop: j_unroll_40 = gen_nondet(76);
tmp_2_unroll_12_unroll_26 = gen_nondet(77);
if (tmp_2_unroll_12_unroll_26 > 10) i_unroll_40 = 10;
else i_unroll_40 = 0;
Frama_C_show_each_i_(i_unroll_40);
tmp_3_unroll_12_unroll_26 = gen_nondet(79);
if (tmp_3_unroll_12_unroll_26) goto L_unrolling_8_loop;
tmp_4_unroll_12_unroll_26 = gen_nondet(80);
if (tmp_4_unroll_12_unroll_26) goto L0;
tmp_5_unroll_12_unroll_26 = gen_nondet(81);
if (tmp_5_unroll_12_unroll_26) goto L3;
int tmp_2_unfold_12_unfold_26;
int tmp_3_unfold_12_unfold_26;
int tmp_4_unfold_12_unfold_26;
int tmp_5_unfold_12_unfold_26;
L1_unfolding_4_loop_unfolding_9_loop: j_unfold_40 = gen_nondet(76);
tmp_2_unfold_12_unfold_26 = gen_nondet(77);
if (tmp_2_unfold_12_unfold_26 > 10) i_unfold_40 = 10;
else i_unfold_40 = 0;
Frama_C_show_each_i_(i_unfold_40);
tmp_3_unfold_12_unfold_26 = gen_nondet(79);
if (tmp_3_unfold_12_unfold_26) goto L_unfolding_8_loop;
tmp_4_unfold_12_unfold_26 = gen_nondet(80);
if (tmp_4_unfold_12_unfold_26) goto L0;
tmp_5_unfold_12_unfold_26 = gen_nondet(81);
if (tmp_5_unfold_12_unfold_26) goto L3;
}
i_unroll_40 ++;
unrolling_3_loop_unrolling_10_loop: ;
/*@ loop pragma UNROLL "done", 1; */
while (i_unroll_40 < 4) {
i_unfold_40 ++;
unfolding_3_loop_unfolding_10_loop: ;
/*@ loop unfold "done", 1; */
while (i_unfold_40 < 4) {
{
int tmp_2_unroll_37;
int tmp_3_unroll_37;
int tmp_4_unroll_37;
int tmp_5_unroll_37;
L1_unrolling_11_loop: j_unroll_40 = gen_nondet(76);
tmp_2_unroll_37 = gen_nondet(77);
if (tmp_2_unroll_37 > 10) i_unroll_40 = 10; else i_unroll_40 = 0;
Frama_C_show_each_i_(i_unroll_40);
tmp_3_unroll_37 = gen_nondet(79);
if (tmp_3_unroll_37) goto L_unrolling_8_loop;
tmp_4_unroll_37 = gen_nondet(80);
if (tmp_4_unroll_37) goto L0;
tmp_5_unroll_37 = gen_nondet(81);
if (tmp_5_unroll_37) goto L3;
int tmp_2_unfold_37;
int tmp_3_unfold_37;
int tmp_4_unfold_37;
int tmp_5_unfold_37;
L1_unfolding_11_loop: j_unfold_40 = gen_nondet(76);
tmp_2_unfold_37 = gen_nondet(77);
if (tmp_2_unfold_37 > 10) i_unfold_40 = 10; else i_unfold_40 = 0;
Frama_C_show_each_i_(i_unfold_40);
tmp_3_unfold_37 = gen_nondet(79);
if (tmp_3_unfold_37) goto L_unfolding_8_loop;
tmp_4_unfold_37 = gen_nondet(80);
if (tmp_4_unfold_37) goto L0;
tmp_5_unfold_37 = gen_nondet(81);
if (tmp_5_unfold_37) goto L3;
}
i_unroll_40 ++;
i_unfold_40 ++;
}
unrolling_2_loop_unrolling_12_loop: ;
unfolding_2_loop_unfolding_12_loop: ;
}
}
n --;
if (! (n > 0)) goto unrolling_6_loop;
unrolling_7_loop: ;
/*@ loop pragma UNROLL "done", 1; */
if (! (n > 0)) goto unfolding_6_loop;
unfolding_7_loop: ;
/*@ loop unfold "done", 1; */
while (1) {
{
int tmp_1;
......@@ -238,26 +238,26 @@ void main(void)
{
int j;
int i = 0;
if (! (i < 4)) goto unrolling_2_loop;
if (! (i < 4)) goto unfolding_2_loop;
{
int tmp_2_unroll_12;
int tmp_3_unroll_12;
int tmp_4_unroll_12;
int tmp_5_unroll_12;
L1_unrolling_4_loop: j = gen_nondet(76);
tmp_2_unroll_12 = gen_nondet(77);
if (tmp_2_unroll_12 > 10) i = 10; else i = 0;
int tmp_2_unfold_12;
int tmp_3_unfold_12;
int tmp_4_unfold_12;
int tmp_5_unfold_12;
L1_unfolding_4_loop: j = gen_nondet(76);
tmp_2_unfold_12 = gen_nondet(77);
if (tmp_2_unfold_12 > 10) i = 10; else i = 0;
Frama_C_show_each_i_(i);
tmp_3_unroll_12 = gen_nondet(79);
if (tmp_3_unroll_12) goto L;
tmp_4_unroll_12 = gen_nondet(80);
if (tmp_4_unroll_12) goto L0;
tmp_5_unroll_12 = gen_nondet(81);
if (tmp_5_unroll_12) goto L3;
tmp_3_unfold_12 = gen_nondet(79);
if (tmp_3_unfold_12) goto L;
tmp_4_unfold_12 = gen_nondet(80);
if (tmp_4_unfold_12) goto L0;
tmp_5_unfold_12 = gen_nondet(81);
if (tmp_5_unfold_12) goto L3;
}
i ++;
unrolling_3_loop: ;
/*@ loop pragma UNROLL "done", 1; */
unfolding_3_loop: ;
/*@ loop unfold "done", 1; */
while (i < 4) {
{
int tmp_2;
......@@ -277,13 +277,13 @@ void main(void)
}
i ++;
}
unrolling_2_loop: ;
unfolding_2_loop: ;
}
}
n --;
if (! (n > 0)) break;
}
unrolling_6_loop: ;
unfolding_6_loop: ;
Frama_C_show_each_y_(y);
Frama_C_show_each_x_(x);
}
......
tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle
+ 163
− 163
View file @ e0c1813d
......@@ -174,160 +174,160 @@ void main(void)
tmp_0 = gen_nondet(68);
if (tmp_0) goto L1;
{
int tmp_1_unroll_106;
case 1: tmp_1_unroll_106 = gen_nondet(71);
if (tmp_1_unroll_106) goto L1_unrolling_23_loop;
L_unrolling_18_loop: x = y;
int tmp_1_unfold_106;
case 1: tmp_1_unfold_106 = gen_nondet(71);
if (tmp_1_unfold_106) goto L1_unfolding_23_loop;
L_unfolding_18_loop: x = y;
case 2:
{
int j_unroll_105;
int i_unroll_105 = 0;
if (! (i_unroll_105 < 4)) goto unrolling_2_loop_unrolling_24_loop;
int j_unfold_105;
int i_unfold_105 = 0;
if (! (i_unfold_105 < 4)) goto unfolding_2_loop_unfolding_24_loop;
{
int tmp_2_unroll_24_unroll_80;
int tmp_3_unroll_24_unroll_80;
int tmp_4_unroll_24_unroll_80;
int tmp_5_unroll_24_unroll_80;
L1_unrolling_6_loop_unrolling_19_loop:
j_unroll_105 = gen_nondet(76);
tmp_2_unroll_24_unroll_80 = gen_nondet(77);
if (tmp_2_unroll_24_unroll_80 > 10) i_unroll_105 = 10;
else i_unroll_105 = 0;
Frama_C_show_each_i_(i_unroll_105);
tmp_3_unroll_24_unroll_80 = gen_nondet(79);
if (tmp_3_unroll_24_unroll_80) goto L_unrolling_18_loop;
tmp_4_unroll_24_unroll_80 = gen_nondet(80);
if (tmp_4_unroll_24_unroll_80) goto L0;
tmp_5_unroll_24_unroll_80 = gen_nondet(81);
if (tmp_5_unroll_24_unroll_80) goto L3;
int tmp_2_unfold_24_unfold_80;
int tmp_3_unfold_24_unfold_80;
int tmp_4_unfold_24_unfold_80;
int tmp_5_unfold_24_unfold_80;
L1_unfolding_6_loop_unfolding_19_loop:
j_unfold_105 = gen_nondet(76);
tmp_2_unfold_24_unfold_80 = gen_nondet(77);
if (tmp_2_unfold_24_unfold_80 > 10) i_unfold_105 = 10;
else i_unfold_105 = 0;
Frama_C_show_each_i_(i_unfold_105);
tmp_3_unfold_24_unfold_80 = gen_nondet(79);
if (tmp_3_unfold_24_unfold_80) goto L_unfolding_18_loop;
tmp_4_unfold_24_unfold_80 = gen_nondet(80);
if (tmp_4_unfold_24_unfold_80) goto L0;
tmp_5_unfold_24_unfold_80 = gen_nondet(81);
if (tmp_5_unfold_24_unfold_80) goto L3;
}
i_unroll_105 ++;
unrolling_5_loop_unrolling_20_loop: ;
if (! (i_unroll_105 < 4)) goto unrolling_2_loop_unrolling_24_loop;
i_unfold_105 ++;
unfolding_5_loop_unfolding_20_loop: ;
if (! (i_unfold_105 < 4)) goto unfolding_2_loop_unfolding_24_loop;
{
int tmp_2_unroll_12_unroll_91;
int tmp_3_unroll_12_unroll_91;
int tmp_4_unroll_12_unroll_91;
int tmp_5_unroll_12_unroll_91;
L1_unrolling_4_loop_unrolling_21_loop:
j_unroll_105 = gen_nondet(76);
tmp_2_unroll_12_unroll_91 = gen_nondet(77);
if (tmp_2_unroll_12_unroll_91 > 10) i_unroll_105 = 10;
else i_unroll_105 = 0;
Frama_C_show_each_i_(i_unroll_105);
tmp_3_unroll_12_unroll_91 = gen_nondet(79);
if (tmp_3_unroll_12_unroll_91) goto L_unrolling_18_loop;
tmp_4_unroll_12_unroll_91 = gen_nondet(80);
if (tmp_4_unroll_12_unroll_91) goto L0;
tmp_5_unroll_12_unroll_91 = gen_nondet(81);
if (tmp_5_unroll_12_unroll_91) goto L3;
int tmp_2_unfold_12_unfold_91;
int tmp_3_unfold_12_unfold_91;
int tmp_4_unfold_12_unfold_91;
int tmp_5_unfold_12_unfold_91;
L1_unfolding_4_loop_unfolding_21_loop:
j_unfold_105 = gen_nondet(76);
tmp_2_unfold_12_unfold_91 = gen_nondet(77);
if (tmp_2_unfold_12_unfold_91 > 10) i_unfold_105 = 10;
else i_unfold_105 = 0;
Frama_C_show_each_i_(i_unfold_105);
tmp_3_unfold_12_unfold_91 = gen_nondet(79);
if (tmp_3_unfold_12_unfold_91) goto L_unfolding_18_loop;
tmp_4_unfold_12_unfold_91 = gen_nondet(80);
if (tmp_4_unfold_12_unfold_91) goto L0;
tmp_5_unfold_12_unfold_91 = gen_nondet(81);
if (tmp_5_unfold_12_unfold_91) goto L3;
}
i_unroll_105 ++;
unrolling_3_loop_unrolling_22_loop: ;
/*@ loop pragma UNROLL "done", 2; */
while (i_unroll_105 < 4) {
i_unfold_105 ++;
unfolding_3_loop_unfolding_22_loop: ;
/*@ loop unfold "done", 2; */
while (i_unfold_105 < 4) {
{
int tmp_2_unroll_102;
int tmp_3_unroll_102;
int tmp_4_unroll_102;
int tmp_5_unroll_102;
L1_unrolling_23_loop: j_unroll_105 = gen_nondet(76);
tmp_2_unroll_102 = gen_nondet(77);
if (tmp_2_unroll_102 > 10) i_unroll_105 = 10;
else i_unroll_105 = 0;
Frama_C_show_each_i_(i_unroll_105);
tmp_3_unroll_102 = gen_nondet(79);
if (tmp_3_unroll_102) goto L_unrolling_18_loop;
tmp_4_unroll_102 = gen_nondet(80);
if (tmp_4_unroll_102) goto L0;
tmp_5_unroll_102 = gen_nondet(81);
if (tmp_5_unroll_102) goto L3;
int tmp_2_unfold_102;
int tmp_3_unfold_102;
int tmp_4_unfold_102;
int tmp_5_unfold_102;
L1_unfolding_23_loop: j_unfold_105 = gen_nondet(76);
tmp_2_unfold_102 = gen_nondet(77);
if (tmp_2_unfold_102 > 10) i_unfold_105 = 10;
else i_unfold_105 = 0;
Frama_C_show_each_i_(i_unfold_105);
tmp_3_unfold_102 = gen_nondet(79);
if (tmp_3_unfold_102) goto L_unfolding_18_loop;
tmp_4_unfold_102 = gen_nondet(80);
if (tmp_4_unfold_102) goto L0;
tmp_5_unfold_102 = gen_nondet(81);
if (tmp_5_unfold_102) goto L3;
}
i_unroll_105 ++;
i_unfold_105 ++;
}
unrolling_2_loop_unrolling_24_loop: ;
unfolding_2_loop_unfolding_24_loop: ;
}
}
n --;
if (! (n > 0)) goto unrolling_8_loop;
unrolling_17_loop: ;
if (! (n > 0)) goto unfolding_8_loop;
unfolding_17_loop: ;
{
int tmp_1_unroll_64;
tmp_1_unroll_64 = gen_nondet(71);
if (tmp_1_unroll_64) goto L1_unrolling_15_loop;
L_unrolling_10_loop: x = y;
int tmp_1_unfold_64;
tmp_1_unfold_64 = gen_nondet(71);
if (tmp_1_unfold_64) goto L1_unfolding_15_loop;
L_unfolding_10_loop: x = y;
{
int j_unroll_63;
int i_unroll_63 = 0;
if (! (i_unroll_63 < 4)) goto unrolling_2_loop_unrolling_16_loop;
int j_unfold_63;
int i_unfold_63 = 0;
if (! (i_unfold_63 < 4)) goto unfolding_2_loop_unfolding_16_loop;
{
int tmp_2_unroll_24_unroll_38;
int tmp_3_unroll_24_unroll_38;
int tmp_4_unroll_24_unroll_38;
int tmp_5_unroll_24_unroll_38;
L1_unrolling_6_loop_unrolling_11_loop:
j_unroll_63 = gen_nondet(76);
tmp_2_unroll_24_unroll_38 = gen_nondet(77);
if (tmp_2_unroll_24_unroll_38 > 10) i_unroll_63 = 10;
else i_unroll_63 = 0;
Frama_C_show_each_i_(i_unroll_63);
tmp_3_unroll_24_unroll_38 = gen_nondet(79);
if (tmp_3_unroll_24_unroll_38) goto L_unrolling_10_loop;
tmp_4_unroll_24_unroll_38 = gen_nondet(80);
if (tmp_4_unroll_24_unroll_38) goto L0;
tmp_5_unroll_24_unroll_38 = gen_nondet(81);
if (tmp_5_unroll_24_unroll_38) goto L3;
int tmp_2_unfold_24_unfold_38;
int tmp_3_unfold_24_unfold_38;
int tmp_4_unfold_24_unfold_38;
int tmp_5_unfold_24_unfold_38;
L1_unfolding_6_loop_unfolding_11_loop:
j_unfold_63 = gen_nondet(76);
tmp_2_unfold_24_unfold_38 = gen_nondet(77);
if (tmp_2_unfold_24_unfold_38 > 10) i_unfold_63 = 10;
else i_unfold_63 = 0;
Frama_C_show_each_i_(i_unfold_63);
tmp_3_unfold_24_unfold_38 = gen_nondet(79);
if (tmp_3_unfold_24_unfold_38) goto L_unfolding_10_loop;
tmp_4_unfold_24_unfold_38 = gen_nondet(80);
if (tmp_4_unfold_24_unfold_38) goto L0;
tmp_5_unfold_24_unfold_38 = gen_nondet(81);
if (tmp_5_unfold_24_unfold_38) goto L3;
}
i_unroll_63 ++;
unrolling_5_loop_unrolling_12_loop: ;
if (! (i_unroll_63 < 4)) goto unrolling_2_loop_unrolling_16_loop;
i_unfold_63 ++;
unfolding_5_loop_unfolding_12_loop: ;
if (! (i_unfold_63 < 4)) goto unfolding_2_loop_unfolding_16_loop;
{
int tmp_2_unroll_12_unroll_49;
int tmp_3_unroll_12_unroll_49;
int tmp_4_unroll_12_unroll_49;
int tmp_5_unroll_12_unroll_49;
L1_unrolling_4_loop_unrolling_13_loop:
j_unroll_63 = gen_nondet(76);
tmp_2_unroll_12_unroll_49 = gen_nondet(77);
if (tmp_2_unroll_12_unroll_49 > 10) i_unroll_63 = 10;
else i_unroll_63 = 0;
Frama_C_show_each_i_(i_unroll_63);
tmp_3_unroll_12_unroll_49 = gen_nondet(79);
if (tmp_3_unroll_12_unroll_49) goto L_unrolling_10_loop;
tmp_4_unroll_12_unroll_49 = gen_nondet(80);
if (tmp_4_unroll_12_unroll_49) goto L0;
tmp_5_unroll_12_unroll_49 = gen_nondet(81);
if (tmp_5_unroll_12_unroll_49) goto L3;
int tmp_2_unfold_12_unfold_49;
int tmp_3_unfold_12_unfold_49;
int tmp_4_unfold_12_unfold_49;
int tmp_5_unfold_12_unfold_49;
L1_unfolding_4_loop_unfolding_13_loop:
j_unfold_63 = gen_nondet(76);
tmp_2_unfold_12_unfold_49 = gen_nondet(77);
if (tmp_2_unfold_12_unfold_49 > 10) i_unfold_63 = 10;
else i_unfold_63 = 0;
Frama_C_show_each_i_(i_unfold_63);
tmp_3_unfold_12_unfold_49 = gen_nondet(79);
if (tmp_3_unfold_12_unfold_49) goto L_unfolding_10_loop;
tmp_4_unfold_12_unfold_49 = gen_nondet(80);
if (tmp_4_unfold_12_unfold_49) goto L0;
tmp_5_unfold_12_unfold_49 = gen_nondet(81);
if (tmp_5_unfold_12_unfold_49) goto L3;
}
i_unroll_63 ++;
unrolling_3_loop_unrolling_14_loop: ;
/*@ loop pragma UNROLL "done", 2; */
while (i_unroll_63 < 4) {
i_unfold_63 ++;
unfolding_3_loop_unfolding_14_loop: ;
/*@ loop unfold "done", 2; */
while (i_unfold_63 < 4) {
{
int tmp_2_unroll_60;
int tmp_3_unroll_60;
int tmp_4_unroll_60;
int tmp_5_unroll_60;
L1_unrolling_15_loop: j_unroll_63 = gen_nondet(76);
tmp_2_unroll_60 = gen_nondet(77);
if (tmp_2_unroll_60 > 10) i_unroll_63 = 10; else i_unroll_63 = 0;
Frama_C_show_each_i_(i_unroll_63);
tmp_3_unroll_60 = gen_nondet(79);
if (tmp_3_unroll_60) goto L_unrolling_10_loop;
tmp_4_unroll_60 = gen_nondet(80);
if (tmp_4_unroll_60) goto L0;
tmp_5_unroll_60 = gen_nondet(81);
if (tmp_5_unroll_60) goto L3;
int tmp_2_unfold_60;
int tmp_3_unfold_60;
int tmp_4_unfold_60;
int tmp_5_unfold_60;
L1_unfolding_15_loop: j_unfold_63 = gen_nondet(76);
tmp_2_unfold_60 = gen_nondet(77);
if (tmp_2_unfold_60 > 10) i_unfold_63 = 10; else i_unfold_63 = 0;
Frama_C_show_each_i_(i_unfold_63);
tmp_3_unfold_60 = gen_nondet(79);
if (tmp_3_unfold_60) goto L_unfolding_10_loop;
tmp_4_unfold_60 = gen_nondet(80);
if (tmp_4_unfold_60) goto L0;
tmp_5_unfold_60 = gen_nondet(81);
if (tmp_5_unfold_60) goto L3;
}
i_unroll_63 ++;
i_unfold_63 ++;
}
unrolling_2_loop_unrolling_16_loop: ;
unfolding_2_loop_unfolding_16_loop: ;
}
}
n --;
if (! (n > 0)) goto unrolling_8_loop;
unrolling_9_loop: ;
/*@ loop pragma UNROLL "done", 2; */
if (! (n > 0)) goto unfolding_8_loop;
unfolding_9_loop: ;
/*@ loop unfold "done", 2; */
while (1) {
{
int tmp_1;
......@@ -337,45 +337,45 @@ void main(void)
{
int j;
int i = 0;
if (! (i < 4)) goto unrolling_2_loop;
if (! (i < 4)) goto unfolding_2_loop;
{
int tmp_2_unroll_24;
int tmp_3_unroll_24;
int tmp_4_unroll_24;
int tmp_5_unroll_24;
L1_unrolling_6_loop: j = gen_nondet(76);
tmp_2_unroll_24 = gen_nondet(77);
if (tmp_2_unroll_24 > 10) i = 10; else i = 0;
int tmp_2_unfold_24;
int tmp_3_unfold_24;
int tmp_4_unfold_24;
int tmp_5_unfold_24;
L1_unfolding_6_loop: j = gen_nondet(76);
tmp_2_unfold_24 = gen_nondet(77);
if (tmp_2_unfold_24 > 10) i = 10; else i = 0;
Frama_C_show_each_i_(i);
tmp_3_unroll_24 = gen_nondet(79);
if (tmp_3_unroll_24) goto L;
tmp_4_unroll_24 = gen_nondet(80);
if (tmp_4_unroll_24) goto L0;
tmp_5_unroll_24 = gen_nondet(81);
if (tmp_5_unroll_24) goto L3;
tmp_3_unfold_24 = gen_nondet(79);
if (tmp_3_unfold_24) goto L;
tmp_4_unfold_24 = gen_nondet(80);
if (tmp_4_unfold_24) goto L0;
tmp_5_unfold_24 = gen_nondet(81);
if (tmp_5_unfold_24) goto L3;
}
i ++;
unrolling_5_loop: ;
if (! (i < 4)) goto unrolling_2_loop;
unfolding_5_loop: ;
if (! (i < 4)) goto unfolding_2_loop;
{
int tmp_2_unroll_12;
int tmp_3_unroll_12;
int tmp_4_unroll_12;
int tmp_5_unroll_12;
L1_unrolling_4_loop: j = gen_nondet(76);
tmp_2_unroll_12 = gen_nondet(77);
if (tmp_2_unroll_12 > 10) i = 10; else i = 0;
int tmp_2_unfold_12;
int tmp_3_unfold_12;
int tmp_4_unfold_12;
int tmp_5_unfold_12;
L1_unfolding_4_loop: j = gen_nondet(76);
tmp_2_unfold_12 = gen_nondet(77);
if (tmp_2_unfold_12 > 10) i = 10; else i = 0;
Frama_C_show_each_i_(i);
tmp_3_unroll_12 = gen_nondet(79);
if (tmp_3_unroll_12) goto L;
tmp_4_unroll_12 = gen_nondet(80);
if (tmp_4_unroll_12) goto L0;
tmp_5_unroll_12 = gen_nondet(81);
if (tmp_5_unroll_12) goto L3;
tmp_3_unfold_12 = gen_nondet(79);
if (tmp_3_unfold_12) goto L;
tmp_4_unfold_12 = gen_nondet(80);
if (tmp_4_unfold_12) goto L0;
tmp_5_unfold_12 = gen_nondet(81);
if (tmp_5_unfold_12) goto L3;
}
i ++;
unrolling_3_loop: ;
/*@ loop pragma UNROLL "done", 2; */
unfolding_3_loop: ;
/*@ loop unfold "done", 2; */
while (i < 4) {
{
int tmp_2;
......@@ -395,13 +395,13 @@ void main(void)
}
i ++;
}
unrolling_2_loop: ;
unfolding_2_loop: ;
}
}
n --;
if (! (n > 0)) break;
}
unrolling_8_loop: ;
unfolding_8_loop: ;
Frama_C_show_each_y_(y);
Frama_C_show_each_x_(x);
}
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment