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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
|
/*
* ott.c - a complicated example, multiple trace levels, logging
* to buffers and files and processes etc, etc.
*/
#include <stdlib.h>
#include <ott.h> /* a modified nana setup for this system */
/*
* initialise_ott - just opens the files or processes and creates any buffers
* we need for tracing and checking.
*/
L_BUFFER *_ott_fast; /* buffer for fast messages */
FILE *_ott_longterm; /* long term log */
FILE *_ott_plotting; /* a plotting process */
void initialise_ott() {
/* create a memory buffer for fast messages */
_ott_fast = L_buffer_create(80*2);
/* a long term log is kept for for slower events */
_ott_longterm = fopen("ott.log", "w");
if(_ott_longterm == NULL) {
fprintf(stderr, "initialise_ott: failed cannot open log file\n");
exit(1);
}
setbuf(_ott_longterm,NULL); /* turn off buffering */
/* a separate process is created to plot some of the log messages */
/* (for now we just use cat -n to print them out) */
_ott_plotting = popen("cat -n", "w");
if(_ott_plotting == NULL) {
fprintf(stderr, "initialise_ott: failed cannot open plot process\n");
exit(1);
}
setbuf(_ott_plotting,NULL); /* turn off buffering */
}
void restart_system(const char *m, int l) {
printf("restart_system(%s, line %d) called: ignored\n", m, l);
}
void set_I_level(int n) {
_ott_I_level = n;
}
/*
* main() - the example calls.
*/
int x = 10;
void show_log(void), show_inv(void);
int main(int argc, char **argv) {
initialise_ott();
show_log();
show_inv();
return 0;
}
void show_log() {
/* Display a status message for the tester */
LTERM("System has started\n");
LTERM("And the world is fine %d\n", 13);
/* Put a couple of messages in the long term log and print them */
LLONG("one is %d\n", 1);
LLONG("two is %d\n", 2);
system("cat ott.log");
/* Put a lot of messages in the fast circular buffer and print them */
for(x = 0; x != 32*1024; x++) {
LFAST("x is %d\n", x);
}
L_buffer_dump(_ott_fast,stderr);
/* Put some messages to a process (cat -n -u) */
LPLOT("%d %d\n", 1, 2);
LPLOT("%d %d\n", 2, 7 );
}
void show_inv(void) {
int x = 10, y = 0;
printf("* Showing invariants\n");
I(x != y);
I(x == y); /* fails prints a messsge and continues */
I0(x != y); /* doesn't fail since its not enabled */
set_I_level(0); /* disable I1,I2 */
I1(x < y); /* no failure since its disabled */
I2(x < y); /* no failure since its disabled */
set_I_level(1); /* disable I2 */
I1(x <= y); /* failure since its enabled */
I2(x <= y); /* no failure since its disabled */
set_I_level(2); /* enable all checking */
I0(x < y); /* failure since its enabled */
I1(x < y); /* failure since its enabled */
I2(x < y); /* failure since its enabled */
}
|
