File: ring_buffer2.c

package info (click to toggle)
cbmc 4.9-4
  • links: PTS
  • area: main
  • in suites: jessie, jessie-kfreebsd
  • size: 40,588 kB
  • ctags: 19,198
  • sloc: cpp: 185,860; ansic: 16,162; yacc: 5,343; lex: 4,518; makefile: 954; pascal: 506; sh: 318; perl: 213; java: 206
file content (33 lines) | stat: -rw-r--r-- 523 bytes parent folder | download | duplicates (3) 
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
28
29
30
31
32
33
 
#include <stdio.h>
#include <assert.h>
#include <stdlib.h>

#define MAX 1000
#define SIZE 10

unsigned int sample()
{
  return random()%(MAX+1);
}

unsigned int ring_buffer[SIZE];

int main()
{
  unsigned index=0, previous_index=SIZE-1;
  
  while(1)
  {
    unsigned output;
    output=(ring_buffer[index]+ring_buffer[previous_index])/2;
    assert(ring_buffer[index]<=MAX);
    assert(output<=MAX);
    
    ring_buffer[index]=sample();

    previous_index=index;
    index=(index+1)%SIZE;

    assert(index<SIZE);
  }
}