File: loop1.i

package info (click to toggle)
frama-c 20220511-manganese-5
  • links: PTS, VCS
  • area: main
  • in suites: sid
  • size: 66,492 kB
  • sloc: ml: 278,834; ansic: 47,093; sh: 4,823; makefile: 3,613; javascript: 2,436; python: 1,919; perl: 897; lisp: 293; xml: 62
file content (27 lines) | stat: -rw-r--r-- 427 bytes parent folder | download | duplicates (4) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
 
char U[100]={1, 2};
char NULL_GLOBAL_LOOSING_BITS_ONE_BY_ONE = 0;
void main1 () {
  int i;
  for(i=0;i<100; i++)
    {
      // these assertions are meaningless; used to test if Value does not crash
      /*@ assert i >= \at(i,LoopCurrent); */
      /*@ assert i >= \at(i,LoopEntry); */
      U[i]=7;
    }

}

void main2 () {
  int i;
  for(i=0;i<=100; i++)
    {
      U[i]=7;
    }

}

int main () {
  main1();
  main2();
}