1extern int __VERIFIER_nondet_int(void);
2
3
4
5#line 2 "libacc.c"
6struct JoinPoint {
7 void **(*fp)(struct JoinPoint * ) ;
8 void **args ;
9 int argsCount ;
10 char const **argsType ;
11 void *(*arg)(int , struct JoinPoint * ) ;
12 char const *(*argType)(int , struct JoinPoint * ) ;
13 void **retValue ;
14 char const *retType ;
15 char const *funcName ;
16 char const *targetName ;
17 char const *fileName ;
18 char const *kind ;
19 void *excep_return ;
20};
21#line 18 "libacc.c"
22struct __UTAC__CFLOW_FUNC {
23 int (*func)(int , int ) ;
24 int val ;
25 struct __UTAC__CFLOW_FUNC *next ;
26};
27#line 18 "libacc.c"
28struct __UTAC__EXCEPTION {
29 void *jumpbuf ;
30 unsigned long long prtValue ;
31 int pops ;
32 struct __UTAC__CFLOW_FUNC *cflowfuncs ;
33};
34#line 211 "/usr/lib/gcc/x86_64-linux-gnu/4.4.5/include/stddef.h"
35typedef unsigned long size_t;
36#line 76 "libacc.c"
37struct __ACC__ERR {
38 void *v ;
39 struct __ACC__ERR *next ;
40};
41#line 1 "featureselect.o"
42#pragma merger(0,"featureselect.i","")
43#line 8 "featureselect.h"
44int __SELECTED_FEATURE_Base ;
45#line 11 "featureselect.h"
46int __SELECTED_FEATURE_Keys ;
47#line 14 "featureselect.h"
48int __SELECTED_FEATURE_Encrypt ;
49#line 17 "featureselect.h"
50int __SELECTED_FEATURE_AutoResponder ;
51#line 20 "featureselect.h"
52int __SELECTED_FEATURE_AddressBook ;
53#line 23 "featureselect.h"
54int __SELECTED_FEATURE_Sign ;
55#line 26 "featureselect.h"
56int __SELECTED_FEATURE_Forward ;
57#line 29 "featureselect.h"
58int __SELECTED_FEATURE_Verify ;
59#line 32 "featureselect.h"
60int __SELECTED_FEATURE_Decrypt ;
61#line 35 "featureselect.h"
62int __GUIDSL_ROOT_PRODUCTION ;
63#line 37 "featureselect.h"
64int __GUIDSL_NON_TERMINAL_main ;
65#line 41
66int select_one(void) ;
67#line 43
68void select_features(void) ;
69#line 45
70void select_helpers(void) ;
71#line 47
72int valid_product(void) ;
73#line 8 "featureselect.c"
74int select_one(void)
75{ int retValue_acc ;
76 int choice = __VERIFIER_nondet_int();
77
78 {
79#line 84 "featureselect.c"
80 retValue_acc = choice;
81#line 86
82 return (retValue_acc);
83#line 93
84 return (retValue_acc);
85}
86}
87#line 14 "featureselect.c"
88void select_features(void)
89{
90
91 {
92#line 115 "featureselect.c"
93 return;
94}
95}
96#line 20 "featureselect.c"
97void select_helpers(void)
98{
99
100 {
101#line 133 "featureselect.c"
102 return;
103}
104}
105#line 25 "featureselect.c"
106int valid_product(void)
107{ int retValue_acc ;
108
109 {
110#line 151 "featureselect.c"
111 retValue_acc = 1;
112#line 153
113 return (retValue_acc);
114#line 160
115 return (retValue_acc);
116}
117}
118#line 1 "libacc.o"
119#pragma merger(0,"libacc.i","")
120#line 73 "/usr/include/assert.h"
121extern __attribute__((__nothrow__, __noreturn__)) void __assert_fail(char const *__assertion ,
122 char const *__file ,
123 unsigned int __line ,
124 char const *__function ) ;
125#line 471 "/usr/include/stdlib.h"
126extern __attribute__((__nothrow__)) void *malloc(size_t __size ) __attribute__((__malloc__)) ;
127#line 488
128extern __attribute__((__nothrow__)) void free(void *__ptr ) ;
129#line 32 "libacc.c"
130void __utac__exception__cf_handler_set(void *exception , int (*cflow_func)(int ,
131 int ) ,
132 int val )
133{ struct __UTAC__EXCEPTION *excep ;
134 struct __UTAC__CFLOW_FUNC *cf ;
135 void *tmp ;
136 unsigned long __cil_tmp7 ;
137 unsigned long __cil_tmp8 ;
138 unsigned long __cil_tmp9 ;
139 unsigned long __cil_tmp10 ;
140 unsigned long __cil_tmp11 ;
141 unsigned long __cil_tmp12 ;
142 unsigned long __cil_tmp13 ;
143 unsigned long __cil_tmp14 ;
144 int (**mem_15)(int , int ) ;
145 int *mem_16 ;
146 struct __UTAC__CFLOW_FUNC **mem_17 ;
147 struct __UTAC__CFLOW_FUNC **mem_18 ;
148 struct __UTAC__CFLOW_FUNC **mem_19 ;
149
150 {
151 {
152#line 33
153 excep = (struct __UTAC__EXCEPTION *)exception;
154#line 34
155 tmp = malloc(24UL);
156#line 34
157 cf = (struct __UTAC__CFLOW_FUNC *)tmp;
158#line 36
159 mem_15 = (int (**)(int , int ))cf;
160#line 36
161 *mem_15 = cflow_func;
162#line 37
163 __cil_tmp7 = (unsigned long )cf;
164#line 37
165 __cil_tmp8 = __cil_tmp7 + 8;
166#line 37
167 mem_16 = (int *)__cil_tmp8;
168#line 37
169 *mem_16 = val;
170#line 38
171 __cil_tmp9 = (unsigned long )cf;
172#line 38
173 __cil_tmp10 = __cil_tmp9 + 16;
174#line 38
175 __cil_tmp11 = (unsigned long )excep;
176#line 38
177 __cil_tmp12 = __cil_tmp11 + 24;
178#line 38
179 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp10;
180#line 38
181 mem_18 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp12;
182#line 38
183 *mem_17 = *mem_18;
184#line 39
185 __cil_tmp13 = (unsigned long )excep;
186#line 39
187 __cil_tmp14 = __cil_tmp13 + 24;
188#line 39
189 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
190#line 39
191 *mem_19 = cf;
192 }
193#line 654 "libacc.c"
194 return;
195}
196}
197#line 44 "libacc.c"
198void __utac__exception__cf_handler_free(void *exception )
199{ struct __UTAC__EXCEPTION *excep ;
200 struct __UTAC__CFLOW_FUNC *cf ;
201 struct __UTAC__CFLOW_FUNC *tmp ;
202 unsigned long __cil_tmp5 ;
203 unsigned long __cil_tmp6 ;
204 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
205 unsigned long __cil_tmp8 ;
206 unsigned long __cil_tmp9 ;
207 unsigned long __cil_tmp10 ;
208 unsigned long __cil_tmp11 ;
209 void *__cil_tmp12 ;
210 unsigned long __cil_tmp13 ;
211 unsigned long __cil_tmp14 ;
212 struct __UTAC__CFLOW_FUNC **mem_15 ;
213 struct __UTAC__CFLOW_FUNC **mem_16 ;
214 struct __UTAC__CFLOW_FUNC **mem_17 ;
215
216 {
217#line 45
218 excep = (struct __UTAC__EXCEPTION *)exception;
219#line 46
220 __cil_tmp5 = (unsigned long )excep;
221#line 46
222 __cil_tmp6 = __cil_tmp5 + 24;
223#line 46
224 mem_15 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
225#line 46
226 cf = *mem_15;
227 {
228#line 49
229 while (1) {
230 while_0_continue: ;
231 {
232#line 49
233 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
234#line 49
235 __cil_tmp8 = (unsigned long )__cil_tmp7;
236#line 49
237 __cil_tmp9 = (unsigned long )cf;
238#line 49
239 if (__cil_tmp9 != __cil_tmp8) {
240
241 } else {
242 goto while_0_break;
243 }
244 }
245 {
246#line 50
247 tmp = cf;
248#line 51
249 __cil_tmp10 = (unsigned long )cf;
250#line 51
251 __cil_tmp11 = __cil_tmp10 + 16;
252#line 51
253 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp11;
254#line 51
255 cf = *mem_16;
256#line 52
257 __cil_tmp12 = (void *)tmp;
258#line 52
259 free(__cil_tmp12);
260 }
261 }
262 while_0_break: ;
263 }
264#line 55
265 __cil_tmp13 = (unsigned long )excep;
266#line 55
267 __cil_tmp14 = __cil_tmp13 + 24;
268#line 55
269 mem_17 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp14;
270#line 55
271 *mem_17 = (struct __UTAC__CFLOW_FUNC *)0;
272#line 694 "libacc.c"
273 return;
274}
275}
276#line 59 "libacc.c"
277void __utac__exception__cf_handler_reset(void *exception )
278{ struct __UTAC__EXCEPTION *excep ;
279 struct __UTAC__CFLOW_FUNC *cf ;
280 unsigned long __cil_tmp5 ;
281 unsigned long __cil_tmp6 ;
282 struct __UTAC__CFLOW_FUNC *__cil_tmp7 ;
283 unsigned long __cil_tmp8 ;
284 unsigned long __cil_tmp9 ;
285 int (*__cil_tmp10)(int , int ) ;
286 unsigned long __cil_tmp11 ;
287 unsigned long __cil_tmp12 ;
288 int __cil_tmp13 ;
289 unsigned long __cil_tmp14 ;
290 unsigned long __cil_tmp15 ;
291 struct __UTAC__CFLOW_FUNC **mem_16 ;
292 int (**mem_17)(int , int ) ;
293 int *mem_18 ;
294 struct __UTAC__CFLOW_FUNC **mem_19 ;
295
296 {
297#line 60
298 excep = (struct __UTAC__EXCEPTION *)exception;
299#line 61
300 __cil_tmp5 = (unsigned long )excep;
301#line 61
302 __cil_tmp6 = __cil_tmp5 + 24;
303#line 61
304 mem_16 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp6;
305#line 61
306 cf = *mem_16;
307 {
308#line 64
309 while (1) {
310 while_1_continue: ;
311 {
312#line 64
313 __cil_tmp7 = (struct __UTAC__CFLOW_FUNC *)0;
314#line 64
315 __cil_tmp8 = (unsigned long )__cil_tmp7;
316#line 64
317 __cil_tmp9 = (unsigned long )cf;
318#line 64
319 if (__cil_tmp9 != __cil_tmp8) {
320
321 } else {
322 goto while_1_break;
323 }
324 }
325 {
326#line 65
327 mem_17 = (int (**)(int , int ))cf;
328#line 65
329 __cil_tmp10 = *mem_17;
330#line 65
331 __cil_tmp11 = (unsigned long )cf;
332#line 65
333 __cil_tmp12 = __cil_tmp11 + 8;
334#line 65
335 mem_18 = (int *)__cil_tmp12;
336#line 65
337 __cil_tmp13 = *mem_18;
338#line 65
339 (*__cil_tmp10)(4, __cil_tmp13);
340#line 66
341 __cil_tmp14 = (unsigned long )cf;
342#line 66
343 __cil_tmp15 = __cil_tmp14 + 16;
344#line 66
345 mem_19 = (struct __UTAC__CFLOW_FUNC **)__cil_tmp15;
346#line 66
347 cf = *mem_19;
348 }
349 }
350 while_1_break: ;
351 }
352 {
353#line 69
354 __utac__exception__cf_handler_free(exception);
355 }
356#line 732 "libacc.c"
357 return;
358}
359}
360#line 80 "libacc.c"
361void *__utac__error_stack_mgt(void *env , int mode , int count ) ;
362#line 80 "libacc.c"
363static struct __ACC__ERR *head = (struct __ACC__ERR *)0;
364#line 79 "libacc.c"
365void *__utac__error_stack_mgt(void *env , int mode , int count )
366{ void *retValue_acc ;
367 struct __ACC__ERR *new ;
368 void *tmp ;
369 struct __ACC__ERR *temp ;
370 struct __ACC__ERR *next ;
371 void *excep ;
372 unsigned long __cil_tmp10 ;
373 unsigned long __cil_tmp11 ;
374 unsigned long __cil_tmp12 ;
375 unsigned long __cil_tmp13 ;
376 void *__cil_tmp14 ;
377 unsigned long __cil_tmp15 ;
378 unsigned long __cil_tmp16 ;
379 void *__cil_tmp17 ;
380 void **mem_18 ;
381 struct __ACC__ERR **mem_19 ;
382 struct __ACC__ERR **mem_20 ;
383 void **mem_21 ;
384 struct __ACC__ERR **mem_22 ;
385 void **mem_23 ;
386 void **mem_24 ;
387
388 {
389#line 82 "libacc.c"
390 if (count == 0) {
391#line 758 "libacc.c"
392 return (retValue_acc);
393 } else {
394
395 }
396#line 86 "libacc.c"
397 if (mode == 0) {
398 {
399#line 87
400 tmp = malloc(16UL);
401#line 87
402 new = (struct __ACC__ERR *)tmp;
403#line 88
404 mem_18 = (void **)new;
405#line 88
406 *mem_18 = env;
407#line 89
408 __cil_tmp10 = (unsigned long )new;
409#line 89
410 __cil_tmp11 = __cil_tmp10 + 8;
411#line 89
412 mem_19 = (struct __ACC__ERR **)__cil_tmp11;
413#line 89
414 *mem_19 = head;
415#line 90
416 head = new;
417#line 776 "libacc.c"
418 retValue_acc = (void *)new;
419 }
420#line 778
421 return (retValue_acc);
422 } else {
423
424 }
425#line 94 "libacc.c"
426 if (mode == 1) {
427#line 95
428 temp = head;
429 {
430#line 98
431 while (1) {
432 while_2_continue: ;
433#line 98
434 if (count > 1) {
435
436 } else {
437 goto while_2_break;
438 }
439 {
440#line 99
441 __cil_tmp12 = (unsigned long )temp;
442#line 99
443 __cil_tmp13 = __cil_tmp12 + 8;
444#line 99
445 mem_20 = (struct __ACC__ERR **)__cil_tmp13;
446#line 99
447 next = *mem_20;
448#line 100
449 mem_21 = (void **)temp;
450#line 100
451 excep = *mem_21;
452#line 101
453 __cil_tmp14 = (void *)temp;
454#line 101
455 free(__cil_tmp14);
456#line 102
457 __utac__exception__cf_handler_reset(excep);
458#line 103
459 temp = next;
460#line 104
461 count = count - 1;
462 }
463 }
464 while_2_break: ;
465 }
466 {
467#line 107
468 __cil_tmp15 = (unsigned long )temp;
469#line 107
470 __cil_tmp16 = __cil_tmp15 + 8;
471#line 107
472 mem_22 = (struct __ACC__ERR **)__cil_tmp16;
473#line 107
474 head = *mem_22;
475#line 108
476 mem_23 = (void **)temp;
477#line 108
478 excep = *mem_23;
479#line 109
480 __cil_tmp17 = (void *)temp;
481#line 109
482 free(__cil_tmp17);
483#line 110
484 __utac__exception__cf_handler_reset(excep);
485#line 820 "libacc.c"
486 retValue_acc = excep;
487 }
488#line 822
489 return (retValue_acc);
490 } else {
491
492 }
493#line 114
494 if (mode == 2) {
495#line 118 "libacc.c"
496 if (head) {
497#line 831
498 mem_24 = (void **)head;
499#line 831
500 retValue_acc = *mem_24;
501#line 833
502 return (retValue_acc);
503 } else {
504#line 837 "libacc.c"
505 retValue_acc = (void *)0;
506#line 839
507 return (retValue_acc);
508 }
509 } else {
510
511 }
512#line 846 "libacc.c"
513 return (retValue_acc);
514}
515}
516#line 122 "libacc.c"
517void *__utac__get_this_arg(int i , struct JoinPoint *this )
518{ void *retValue_acc ;
519 unsigned long __cil_tmp4 ;
520 unsigned long __cil_tmp5 ;
521 int __cil_tmp6 ;
522 int __cil_tmp7 ;
523 unsigned long __cil_tmp8 ;
524 unsigned long __cil_tmp9 ;
525 void **__cil_tmp10 ;
526 void **__cil_tmp11 ;
527 int *mem_12 ;
528 void ***mem_13 ;
529
530 {
531#line 123
532 if (i > 0) {
533 {
534#line 123
535 __cil_tmp4 = (unsigned long )this;
536#line 123
537 __cil_tmp5 = __cil_tmp4 + 16;
538#line 123
539 mem_12 = (int *)__cil_tmp5;
540#line 123
541 __cil_tmp6 = *mem_12;
542#line 123
543 if (i <= __cil_tmp6) {
544
545 } else {
546 {
547#line 123
548 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
549 123U, "__utac__get_this_arg");
550 }
551 }
552 }
553 } else {
554 {
555#line 123
556 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
557 123U, "__utac__get_this_arg");
558 }
559 }
560#line 870 "libacc.c"
561 __cil_tmp7 = i - 1;
562#line 870
563 __cil_tmp8 = (unsigned long )this;
564#line 870
565 __cil_tmp9 = __cil_tmp8 + 8;
566#line 870
567 mem_13 = (void ***)__cil_tmp9;
568#line 870
569 __cil_tmp10 = *mem_13;
570#line 870
571 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
572#line 870
573 retValue_acc = *__cil_tmp11;
574#line 872
575 return (retValue_acc);
576#line 879
577 return (retValue_acc);
578}
579}
580#line 129 "libacc.c"
581char const *__utac__get_this_argtype(int i , struct JoinPoint *this )
582{ char const *retValue_acc ;
583 unsigned long __cil_tmp4 ;
584 unsigned long __cil_tmp5 ;
585 int __cil_tmp6 ;
586 int __cil_tmp7 ;
587 unsigned long __cil_tmp8 ;
588 unsigned long __cil_tmp9 ;
589 char const **__cil_tmp10 ;
590 char const **__cil_tmp11 ;
591 int *mem_12 ;
592 char const ***mem_13 ;
593
594 {
595#line 131
596 if (i > 0) {
597 {
598#line 131
599 __cil_tmp4 = (unsigned long )this;
600#line 131
601 __cil_tmp5 = __cil_tmp4 + 16;
602#line 131
603 mem_12 = (int *)__cil_tmp5;
604#line 131
605 __cil_tmp6 = *mem_12;
606#line 131
607 if (i <= __cil_tmp6) {
608
609 } else {
610 {
611#line 131
612 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
613 131U, "__utac__get_this_argtype");
614 }
615 }
616 }
617 } else {
618 {
619#line 131
620 __assert_fail("i > 0 && i <= this->argsCount", "libacc.c",
621 131U, "__utac__get_this_argtype");
622 }
623 }
624#line 903 "libacc.c"
625 __cil_tmp7 = i - 1;
626#line 903
627 __cil_tmp8 = (unsigned long )this;
628#line 903
629 __cil_tmp9 = __cil_tmp8 + 24;
630#line 903
631 mem_13 = (char const ***)__cil_tmp9;
632#line 903
633 __cil_tmp10 = *mem_13;
634#line 903
635 __cil_tmp11 = __cil_tmp10 + __cil_tmp7;
636#line 903
637 retValue_acc = *__cil_tmp11;
638#line 905
639 return (retValue_acc);
640#line 912
641 return (retValue_acc);
642}
643}
644#line 1 "Util.o"
645#pragma merger(0,"Util.i","")
646#line 359 "/usr/include/stdio.h"
647extern int printf(char const * __restrict __format , ...) ;
648#line 1 "Util.h"
649int prompt(char *msg ) ;
650#line 9 "Util.c"
651int prompt(char *msg )
652{ int retValue_acc ;
653 int retval ;
654 char const * __restrict __cil_tmp4 ;
655
656 {
657 {
658#line 10
659 __cil_tmp4 = (char const * __restrict )"%s\n";
660#line 10
661 printf(__cil_tmp4, msg);
662#line 518 "Util.c"
663 retValue_acc = retval;
664 }
665#line 520
666 return (retValue_acc);
667#line 527
668 return (retValue_acc);
669}
670}
671#line 1 "wsllib_check.o"
672#pragma merger(0,"wsllib_check.i","")
673#line 3 "wsllib_check.c"
674void __automaton_fail(void)
675{
676
677 {
678 goto ERROR;
679 ERROR: ;
680#line 53 "wsllib_check.c"
681 return;
682}
683}
684#line 1 "ClientLib.o"
685#pragma merger(0,"ClientLib.i","")
686#line 4 "ClientLib.h"
687int initClient(void) ;
688#line 6
689char *getClientName(int handle ) ;
690#line 8
691void setClientName(int handle , char *value ) ;
692#line 10
693int getClientOutbuffer(int handle ) ;
694#line 12
695void setClientOutbuffer(int handle , int value ) ;
696#line 14
697int getClientAddressBookSize(int handle ) ;
698#line 16
699void setClientAddressBookSize(int handle , int value ) ;
700#line 18
701int createClientAddressBookEntry(int handle ) ;
702#line 20
703int getClientAddressBookAlias(int handle , int index ) ;
704#line 22
705void setClientAddressBookAlias(int handle , int index , int value ) ;
706#line 24
707int getClientAddressBookAddress(int handle , int index ) ;
708#line 26
709void setClientAddressBookAddress(int handle , int index , int value ) ;
710#line 29
711int getClientAutoResponse(int handle ) ;
712#line 31
713void setClientAutoResponse(int handle , int value ) ;
714#line 33
715int getClientPrivateKey(int handle ) ;
716#line 35
717void setClientPrivateKey(int handle , int value ) ;
718#line 37
719int getClientKeyringSize(int handle ) ;
720#line 39
721int createClientKeyringEntry(int handle ) ;
722#line 41
723int getClientKeyringUser(int handle , int index ) ;
724#line 43
725void setClientKeyringUser(int handle , int index , int value ) ;
726#line 45
727int getClientKeyringPublicKey(int handle , int index ) ;
728#line 47
729void setClientKeyringPublicKey(int handle , int index , int value ) ;
730#line 49
731int getClientForwardReceiver(int handle ) ;
732#line 51
733void setClientForwardReceiver(int handle , int value ) ;
734#line 53
735int getClientId(int handle ) ;
736#line 55
737void setClientId(int handle , int value ) ;
738#line 57
739int findPublicKey(int handle , int userid ) ;
740#line 59
741int findClientAddressBookAlias(int handle , int userid ) ;
742#line 5 "ClientLib.c"
743int __ste_Client_counter = 0;
744#line 7 "ClientLib.c"
745int initClient(void)
746{ int retValue_acc ;
747
748 {
749#line 12 "ClientLib.c"
750 if (__ste_Client_counter < 3) {
751#line 684
752 __ste_Client_counter = __ste_Client_counter + 1;
753#line 684
754 retValue_acc = __ste_Client_counter;
755#line 686
756 return (retValue_acc);
757 } else {
758#line 692 "ClientLib.c"
759 retValue_acc = -1;
760#line 694
761 return (retValue_acc);
762 }
763#line 701 "ClientLib.c"
764 return (retValue_acc);
765}
766}
767#line 15 "ClientLib.c"
768char *__ste_client_name0 = (char *)0;
769#line 17 "ClientLib.c"
770char *__ste_client_name1 = (char *)0;
771#line 19 "ClientLib.c"
772char *__ste_client_name2 = (char *)0;
773#line 22 "ClientLib.c"
774char *getClientName(int handle )
775{ char *retValue_acc ;
776 void *__cil_tmp3 ;
777
778 {
779#line 31 "ClientLib.c"
780 if (handle == 1) {
781#line 732
782 retValue_acc = __ste_client_name0;
783#line 734
784 return (retValue_acc);
785 } else {
786#line 736
787 if (handle == 2) {
788#line 741
789 retValue_acc = __ste_client_name1;
790#line 743
791 return (retValue_acc);
792 } else {
793#line 745
794 if (handle == 3) {
795#line 750
796 retValue_acc = __ste_client_name2;
797#line 752
798 return (retValue_acc);
799 } else {
800#line 758 "ClientLib.c"
801 __cil_tmp3 = (void *)0;
802#line 758
803 retValue_acc = (char *)__cil_tmp3;
804#line 760
805 return (retValue_acc);
806 }
807 }
808 }
809#line 767 "ClientLib.c"
810 return (retValue_acc);
811}
812}
813#line 34 "ClientLib.c"
814void setClientName(int handle , char *value )
815{
816
817 {
818#line 42
819 if (handle == 1) {
820#line 36
821 __ste_client_name0 = value;
822 } else {
823#line 37
824 if (handle == 2) {
825#line 38
826 __ste_client_name1 = value;
827 } else {
828#line 39
829 if (handle == 3) {
830#line 40
831 __ste_client_name2 = value;
832 } else {
833
834 }
835 }
836 }
837#line 802 "ClientLib.c"
838 return;
839}
840}
841#line 44 "ClientLib.c"
842int __ste_client_outbuffer0 = 0;
843#line 46 "ClientLib.c"
844int __ste_client_outbuffer1 = 0;
845#line 48 "ClientLib.c"
846int __ste_client_outbuffer2 = 0;
847#line 50 "ClientLib.c"
848int __ste_client_outbuffer3 = 0;
849#line 53 "ClientLib.c"
850int getClientOutbuffer(int handle )
851{ int retValue_acc ;
852
853 {
854#line 62 "ClientLib.c"
855 if (handle == 1) {
856#line 831
857 retValue_acc = __ste_client_outbuffer0;
858#line 833
859 return (retValue_acc);
860 } else {
861#line 835
862 if (handle == 2) {
863#line 840
864 retValue_acc = __ste_client_outbuffer1;
865#line 842
866 return (retValue_acc);
867 } else {
868#line 844
869 if (handle == 3) {
870#line 849
871 retValue_acc = __ste_client_outbuffer2;
872#line 851
873 return (retValue_acc);
874 } else {
875#line 857 "ClientLib.c"
876 retValue_acc = 0;
877#line 859
878 return (retValue_acc);
879 }
880 }
881 }
882#line 866 "ClientLib.c"
883 return (retValue_acc);
884}
885}
886#line 65 "ClientLib.c"
887void setClientOutbuffer(int handle , int value )
888{
889
890 {
891#line 73
892 if (handle == 1) {
893#line 67
894 __ste_client_outbuffer0 = value;
895 } else {
896#line 68
897 if (handle == 2) {
898#line 69
899 __ste_client_outbuffer1 = value;
900 } else {
901#line 70
902 if (handle == 3) {
903#line 71
904 __ste_client_outbuffer2 = value;
905 } else {
906
907 }
908 }
909 }
910#line 901 "ClientLib.c"
911 return;
912}
913}
914#line 77 "ClientLib.c"
915int __ste_ClientAddressBook_size0 = 0;
916#line 79 "ClientLib.c"
917int __ste_ClientAddressBook_size1 = 0;
918#line 81 "ClientLib.c"
919int __ste_ClientAddressBook_size2 = 0;
920#line 84 "ClientLib.c"
921int getClientAddressBookSize(int handle )
922{ int retValue_acc ;
923
924 {
925#line 93 "ClientLib.c"
926 if (handle == 1) {
927#line 928
928 retValue_acc = __ste_ClientAddressBook_size0;
929#line 930
930 return (retValue_acc);
931 } else {
932#line 932
933 if (handle == 2) {
934#line 937
935 retValue_acc = __ste_ClientAddressBook_size1;
936#line 939
937 return (retValue_acc);
938 } else {
939#line 941
940 if (handle == 3) {
941#line 946
942 retValue_acc = __ste_ClientAddressBook_size2;
943#line 948
944 return (retValue_acc);
945 } else {
946#line 954 "ClientLib.c"
947 retValue_acc = 0;
948#line 956
949 return (retValue_acc);
950 }
951 }
952 }
953#line 963 "ClientLib.c"
954 return (retValue_acc);
955}
956}
957#line 96 "ClientLib.c"
958void setClientAddressBookSize(int handle , int value )
959{
960
961 {
962#line 104
963 if (handle == 1) {
964#line 98
965 __ste_ClientAddressBook_size0 = value;
966 } else {
967#line 99
968 if (handle == 2) {
969#line 100
970 __ste_ClientAddressBook_size1 = value;
971 } else {
972#line 101
973 if (handle == 3) {
974#line 102
975 __ste_ClientAddressBook_size2 = value;
976 } else {
977
978 }
979 }
980 }
981#line 998 "ClientLib.c"
982 return;
983}
984}
985#line 106 "ClientLib.c"
986int createClientAddressBookEntry(int handle )
987{ int retValue_acc ;
988 int size ;
989 int tmp ;
990 int __cil_tmp5 ;
991
992 {
993 {
994#line 107
995 tmp = getClientAddressBookSize(handle);
996#line 107
997 size = tmp;
998 }
999#line 108 "ClientLib.c"
1000 if (size < 3) {
1001 {
1002#line 109 "ClientLib.c"
1003 __cil_tmp5 = size + 1;
1004#line 109
1005 setClientAddressBookSize(handle, __cil_tmp5);
1006#line 1025 "ClientLib.c"
1007 retValue_acc = size + 1;
1008 }
1009#line 1027
1010 return (retValue_acc);
1011 } else {
1012#line 1031 "ClientLib.c"
1013 retValue_acc = -1;
1014#line 1033
1015 return (retValue_acc);
1016 }
1017#line 1040 "ClientLib.c"
1018 return (retValue_acc);
1019}
1020}
1021#line 115 "ClientLib.c"
1022int __ste_Client_AddressBook0_Alias0 = 0;
1023#line 117 "ClientLib.c"
1024int __ste_Client_AddressBook0_Alias1 = 0;
1025#line 119 "ClientLib.c"
1026int __ste_Client_AddressBook0_Alias2 = 0;
1027#line 121 "ClientLib.c"
1028int __ste_Client_AddressBook1_Alias0 = 0;
1029#line 123 "ClientLib.c"
1030int __ste_Client_AddressBook1_Alias1 = 0;
1031#line 125 "ClientLib.c"
1032int __ste_Client_AddressBook1_Alias2 = 0;
1033#line 127 "ClientLib.c"
1034int __ste_Client_AddressBook2_Alias0 = 0;
1035#line 129 "ClientLib.c"
1036int __ste_Client_AddressBook2_Alias1 = 0;
1037#line 131 "ClientLib.c"
1038int __ste_Client_AddressBook2_Alias2 = 0;
1039#line 134 "ClientLib.c"
1040int getClientAddressBookAlias(int handle , int index )
1041{ int retValue_acc ;
1042
1043 {
1044#line 167
1045 if (handle == 1) {
1046#line 144 "ClientLib.c"
1047 if (index == 0) {
1048#line 1086
1049 retValue_acc = __ste_Client_AddressBook0_Alias0;
1050#line 1088
1051 return (retValue_acc);
1052 } else {
1053#line 1090
1054 if (index == 1) {
1055#line 1095
1056 retValue_acc = __ste_Client_AddressBook0_Alias1;
1057#line 1097
1058 return (retValue_acc);
1059 } else {
1060#line 1099
1061 if (index == 2) {
1062#line 1104
1063 retValue_acc = __ste_Client_AddressBook0_Alias2;
1064#line 1106
1065 return (retValue_acc);
1066 } else {
1067#line 1112
1068 retValue_acc = 0;
1069#line 1114
1070 return (retValue_acc);
1071 }
1072 }
1073 }
1074 } else {
1075#line 1116 "ClientLib.c"
1076 if (handle == 2) {
1077#line 154 "ClientLib.c"
1078 if (index == 0) {
1079#line 1124
1080 retValue_acc = __ste_Client_AddressBook1_Alias0;
1081#line 1126
1082 return (retValue_acc);
1083 } else {
1084#line 1128
1085 if (index == 1) {
1086#line 1133
1087 retValue_acc = __ste_Client_AddressBook1_Alias1;
1088#line 1135
1089 return (retValue_acc);
1090 } else {
1091#line 1137
1092 if (index == 2) {
1093#line 1142
1094 retValue_acc = __ste_Client_AddressBook1_Alias2;
1095#line 1144
1096 return (retValue_acc);
1097 } else {
1098#line 1150
1099 retValue_acc = 0;
1100#line 1152
1101 return (retValue_acc);
1102 }
1103 }
1104 }
1105 } else {
1106#line 1154 "ClientLib.c"
1107 if (handle == 3) {
1108#line 164 "ClientLib.c"
1109 if (index == 0) {
1110#line 1162
1111 retValue_acc = __ste_Client_AddressBook2_Alias0;
1112#line 1164
1113 return (retValue_acc);
1114 } else {
1115#line 1166
1116 if (index == 1) {
1117#line 1171
1118 retValue_acc = __ste_Client_AddressBook2_Alias1;
1119#line 1173
1120 return (retValue_acc);
1121 } else {
1122#line 1175
1123 if (index == 2) {
1124#line 1180
1125 retValue_acc = __ste_Client_AddressBook2_Alias2;
1126#line 1182
1127 return (retValue_acc);
1128 } else {
1129#line 1188
1130 retValue_acc = 0;
1131#line 1190
1132 return (retValue_acc);
1133 }
1134 }
1135 }
1136 } else {
1137#line 1196 "ClientLib.c"
1138 retValue_acc = 0;
1139#line 1198
1140 return (retValue_acc);
1141 }
1142 }
1143 }
1144#line 1205 "ClientLib.c"
1145 return (retValue_acc);
1146}
1147}
1148#line 171 "ClientLib.c"
1149int findClientAddressBookAlias(int handle , int userid )
1150{ int retValue_acc ;
1151
1152 {
1153#line 204
1154 if (handle == 1) {
1155#line 181 "ClientLib.c"
1156 if (userid == __ste_Client_AddressBook0_Alias0) {
1157#line 1233
1158 retValue_acc = 0;
1159#line 1235
1160 return (retValue_acc);
1161 } else {
1162#line 1237
1163 if (userid == __ste_Client_AddressBook0_Alias1) {
1164#line 1242
1165 retValue_acc = 1;
1166#line 1244
1167 return (retValue_acc);
1168 } else {
1169#line 1246
1170 if (userid == __ste_Client_AddressBook0_Alias2) {
1171#line 1251
1172 retValue_acc = 2;
1173#line 1253
1174 return (retValue_acc);
1175 } else {
1176#line 1259
1177 retValue_acc = -1;
1178#line 1261
1179 return (retValue_acc);
1180 }
1181 }
1182 }
1183 } else {
1184#line 1263 "ClientLib.c"
1185 if (handle == 2) {
1186#line 191 "ClientLib.c"
1187 if (userid == __ste_Client_AddressBook1_Alias0) {
1188#line 1271
1189 retValue_acc = 0;
1190#line 1273
1191 return (retValue_acc);
1192 } else {
1193#line 1275
1194 if (userid == __ste_Client_AddressBook1_Alias1) {
1195#line 1280
1196 retValue_acc = 1;
1197#line 1282
1198 return (retValue_acc);
1199 } else {
1200#line 1284
1201 if (userid == __ste_Client_AddressBook1_Alias2) {
1202#line 1289
1203 retValue_acc = 2;
1204#line 1291
1205 return (retValue_acc);
1206 } else {
1207#line 1297
1208 retValue_acc = -1;
1209#line 1299
1210 return (retValue_acc);
1211 }
1212 }
1213 }
1214 } else {
1215#line 1301 "ClientLib.c"
1216 if (handle == 3) {
1217#line 201 "ClientLib.c"
1218 if (userid == __ste_Client_AddressBook2_Alias0) {
1219#line 1309
1220 retValue_acc = 0;
1221#line 1311
1222 return (retValue_acc);
1223 } else {
1224#line 1313
1225 if (userid == __ste_Client_AddressBook2_Alias1) {
1226#line 1318
1227 retValue_acc = 1;
1228#line 1320
1229 return (retValue_acc);
1230 } else {
1231#line 1322
1232 if (userid == __ste_Client_AddressBook2_Alias2) {
1233#line 1327
1234 retValue_acc = 2;
1235#line 1329
1236 return (retValue_acc);
1237 } else {
1238#line 1335
1239 retValue_acc = -1;
1240#line 1337
1241 return (retValue_acc);
1242 }
1243 }
1244 }
1245 } else {
1246#line 1343 "ClientLib.c"
1247 retValue_acc = -1;
1248#line 1345
1249 return (retValue_acc);
1250 }
1251 }
1252 }
1253#line 1352 "ClientLib.c"
1254 return (retValue_acc);
1255}
1256}
1257#line 208 "ClientLib.c"
1258void setClientAddressBookAlias(int handle , int index , int value )
1259{
1260
1261 {
1262#line 234
1263 if (handle == 1) {
1264#line 217
1265 if (index == 0) {
1266#line 211
1267 __ste_Client_AddressBook0_Alias0 = value;
1268 } else {
1269#line 212
1270 if (index == 1) {
1271#line 213
1272 __ste_Client_AddressBook0_Alias1 = value;
1273 } else {
1274#line 214
1275 if (index == 2) {
1276#line 215
1277 __ste_Client_AddressBook0_Alias2 = value;
1278 } else {
1279
1280 }
1281 }
1282 }
1283 } else {
1284#line 216
1285 if (handle == 2) {
1286#line 225
1287 if (index == 0) {
1288#line 219
1289 __ste_Client_AddressBook1_Alias0 = value;
1290 } else {
1291#line 220
1292 if (index == 1) {
1293#line 221
1294 __ste_Client_AddressBook1_Alias1 = value;
1295 } else {
1296#line 222
1297 if (index == 2) {
1298#line 223
1299 __ste_Client_AddressBook1_Alias2 = value;
1300 } else {
1301
1302 }
1303 }
1304 }
1305 } else {
1306#line 224
1307 if (handle == 3) {
1308#line 233
1309 if (index == 0) {
1310#line 227
1311 __ste_Client_AddressBook2_Alias0 = value;
1312 } else {
1313#line 228
1314 if (index == 1) {
1315#line 229
1316 __ste_Client_AddressBook2_Alias1 = value;
1317 } else {
1318#line 230
1319 if (index == 2) {
1320#line 231
1321 __ste_Client_AddressBook2_Alias2 = value;
1322 } else {
1323
1324 }
1325 }
1326 }
1327 } else {
1328
1329 }
1330 }
1331 }
1332#line 1420 "ClientLib.c"
1333 return;
1334}
1335}
1336#line 236 "ClientLib.c"
1337int __ste_Client_AddressBook0_Address0 = 0;
1338#line 238 "ClientLib.c"
1339int __ste_Client_AddressBook0_Address1 = 0;
1340#line 240 "ClientLib.c"
1341int __ste_Client_AddressBook0_Address2 = 0;
1342#line 242 "ClientLib.c"
1343int __ste_Client_AddressBook1_Address0 = 0;
1344#line 244 "ClientLib.c"
1345int __ste_Client_AddressBook1_Address1 = 0;
1346#line 246 "ClientLib.c"
1347int __ste_Client_AddressBook1_Address2 = 0;
1348#line 248 "ClientLib.c"
1349int __ste_Client_AddressBook2_Address0 = 0;
1350#line 250 "ClientLib.c"
1351int __ste_Client_AddressBook2_Address1 = 0;
1352#line 252 "ClientLib.c"
1353int __ste_Client_AddressBook2_Address2 = 0;
1354#line 255 "ClientLib.c"
1355int getClientAddressBookAddress(int handle , int index )
1356{ int retValue_acc ;
1357
1358 {
1359#line 288
1360 if (handle == 1) {
1361#line 265 "ClientLib.c"
1362 if (index == 0) {
1363#line 1462
1364 retValue_acc = __ste_Client_AddressBook0_Address0;
1365#line 1464
1366 return (retValue_acc);
1367 } else {
1368#line 1466
1369 if (index == 1) {
1370#line 1471
1371 retValue_acc = __ste_Client_AddressBook0_Address1;
1372#line 1473
1373 return (retValue_acc);
1374 } else {
1375#line 1475
1376 if (index == 2) {
1377#line 1480
1378 retValue_acc = __ste_Client_AddressBook0_Address2;
1379#line 1482
1380 return (retValue_acc);
1381 } else {
1382#line 1488
1383 retValue_acc = 0;
1384#line 1490
1385 return (retValue_acc);
1386 }
1387 }
1388 }
1389 } else {
1390#line 1492 "ClientLib.c"
1391 if (handle == 2) {
1392#line 275 "ClientLib.c"
1393 if (index == 0) {
1394#line 1500
1395 retValue_acc = __ste_Client_AddressBook1_Address0;
1396#line 1502
1397 return (retValue_acc);
1398 } else {
1399#line 1504
1400 if (index == 1) {
1401#line 1509
1402 retValue_acc = __ste_Client_AddressBook1_Address1;
1403#line 1511
1404 return (retValue_acc);
1405 } else {
1406#line 1513
1407 if (index == 2) {
1408#line 1518
1409 retValue_acc = __ste_Client_AddressBook1_Address2;
1410#line 1520
1411 return (retValue_acc);
1412 } else {
1413#line 1526
1414 retValue_acc = 0;
1415#line 1528
1416 return (retValue_acc);
1417 }
1418 }
1419 }
1420 } else {
1421#line 1530 "ClientLib.c"
1422 if (handle == 3) {
1423#line 285 "ClientLib.c"
1424 if (index == 0) {
1425#line 1538
1426 retValue_acc = __ste_Client_AddressBook2_Address0;
1427#line 1540
1428 return (retValue_acc);
1429 } else {
1430#line 1542
1431 if (index == 1) {
1432#line 1547
1433 retValue_acc = __ste_Client_AddressBook2_Address1;
1434#line 1549
1435 return (retValue_acc);
1436 } else {
1437#line 1551
1438 if (index == 2) {
1439#line 1556
1440 retValue_acc = __ste_Client_AddressBook2_Address2;
1441#line 1558
1442 return (retValue_acc);
1443 } else {
1444#line 1564
1445 retValue_acc = 0;
1446#line 1566
1447 return (retValue_acc);
1448 }
1449 }
1450 }
1451 } else {
1452#line 1572 "ClientLib.c"
1453 retValue_acc = 0;
1454#line 1574
1455 return (retValue_acc);
1456 }
1457 }
1458 }
1459#line 1581 "ClientLib.c"
1460 return (retValue_acc);
1461}
1462}
1463#line 291 "ClientLib.c"
1464void setClientAddressBookAddress(int handle , int index , int value )
1465{
1466
1467 {
1468#line 317
1469 if (handle == 1) {
1470#line 300
1471 if (index == 0) {
1472#line 294
1473 __ste_Client_AddressBook0_Address0 = value;
1474 } else {
1475#line 295
1476 if (index == 1) {
1477#line 296
1478 __ste_Client_AddressBook0_Address1 = value;
1479 } else {
1480#line 297
1481 if (index == 2) {
1482#line 298
1483 __ste_Client_AddressBook0_Address2 = value;
1484 } else {
1485
1486 }
1487 }
1488 }
1489 } else {
1490#line 299
1491 if (handle == 2) {
1492#line 308
1493 if (index == 0) {
1494#line 302
1495 __ste_Client_AddressBook1_Address0 = value;
1496 } else {
1497#line 303
1498 if (index == 1) {
1499#line 304
1500 __ste_Client_AddressBook1_Address1 = value;
1501 } else {
1502#line 305
1503 if (index == 2) {
1504#line 306
1505 __ste_Client_AddressBook1_Address2 = value;
1506 } else {
1507
1508 }
1509 }
1510 }
1511 } else {
1512#line 307
1513 if (handle == 3) {
1514#line 316
1515 if (index == 0) {
1516#line 310
1517 __ste_Client_AddressBook2_Address0 = value;
1518 } else {
1519#line 311
1520 if (index == 1) {
1521#line 312
1522 __ste_Client_AddressBook2_Address1 = value;
1523 } else {
1524#line 313
1525 if (index == 2) {
1526#line 314
1527 __ste_Client_AddressBook2_Address2 = value;
1528 } else {
1529
1530 }
1531 }
1532 }
1533 } else {
1534
1535 }
1536 }
1537 }
1538#line 1649 "ClientLib.c"
1539 return;
1540}
1541}
1542#line 319 "ClientLib.c"
1543int __ste_client_autoResponse0 = 0;
1544#line 321 "ClientLib.c"
1545int __ste_client_autoResponse1 = 0;
1546#line 323 "ClientLib.c"
1547int __ste_client_autoResponse2 = 0;
1548#line 326 "ClientLib.c"
1549int getClientAutoResponse(int handle )
1550{ int retValue_acc ;
1551
1552 {
1553#line 335 "ClientLib.c"
1554 if (handle == 1) {
1555#line 1676
1556 retValue_acc = __ste_client_autoResponse0;
1557#line 1678
1558 return (retValue_acc);
1559 } else {
1560#line 1680
1561 if (handle == 2) {
1562#line 1685
1563 retValue_acc = __ste_client_autoResponse1;
1564#line 1687
1565 return (retValue_acc);
1566 } else {
1567#line 1689
1568 if (handle == 3) {
1569#line 1694
1570 retValue_acc = __ste_client_autoResponse2;
1571#line 1696
1572 return (retValue_acc);
1573 } else {
1574#line 1702 "ClientLib.c"
1575 retValue_acc = -1;
1576#line 1704
1577 return (retValue_acc);
1578 }
1579 }
1580 }
1581#line 1711 "ClientLib.c"
1582 return (retValue_acc);
1583}
1584}
1585#line 338 "ClientLib.c"
1586void setClientAutoResponse(int handle , int value )
1587{
1588
1589 {
1590#line 346
1591 if (handle == 1) {
1592#line 340
1593 __ste_client_autoResponse0 = value;
1594 } else {
1595#line 341
1596 if (handle == 2) {
1597#line 342
1598 __ste_client_autoResponse1 = value;
1599 } else {
1600#line 343
1601 if (handle == 3) {
1602#line 344
1603 __ste_client_autoResponse2 = value;
1604 } else {
1605
1606 }
1607 }
1608 }
1609#line 1746 "ClientLib.c"
1610 return;
1611}
1612}
1613#line 348 "ClientLib.c"
1614int __ste_client_privateKey0 = 0;
1615#line 350 "ClientLib.c"
1616int __ste_client_privateKey1 = 0;
1617#line 352 "ClientLib.c"
1618int __ste_client_privateKey2 = 0;
1619#line 355 "ClientLib.c"
1620int getClientPrivateKey(int handle )
1621{ int retValue_acc ;
1622
1623 {
1624#line 364 "ClientLib.c"
1625 if (handle == 1) {
1626#line 1773
1627 retValue_acc = __ste_client_privateKey0;
1628#line 1775
1629 return (retValue_acc);
1630 } else {
1631#line 1777
1632 if (handle == 2) {
1633#line 1782
1634 retValue_acc = __ste_client_privateKey1;
1635#line 1784
1636 return (retValue_acc);
1637 } else {
1638#line 1786
1639 if (handle == 3) {
1640#line 1791
1641 retValue_acc = __ste_client_privateKey2;
1642#line 1793
1643 return (retValue_acc);
1644 } else {
1645#line 1799 "ClientLib.c"
1646 retValue_acc = 0;
1647#line 1801
1648 return (retValue_acc);
1649 }
1650 }
1651 }
1652#line 1808 "ClientLib.c"
1653 return (retValue_acc);
1654}
1655}
1656#line 367 "ClientLib.c"
1657void setClientPrivateKey(int handle , int value )
1658{
1659
1660 {
1661#line 375
1662 if (handle == 1) {
1663#line 369
1664 __ste_client_privateKey0 = value;
1665 } else {
1666#line 370
1667 if (handle == 2) {
1668#line 371
1669 __ste_client_privateKey1 = value;
1670 } else {
1671#line 372
1672 if (handle == 3) {
1673#line 373
1674 __ste_client_privateKey2 = value;
1675 } else {
1676
1677 }
1678 }
1679 }
1680#line 1843 "ClientLib.c"
1681 return;
1682}
1683}
1684#line 377 "ClientLib.c"
1685int __ste_ClientKeyring_size0 = 0;
1686#line 379 "ClientLib.c"
1687int __ste_ClientKeyring_size1 = 0;
1688#line 381 "ClientLib.c"
1689int __ste_ClientKeyring_size2 = 0;
1690#line 384 "ClientLib.c"
1691int getClientKeyringSize(int handle )
1692{ int retValue_acc ;
1693
1694 {
1695#line 393 "ClientLib.c"
1696 if (handle == 1) {
1697#line 1870
1698 retValue_acc = __ste_ClientKeyring_size0;
1699#line 1872
1700 return (retValue_acc);
1701 } else {
1702#line 1874
1703 if (handle == 2) {
1704#line 1879
1705 retValue_acc = __ste_ClientKeyring_size1;
1706#line 1881
1707 return (retValue_acc);
1708 } else {
1709#line 1883
1710 if (handle == 3) {
1711#line 1888
1712 retValue_acc = __ste_ClientKeyring_size2;
1713#line 1890
1714 return (retValue_acc);
1715 } else {
1716#line 1896 "ClientLib.c"
1717 retValue_acc = 0;
1718#line 1898
1719 return (retValue_acc);
1720 }
1721 }
1722 }
1723#line 1905 "ClientLib.c"
1724 return (retValue_acc);
1725}
1726}
1727#line 396 "ClientLib.c"
1728void setClientKeyringSize(int handle , int value )
1729{
1730
1731 {
1732#line 404
1733 if (handle == 1) {
1734#line 398
1735 __ste_ClientKeyring_size0 = value;
1736 } else {
1737#line 399
1738 if (handle == 2) {
1739#line 400
1740 __ste_ClientKeyring_size1 = value;
1741 } else {
1742#line 401
1743 if (handle == 3) {
1744#line 402
1745 __ste_ClientKeyring_size2 = value;
1746 } else {
1747
1748 }
1749 }
1750 }
1751#line 1940 "ClientLib.c"
1752 return;
1753}
1754}
1755#line 406 "ClientLib.c"
1756int createClientKeyringEntry(int handle )
1757{ int retValue_acc ;
1758 int size ;
1759 int tmp ;
1760 int __cil_tmp5 ;
1761
1762 {
1763 {
1764#line 407
1765 tmp = getClientKeyringSize(handle);
1766#line 407
1767 size = tmp;
1768 }
1769#line 408 "ClientLib.c"
1770 if (size < 2) {
1771 {
1772#line 409 "ClientLib.c"
1773 __cil_tmp5 = size + 1;
1774#line 409
1775 setClientKeyringSize(handle, __cil_tmp5);
1776#line 1967 "ClientLib.c"
1777 retValue_acc = size + 1;
1778 }
1779#line 1969
1780 return (retValue_acc);
1781 } else {
1782#line 1973 "ClientLib.c"
1783 retValue_acc = -1;
1784#line 1975
1785 return (retValue_acc);
1786 }
1787#line 1982 "ClientLib.c"
1788 return (retValue_acc);
1789}
1790}
1791#line 414 "ClientLib.c"
1792int __ste_Client_Keyring0_User0 = 0;
1793#line 416 "ClientLib.c"
1794int __ste_Client_Keyring0_User1 = 0;
1795#line 418 "ClientLib.c"
1796int __ste_Client_Keyring0_User2 = 0;
1797#line 420 "ClientLib.c"
1798int __ste_Client_Keyring1_User0 = 0;
1799#line 422 "ClientLib.c"
1800int __ste_Client_Keyring1_User1 = 0;
1801#line 424 "ClientLib.c"
1802int __ste_Client_Keyring1_User2 = 0;
1803#line 426 "ClientLib.c"
1804int __ste_Client_Keyring2_User0 = 0;
1805#line 428 "ClientLib.c"
1806int __ste_Client_Keyring2_User1 = 0;
1807#line 430 "ClientLib.c"
1808int __ste_Client_Keyring2_User2 = 0;
1809#line 433 "ClientLib.c"
1810int getClientKeyringUser(int handle , int index )
1811{ int retValue_acc ;
1812
1813 {
1814#line 466
1815 if (handle == 1) {
1816#line 443 "ClientLib.c"
1817 if (index == 0) {
1818#line 2028
1819 retValue_acc = __ste_Client_Keyring0_User0;
1820#line 2030
1821 return (retValue_acc);
1822 } else {
1823#line 2032
1824 if (index == 1) {
1825#line 2037
1826 retValue_acc = __ste_Client_Keyring0_User1;
1827#line 2039
1828 return (retValue_acc);
1829 } else {
1830#line 2045
1831 retValue_acc = 0;
1832#line 2047
1833 return (retValue_acc);
1834 }
1835 }
1836 } else {
1837#line 2049 "ClientLib.c"
1838 if (handle == 2) {
1839#line 453 "ClientLib.c"
1840 if (index == 0) {
1841#line 2057
1842 retValue_acc = __ste_Client_Keyring1_User0;
1843#line 2059
1844 return (retValue_acc);
1845 } else {
1846#line 2061
1847 if (index == 1) {
1848#line 2066
1849 retValue_acc = __ste_Client_Keyring1_User1;
1850#line 2068
1851 return (retValue_acc);
1852 } else {
1853#line 2074
1854 retValue_acc = 0;
1855#line 2076
1856 return (retValue_acc);
1857 }
1858 }
1859 } else {
1860#line 2078 "ClientLib.c"
1861 if (handle == 3) {
1862#line 463 "ClientLib.c"
1863 if (index == 0) {
1864#line 2086
1865 retValue_acc = __ste_Client_Keyring2_User0;
1866#line 2088
1867 return (retValue_acc);
1868 } else {
1869#line 2090
1870 if (index == 1) {
1871#line 2095
1872 retValue_acc = __ste_Client_Keyring2_User1;
1873#line 2097
1874 return (retValue_acc);
1875 } else {
1876#line 2103
1877 retValue_acc = 0;
1878#line 2105
1879 return (retValue_acc);
1880 }
1881 }
1882 } else {
1883#line 2111 "ClientLib.c"
1884 retValue_acc = 0;
1885#line 2113
1886 return (retValue_acc);
1887 }
1888 }
1889 }
1890#line 2120 "ClientLib.c"
1891 return (retValue_acc);
1892}
1893}
1894#line 473 "ClientLib.c"
1895void setClientKeyringUser(int handle , int index , int value )
1896{
1897
1898 {
1899#line 499
1900 if (handle == 1) {
1901#line 482
1902 if (index == 0) {
1903#line 476
1904 __ste_Client_Keyring0_User0 = value;
1905 } else {
1906#line 477
1907 if (index == 1) {
1908#line 478
1909 __ste_Client_Keyring0_User1 = value;
1910 } else {
1911
1912 }
1913 }
1914 } else {
1915#line 479
1916 if (handle == 2) {
1917#line 490
1918 if (index == 0) {
1919#line 484
1920 __ste_Client_Keyring1_User0 = value;
1921 } else {
1922#line 485
1923 if (index == 1) {
1924#line 486
1925 __ste_Client_Keyring1_User1 = value;
1926 } else {
1927
1928 }
1929 }
1930 } else {
1931#line 487
1932 if (handle == 3) {
1933#line 498
1934 if (index == 0) {
1935#line 492
1936 __ste_Client_Keyring2_User0 = value;
1937 } else {
1938#line 493
1939 if (index == 1) {
1940#line 494
1941 __ste_Client_Keyring2_User1 = value;
1942 } else {
1943
1944 }
1945 }
1946 } else {
1947
1948 }
1949 }
1950 }
1951#line 2176 "ClientLib.c"
1952 return;
1953}
1954}
1955#line 501 "ClientLib.c"
1956int __ste_Client_Keyring0_PublicKey0 = 0;
1957#line 503 "ClientLib.c"
1958int __ste_Client_Keyring0_PublicKey1 = 0;
1959#line 505 "ClientLib.c"
1960int __ste_Client_Keyring0_PublicKey2 = 0;
1961#line 507 "ClientLib.c"
1962int __ste_Client_Keyring1_PublicKey0 = 0;
1963#line 509 "ClientLib.c"
1964int __ste_Client_Keyring1_PublicKey1 = 0;
1965#line 511 "ClientLib.c"
1966int __ste_Client_Keyring1_PublicKey2 = 0;
1967#line 513 "ClientLib.c"
1968int __ste_Client_Keyring2_PublicKey0 = 0;
1969#line 515 "ClientLib.c"
1970int __ste_Client_Keyring2_PublicKey1 = 0;
1971#line 517 "ClientLib.c"
1972int __ste_Client_Keyring2_PublicKey2 = 0;
1973#line 520 "ClientLib.c"
1974int getClientKeyringPublicKey(int handle , int index )
1975{ int retValue_acc ;
1976
1977 {
1978#line 553
1979 if (handle == 1) {
1980#line 530 "ClientLib.c"
1981 if (index == 0) {
1982#line 2218
1983 retValue_acc = __ste_Client_Keyring0_PublicKey0;
1984#line 2220
1985 return (retValue_acc);
1986 } else {
1987#line 2222
1988 if (index == 1) {
1989#line 2227
1990 retValue_acc = __ste_Client_Keyring0_PublicKey1;
1991#line 2229
1992 return (retValue_acc);
1993 } else {
1994#line 2235
1995 retValue_acc = 0;
1996#line 2237
1997 return (retValue_acc);
1998 }
1999 }
2000 } else {
2001#line 2239 "ClientLib.c"
2002 if (handle == 2) {
2003#line 540 "ClientLib.c"
2004 if (index == 0) {
2005#line 2247
2006 retValue_acc = __ste_Client_Keyring1_PublicKey0;
2007#line 2249
2008 return (retValue_acc);
2009 } else {
2010#line 2251
2011 if (index == 1) {
2012#line 2256
2013 retValue_acc = __ste_Client_Keyring1_PublicKey1;
2014#line 2258
2015 return (retValue_acc);
2016 } else {
2017#line 2264
2018 retValue_acc = 0;
2019#line 2266
2020 return (retValue_acc);
2021 }
2022 }
2023 } else {
2024#line 2268 "ClientLib.c"
2025 if (handle == 3) {
2026#line 550 "ClientLib.c"
2027 if (index == 0) {
2028#line 2276
2029 retValue_acc = __ste_Client_Keyring2_PublicKey0;
2030#line 2278
2031 return (retValue_acc);
2032 } else {
2033#line 2280
2034 if (index == 1) {
2035#line 2285
2036 retValue_acc = __ste_Client_Keyring2_PublicKey1;
2037#line 2287
2038 return (retValue_acc);
2039 } else {
2040#line 2293
2041 retValue_acc = 0;
2042#line 2295
2043 return (retValue_acc);
2044 }
2045 }
2046 } else {
2047#line 2301 "ClientLib.c"
2048 retValue_acc = 0;
2049#line 2303
2050 return (retValue_acc);
2051 }
2052 }
2053 }
2054#line 2310 "ClientLib.c"
2055 return (retValue_acc);
2056}
2057}
2058#line 557 "ClientLib.c"
2059int findPublicKey(int handle , int userid )
2060{ int retValue_acc ;
2061
2062 {
2063#line 591
2064 if (handle == 1) {
2065#line 568 "ClientLib.c"
2066 if (userid == __ste_Client_Keyring0_User0) {
2067#line 2338
2068 retValue_acc = __ste_Client_Keyring0_PublicKey0;
2069#line 2340
2070 return (retValue_acc);
2071 } else {
2072#line 2342
2073 if (userid == __ste_Client_Keyring0_User1) {
2074#line 2347
2075 retValue_acc = __ste_Client_Keyring0_PublicKey1;
2076#line 2349
2077 return (retValue_acc);
2078 } else {
2079#line 2355
2080 retValue_acc = 0;
2081#line 2357
2082 return (retValue_acc);
2083 }
2084 }
2085 } else {
2086#line 2359 "ClientLib.c"
2087 if (handle == 2) {
2088#line 578 "ClientLib.c"
2089 if (userid == __ste_Client_Keyring1_User0) {
2090#line 2367
2091 retValue_acc = __ste_Client_Keyring1_PublicKey0;
2092#line 2369
2093 return (retValue_acc);
2094 } else {
2095#line 2371
2096 if (userid == __ste_Client_Keyring1_User1) {
2097#line 2376
2098 retValue_acc = __ste_Client_Keyring1_PublicKey1;
2099#line 2378
2100 return (retValue_acc);
2101 } else {
2102#line 2384
2103 retValue_acc = 0;
2104#line 2386
2105 return (retValue_acc);
2106 }
2107 }
2108 } else {
2109#line 2388 "ClientLib.c"
2110 if (handle == 3) {
2111#line 588 "ClientLib.c"
2112 if (userid == __ste_Client_Keyring2_User0) {
2113#line 2396
2114 retValue_acc = __ste_Client_Keyring2_PublicKey0;
2115#line 2398
2116 return (retValue_acc);
2117 } else {
2118#line 2400
2119 if (userid == __ste_Client_Keyring2_User1) {
2120#line 2405
2121 retValue_acc = __ste_Client_Keyring2_PublicKey1;
2122#line 2407
2123 return (retValue_acc);
2124 } else {
2125#line 2413
2126 retValue_acc = 0;
2127#line 2415
2128 return (retValue_acc);
2129 }
2130 }
2131 } else {
2132#line 2421 "ClientLib.c"
2133 retValue_acc = 0;
2134#line 2423
2135 return (retValue_acc);
2136 }
2137 }
2138 }
2139#line 2430 "ClientLib.c"
2140 return (retValue_acc);
2141}
2142}
2143#line 595 "ClientLib.c"
2144void setClientKeyringPublicKey(int handle , int index , int value )
2145{
2146
2147 {
2148#line 621
2149 if (handle == 1) {
2150#line 604
2151 if (index == 0) {
2152#line 598
2153 __ste_Client_Keyring0_PublicKey0 = value;
2154 } else {
2155#line 599
2156 if (index == 1) {
2157#line 600
2158 __ste_Client_Keyring0_PublicKey1 = value;
2159 } else {
2160
2161 }
2162 }
2163 } else {
2164#line 601
2165 if (handle == 2) {
2166#line 612
2167 if (index == 0) {
2168#line 606
2169 __ste_Client_Keyring1_PublicKey0 = value;
2170 } else {
2171#line 607
2172 if (index == 1) {
2173#line 608
2174 __ste_Client_Keyring1_PublicKey1 = value;
2175 } else {
2176
2177 }
2178 }
2179 } else {
2180#line 609
2181 if (handle == 3) {
2182#line 620
2183 if (index == 0) {
2184#line 614
2185 __ste_Client_Keyring2_PublicKey0 = value;
2186 } else {
2187#line 615
2188 if (index == 1) {
2189#line 616
2190 __ste_Client_Keyring2_PublicKey1 = value;
2191 } else {
2192
2193 }
2194 }
2195 } else {
2196
2197 }
2198 }
2199 }
2200#line 2486 "ClientLib.c"
2201 return;
2202}
2203}
2204#line 623 "ClientLib.c"
2205int __ste_client_forwardReceiver0 = 0;
2206#line 625 "ClientLib.c"
2207int __ste_client_forwardReceiver1 = 0;
2208#line 627 "ClientLib.c"
2209int __ste_client_forwardReceiver2 = 0;
2210#line 629 "ClientLib.c"
2211int __ste_client_forwardReceiver3 = 0;
2212#line 631 "ClientLib.c"
2213int getClientForwardReceiver(int handle )
2214{ int retValue_acc ;
2215
2216 {
2217#line 640 "ClientLib.c"
2218 if (handle == 1) {
2219#line 2515
2220 retValue_acc = __ste_client_forwardReceiver0;
2221#line 2517
2222 return (retValue_acc);
2223 } else {
2224#line 2519
2225 if (handle == 2) {
2226#line 2524
2227 retValue_acc = __ste_client_forwardReceiver1;
2228#line 2526
2229 return (retValue_acc);
2230 } else {
2231#line 2528
2232 if (handle == 3) {
2233#line 2533
2234 retValue_acc = __ste_client_forwardReceiver2;
2235#line 2535
2236 return (retValue_acc);
2237 } else {
2238#line 2541 "ClientLib.c"
2239 retValue_acc = 0;
2240#line 2543
2241 return (retValue_acc);
2242 }
2243 }
2244 }
2245#line 2550 "ClientLib.c"
2246 return (retValue_acc);
2247}
2248}
2249#line 643 "ClientLib.c"
2250void setClientForwardReceiver(int handle , int value )
2251{
2252
2253 {
2254#line 651
2255 if (handle == 1) {
2256#line 645
2257 __ste_client_forwardReceiver0 = value;
2258 } else {
2259#line 646
2260 if (handle == 2) {
2261#line 647
2262 __ste_client_forwardReceiver1 = value;
2263 } else {
2264#line 648
2265 if (handle == 3) {
2266#line 649
2267 __ste_client_forwardReceiver2 = value;
2268 } else {
2269
2270 }
2271 }
2272 }
2273#line 2585 "ClientLib.c"
2274 return;
2275}
2276}
2277#line 653 "ClientLib.c"
2278int __ste_client_idCounter0 = 0;
2279#line 655 "ClientLib.c"
2280int __ste_client_idCounter1 = 0;
2281#line 657 "ClientLib.c"
2282int __ste_client_idCounter2 = 0;
2283#line 660 "ClientLib.c"
2284int getClientId(int handle )
2285{ int retValue_acc ;
2286
2287 {
2288#line 669 "ClientLib.c"
2289 if (handle == 1) {
2290#line 2612
2291 retValue_acc = __ste_client_idCounter0;
2292#line 2614
2293 return (retValue_acc);
2294 } else {
2295#line 2616
2296 if (handle == 2) {
2297#line 2621
2298 retValue_acc = __ste_client_idCounter1;
2299#line 2623
2300 return (retValue_acc);
2301 } else {
2302#line 2625
2303 if (handle == 3) {
2304#line 2630
2305 retValue_acc = __ste_client_idCounter2;
2306#line 2632
2307 return (retValue_acc);
2308 } else {
2309#line 2638 "ClientLib.c"
2310 retValue_acc = 0;
2311#line 2640
2312 return (retValue_acc);
2313 }
2314 }
2315 }
2316#line 2647 "ClientLib.c"
2317 return (retValue_acc);
2318}
2319}
2320#line 672 "ClientLib.c"
2321void setClientId(int handle , int value )
2322{
2323
2324 {
2325#line 680
2326 if (handle == 1) {
2327#line 674
2328 __ste_client_idCounter0 = value;
2329 } else {
2330#line 675
2331 if (handle == 2) {
2332#line 676
2333 __ste_client_idCounter1 = value;
2334 } else {
2335#line 677
2336 if (handle == 3) {
2337#line 678
2338 __ste_client_idCounter2 = value;
2339 } else {
2340
2341 }
2342 }
2343 }
2344#line 2682 "ClientLib.c"
2345 return;
2346}
2347}
2348#line 1 "Email.o"
2349#pragma merger(0,"Email.i","")
2350#line 6 "EmailLib.h"
2351int getEmailId(int handle ) ;
2352#line 10
2353int getEmailFrom(int handle ) ;
2354#line 12
2355void setEmailFrom(int handle , int value ) ;
2356#line 14
2357int getEmailTo(int handle ) ;
2358#line 16
2359void setEmailTo(int handle , int value ) ;
2360#line 6 "Email.h"
2361void printMail(int msg ) ;
2362#line 9
2363int isReadable(int msg ) ;
2364#line 12
2365int createEmail(int from , int to ) ;
2366#line 15
2367int cloneEmail(int msg ) ;
2368#line 9 "Email.c"
2369void printMail(int msg )
2370{ int tmp ;
2371 int tmp___0 ;
2372 int tmp___1 ;
2373 int tmp___2 ;
2374 char const * __restrict __cil_tmp6 ;
2375 char const * __restrict __cil_tmp7 ;
2376 char const * __restrict __cil_tmp8 ;
2377 char const * __restrict __cil_tmp9 ;
2378
2379 {
2380 {
2381#line 10
2382 tmp = getEmailId(msg);
2383#line 10
2384 __cil_tmp6 = (char const * __restrict )"ID:\n %i\n";
2385#line 10
2386 printf(__cil_tmp6, tmp);
2387#line 11
2388 tmp___0 = getEmailFrom(msg);
2389#line 11
2390 __cil_tmp7 = (char const * __restrict )"FROM:\n %i\n";
2391#line 11
2392 printf(__cil_tmp7, tmp___0);
2393#line 12
2394 tmp___1 = getEmailTo(msg);
2395#line 12
2396 __cil_tmp8 = (char const * __restrict )"TO:\n %i\n";
2397#line 12
2398 printf(__cil_tmp8, tmp___1);
2399#line 13
2400 tmp___2 = isReadable(msg);
2401#line 13
2402 __cil_tmp9 = (char const * __restrict )"IS_READABLE\n %i\n";
2403#line 13
2404 printf(__cil_tmp9, tmp___2);
2405 }
2406#line 601 "Email.c"
2407 return;
2408}
2409}
2410#line 19 "Email.c"
2411int isReadable(int msg )
2412{ int retValue_acc ;
2413
2414 {
2415#line 619 "Email.c"
2416 retValue_acc = 1;
2417#line 621
2418 return (retValue_acc);
2419#line 628
2420 return (retValue_acc);
2421}
2422}
2423#line 24 "Email.c"
2424int cloneEmail(int msg )
2425{ int retValue_acc ;
2426
2427 {
2428#line 650 "Email.c"
2429 retValue_acc = msg;
2430#line 652
2431 return (retValue_acc);
2432#line 659
2433 return (retValue_acc);
2434}
2435}
2436#line 29 "Email.c"
2437int createEmail(int from , int to )
2438{ int retValue_acc ;
2439 int msg ;
2440
2441 {
2442 {
2443#line 30
2444 msg = 1;
2445#line 31
2446 setEmailFrom(msg, from);
2447#line 32
2448 setEmailTo(msg, to);
2449#line 689 "Email.c"
2450 retValue_acc = msg;
2451 }
2452#line 691
2453 return (retValue_acc);
2454#line 698
2455 return (retValue_acc);
2456}
2457}
2458#line 1 "Client.o"
2459#pragma merger(0,"Client.i","")
2460#line 688 "/usr/include/stdio.h"
2461extern int puts(char const *__s ) ;
2462#line 14 "Client.h"
2463void queue(int client , int msg ) ;
2464#line 17
2465int is_queue_empty(void) ;
2466#line 19
2467int get_queued_client(void) ;
2468#line 21
2469int get_queued_email(void) ;
2470#line 24
2471void mail(int client , int msg ) ;
2472#line 26
2473void outgoing(int client , int msg ) ;
2474#line 28
2475void deliver(int client , int msg ) ;
2476#line 30
2477void incoming(int client , int msg ) ;
2478#line 32
2479int createClient(char *name ) ;
2480#line 35
2481void sendEmail(int sender , int receiver ) ;
2482#line 36
2483void autoRespond(int client , int msg ) ;
2484#line 37
2485void sendToAddressBook(int client , int msg ) ;
2486#line 39
2487void forward(int client , int msg ) ;
2488#line 6 "Client.c"
2489int queue_empty = 1;
2490#line 9 "Client.c"
2491int queued_message ;
2492#line 12 "Client.c"
2493int queued_client ;
2494#line 18 "Client.c"
2495void mail(int client , int msg )
2496{ int tmp ;
2497
2498 {
2499 {
2500#line 19
2501 puts("mail sent");
2502#line 20
2503 tmp = getEmailTo(msg);
2504#line 20
2505 incoming(tmp, msg);
2506 }
2507#line 731 "Client.c"
2508 return;
2509}
2510}
2511#line 27 "Client.c"
2512void outgoing__wrappee__AutoResponder(int client , int msg )
2513{ int tmp ;
2514
2515 {
2516 {
2517#line 28
2518 tmp = getClientId(client);
2519#line 28
2520 setEmailFrom(msg, tmp);
2521#line 29
2522 mail(client, msg);
2523 }
2524#line 753 "Client.c"
2525 return;
2526}
2527}
2528#line 36 "Client.c"
2529void outgoing(int client , int msg )
2530{ int size ;
2531 int tmp ;
2532 int receiver ;
2533 int tmp___0 ;
2534 int second ;
2535 int tmp___1 ;
2536 int tmp___2 ;
2537
2538 {
2539 {
2540#line 38
2541 tmp = getClientAddressBookSize(client);
2542#line 38
2543 size = tmp;
2544 }
2545#line 40
2546 if (size) {
2547 {
2548#line 41
2549 sendToAddressBook(client, msg);
2550#line 42
2551 puts("sending to alias in address book\n");
2552#line 43
2553 tmp___0 = getEmailTo(msg);
2554#line 43
2555 receiver = tmp___0;
2556#line 45
2557 puts("sending to second receipient\n");
2558#line 46
2559 tmp___1 = getClientAddressBookAddress(client, 1);
2560#line 46
2561 second = tmp___1;
2562#line 47
2563 setEmailTo(msg, second);
2564#line 48
2565 outgoing__wrappee__AutoResponder(client, msg);
2566#line 51
2567 tmp___2 = getClientAddressBookAddress(client, 0);
2568#line 51
2569 setEmailTo(msg, tmp___2);
2570#line 52
2571 outgoing__wrappee__AutoResponder(client, msg);
2572 }
2573 } else {
2574 {
2575#line 54
2576 outgoing__wrappee__AutoResponder(client, msg);
2577 }
2578 }
2579#line 803 "Client.c"
2580 return;
2581}
2582}
2583#line 63 "Client.c"
2584void deliver(int client , int msg )
2585{
2586
2587 {
2588 {
2589#line 64
2590 puts("mail delivered\n");
2591 }
2592#line 823 "Client.c"
2593 return;
2594}
2595}
2596#line 71 "Client.c"
2597void incoming__wrappee__Base(int client , int msg )
2598{
2599
2600 {
2601 {
2602#line 72
2603 deliver(client, msg);
2604 }
2605#line 843 "Client.c"
2606 return;
2607}
2608}
2609#line 78 "Client.c"
2610void incoming__wrappee__AddressBook(int client , int msg )
2611{ int tmp ;
2612
2613 {
2614 {
2615#line 79
2616 incoming__wrappee__Base(client, msg);
2617#line 80
2618 tmp = getClientAutoResponse(client);
2619 }
2620#line 80
2621 if (tmp) {
2622 {
2623#line 81
2624 autoRespond(client, msg);
2625 }
2626 } else {
2627
2628 }
2629#line 868 "Client.c"
2630 return;
2631}
2632}
2633#line 88 "Client.c"
2634void incoming(int client , int msg )
2635{ int fwreceiver ;
2636 int tmp ;
2637
2638 {
2639 {
2640#line 89
2641 incoming__wrappee__AddressBook(client, msg);
2642#line 90
2643 tmp = getClientForwardReceiver(client);
2644#line 90
2645 fwreceiver = tmp;
2646 }
2647#line 91
2648 if (fwreceiver) {
2649 {
2650#line 93
2651 setEmailTo(msg, fwreceiver);
2652#line 94
2653 forward(client, msg);
2654 }
2655 } else {
2656
2657 }
2658#line 899 "Client.c"
2659 return;
2660}
2661}
2662#line 100 "Client.c"
2663int createClient(char *name )
2664{ int retValue_acc ;
2665 int client ;
2666 int tmp ;
2667
2668 {
2669 {
2670#line 101
2671 tmp = initClient();
2672#line 101
2673 client = tmp;
2674#line 921 "Client.c"
2675 retValue_acc = client;
2676 }
2677#line 923
2678 return (retValue_acc);
2679#line 930
2680 return (retValue_acc);
2681}
2682}
2683#line 108 "Client.c"
2684void sendEmail(int sender , int receiver )
2685{ int email ;
2686 int tmp ;
2687
2688 {
2689 {
2690#line 109
2691 tmp = createEmail(0, receiver);
2692#line 109
2693 email = tmp;
2694#line 110
2695 outgoing(sender, email);
2696 }
2697#line 958 "Client.c"
2698 return;
2699}
2700}
2701#line 118 "Client.c"
2702void queue(int client , int msg )
2703{
2704
2705 {
2706#line 119
2707 queue_empty = 0;
2708#line 120
2709 queued_message = msg;
2710#line 121
2711 queued_client = client;
2712#line 982 "Client.c"
2713 return;
2714}
2715}
2716#line 127 "Client.c"
2717int is_queue_empty(void)
2718{ int retValue_acc ;
2719
2720 {
2721#line 1000 "Client.c"
2722 retValue_acc = queue_empty;
2723#line 1002
2724 return (retValue_acc);
2725#line 1009
2726 return (retValue_acc);
2727}
2728}
2729#line 134 "Client.c"
2730int get_queued_client(void)
2731{ int retValue_acc ;
2732
2733 {
2734#line 1031 "Client.c"
2735 retValue_acc = queued_client;
2736#line 1033
2737 return (retValue_acc);
2738#line 1040
2739 return (retValue_acc);
2740}
2741}
2742#line 141 "Client.c"
2743int get_queued_email(void)
2744{ int retValue_acc ;
2745
2746 {
2747#line 1062 "Client.c"
2748 retValue_acc = queued_message;
2749#line 1064
2750 return (retValue_acc);
2751#line 1071
2752 return (retValue_acc);
2753}
2754}
2755#line 148 "Client.c"
2756void autoRespond(int client , int msg )
2757{ int sender ;
2758 int tmp ;
2759
2760 {
2761 {
2762#line 149
2763 puts("sending autoresponse\n");
2764#line 150
2765 tmp = getEmailFrom(msg);
2766#line 150
2767 sender = tmp;
2768#line 151
2769 setEmailTo(msg, sender);
2770#line 152
2771 queue(client, msg);
2772 }
2773#line 1217 "Client.c"
2774 return;
2775}
2776}
2777#line 157 "Client.c"
2778void sendToAddressBook(int client , int msg )
2779{
2780
2781 {
2782#line 1235 "Client.c"
2783 return;
2784}
2785}
2786#line 1237
2787void __utac_acc__DecryptForward_spec__1(int msg ) ;
2788#line 163 "Client.c"
2789void forward(int client , int msg )
2790{ int __utac__ad__arg1 ;
2791
2792 {
2793 {
2794#line 1248 "Client.c"
2795 __utac__ad__arg1 = msg;
2796#line 1249
2797 __utac_acc__DecryptForward_spec__1(__utac__ad__arg1);
2798#line 164 "Client.c"
2799 puts("Forwarding message.\n");
2800#line 165
2801 printMail(msg);
2802#line 166
2803 queue(client, msg);
2804 }
2805#line 1268 "Client.c"
2806 return;
2807}
2808}
2809#line 1 "EmailLib.o"
2810#pragma merger(0,"EmailLib.i","")
2811#line 4 "EmailLib.h"
2812int initEmail(void) ;
2813#line 8
2814void setEmailId(int handle , int value ) ;
2815#line 18
2816char *getEmailSubject(int handle ) ;
2817#line 20
2818void setEmailSubject(int handle , char *value ) ;
2819#line 22
2820char *getEmailBody(int handle ) ;
2821#line 24
2822void setEmailBody(int handle , char *value ) ;
2823#line 26
2824int isEncrypted(int handle ) ;
2825#line 28
2826void setEmailIsEncrypted(int handle , int value ) ;
2827#line 30
2828int getEmailEncryptionKey(int handle ) ;
2829#line 32
2830void setEmailEncryptionKey(int handle , int value ) ;
2831#line 34
2832int isSigned(int handle ) ;
2833#line 36
2834void setEmailIsSigned(int handle , int value ) ;
2835#line 38
2836int getEmailSignKey(int handle ) ;
2837#line 40
2838void setEmailSignKey(int handle , int value ) ;
2839#line 42
2840int isVerified(int handle ) ;
2841#line 44
2842void setEmailIsSignatureVerified(int handle , int value ) ;
2843#line 5 "EmailLib.c"
2844int __ste_Email_counter = 0;
2845#line 7 "EmailLib.c"
2846int initEmail(void)
2847{ int retValue_acc ;
2848
2849 {
2850#line 12 "EmailLib.c"
2851 if (__ste_Email_counter < 2) {
2852#line 670
2853 __ste_Email_counter = __ste_Email_counter + 1;
2854#line 670
2855 retValue_acc = __ste_Email_counter;
2856#line 672
2857 return (retValue_acc);
2858 } else {
2859#line 678 "EmailLib.c"
2860 retValue_acc = -1;
2861#line 680
2862 return (retValue_acc);
2863 }
2864#line 687 "EmailLib.c"
2865 return (retValue_acc);
2866}
2867}
2868#line 15 "EmailLib.c"
2869int __ste_email_id0 = 0;
2870#line 17 "EmailLib.c"
2871int __ste_email_id1 = 0;
2872#line 19 "EmailLib.c"
2873int getEmailId(int handle )
2874{ int retValue_acc ;
2875
2876 {
2877#line 26 "EmailLib.c"
2878 if (handle == 1) {
2879#line 716
2880 retValue_acc = __ste_email_id0;
2881#line 718
2882 return (retValue_acc);
2883 } else {
2884#line 720
2885 if (handle == 2) {
2886#line 725
2887 retValue_acc = __ste_email_id1;
2888#line 727
2889 return (retValue_acc);
2890 } else {
2891#line 733 "EmailLib.c"
2892 retValue_acc = 0;
2893#line 735
2894 return (retValue_acc);
2895 }
2896 }
2897#line 742 "EmailLib.c"
2898 return (retValue_acc);
2899}
2900}
2901#line 29 "EmailLib.c"
2902void setEmailId(int handle , int value )
2903{
2904
2905 {
2906#line 35
2907 if (handle == 1) {
2908#line 31
2909 __ste_email_id0 = value;
2910 } else {
2911#line 32
2912 if (handle == 2) {
2913#line 33
2914 __ste_email_id1 = value;
2915 } else {
2916
2917 }
2918 }
2919#line 773 "EmailLib.c"
2920 return;
2921}
2922}
2923#line 37 "EmailLib.c"
2924int __ste_email_from0 = 0;
2925#line 39 "EmailLib.c"
2926int __ste_email_from1 = 0;
2927#line 41 "EmailLib.c"
2928int getEmailFrom(int handle )
2929{ int retValue_acc ;
2930
2931 {
2932#line 48 "EmailLib.c"
2933 if (handle == 1) {
2934#line 798
2935 retValue_acc = __ste_email_from0;
2936#line 800
2937 return (retValue_acc);
2938 } else {
2939#line 802
2940 if (handle == 2) {
2941#line 807
2942 retValue_acc = __ste_email_from1;
2943#line 809
2944 return (retValue_acc);
2945 } else {
2946#line 815 "EmailLib.c"
2947 retValue_acc = 0;
2948#line 817
2949 return (retValue_acc);
2950 }
2951 }
2952#line 824 "EmailLib.c"
2953 return (retValue_acc);
2954}
2955}
2956#line 51 "EmailLib.c"
2957void setEmailFrom(int handle , int value )
2958{
2959
2960 {
2961#line 57
2962 if (handle == 1) {
2963#line 53
2964 __ste_email_from0 = value;
2965 } else {
2966#line 54
2967 if (handle == 2) {
2968#line 55
2969 __ste_email_from1 = value;
2970 } else {
2971
2972 }
2973 }
2974#line 855 "EmailLib.c"
2975 return;
2976}
2977}
2978#line 59 "EmailLib.c"
2979int __ste_email_to0 = 0;
2980#line 61 "EmailLib.c"
2981int __ste_email_to1 = 0;
2982#line 63 "EmailLib.c"
2983int getEmailTo(int handle )
2984{ int retValue_acc ;
2985
2986 {
2987#line 70 "EmailLib.c"
2988 if (handle == 1) {
2989#line 880
2990 retValue_acc = __ste_email_to0;
2991#line 882
2992 return (retValue_acc);
2993 } else {
2994#line 884
2995 if (handle == 2) {
2996#line 889
2997 retValue_acc = __ste_email_to1;
2998#line 891
2999 return (retValue_acc);
3000 } else {
3001#line 897 "EmailLib.c"
3002 retValue_acc = 0;
3003#line 899
3004 return (retValue_acc);
3005 }
3006 }
3007#line 906 "EmailLib.c"
3008 return (retValue_acc);
3009}
3010}
3011#line 73 "EmailLib.c"
3012void setEmailTo(int handle , int value )
3013{
3014
3015 {
3016#line 79
3017 if (handle == 1) {
3018#line 75
3019 __ste_email_to0 = value;
3020 } else {
3021#line 76
3022 if (handle == 2) {
3023#line 77
3024 __ste_email_to1 = value;
3025 } else {
3026
3027 }
3028 }
3029#line 937 "EmailLib.c"
3030 return;
3031}
3032}
3033#line 81 "EmailLib.c"
3034char *__ste_email_subject0 ;
3035#line 83 "EmailLib.c"
3036char *__ste_email_subject1 ;
3037#line 85 "EmailLib.c"
3038char *getEmailSubject(int handle )
3039{ char *retValue_acc ;
3040 void *__cil_tmp3 ;
3041
3042 {
3043#line 92 "EmailLib.c"
3044 if (handle == 1) {
3045#line 962
3046 retValue_acc = __ste_email_subject0;
3047#line 964
3048 return (retValue_acc);
3049 } else {
3050#line 966
3051 if (handle == 2) {
3052#line 971
3053 retValue_acc = __ste_email_subject1;
3054#line 973
3055 return (retValue_acc);
3056 } else {
3057#line 979 "EmailLib.c"
3058 __cil_tmp3 = (void *)0;
3059#line 979
3060 retValue_acc = (char *)__cil_tmp3;
3061#line 981
3062 return (retValue_acc);
3063 }
3064 }
3065#line 988 "EmailLib.c"
3066 return (retValue_acc);
3067}
3068}
3069#line 95 "EmailLib.c"
3070void setEmailSubject(int handle , char *value )
3071{
3072
3073 {
3074#line 101
3075 if (handle == 1) {
3076#line 97
3077 __ste_email_subject0 = value;
3078 } else {
3079#line 98
3080 if (handle == 2) {
3081#line 99
3082 __ste_email_subject1 = value;
3083 } else {
3084
3085 }
3086 }
3087#line 1019 "EmailLib.c"
3088 return;
3089}
3090}
3091#line 103 "EmailLib.c"
3092char *__ste_email_body0 = (char *)0;
3093#line 105 "EmailLib.c"
3094char *__ste_email_body1 = (char *)0;
3095#line 107 "EmailLib.c"
3096char *getEmailBody(int handle )
3097{ char *retValue_acc ;
3098 void *__cil_tmp3 ;
3099
3100 {
3101#line 114 "EmailLib.c"
3102 if (handle == 1) {
3103#line 1044
3104 retValue_acc = __ste_email_body0;
3105#line 1046
3106 return (retValue_acc);
3107 } else {
3108#line 1048
3109 if (handle == 2) {
3110#line 1053
3111 retValue_acc = __ste_email_body1;
3112#line 1055
3113 return (retValue_acc);
3114 } else {
3115#line 1061 "EmailLib.c"
3116 __cil_tmp3 = (void *)0;
3117#line 1061
3118 retValue_acc = (char *)__cil_tmp3;
3119#line 1063
3120 return (retValue_acc);
3121 }
3122 }
3123#line 1070 "EmailLib.c"
3124 return (retValue_acc);
3125}
3126}
3127#line 117 "EmailLib.c"
3128void setEmailBody(int handle , char *value )
3129{
3130
3131 {
3132#line 123
3133 if (handle == 1) {
3134#line 119
3135 __ste_email_body0 = value;
3136 } else {
3137#line 120
3138 if (handle == 2) {
3139#line 121
3140 __ste_email_body1 = value;
3141 } else {
3142
3143 }
3144 }
3145#line 1101 "EmailLib.c"
3146 return;
3147}
3148}
3149#line 125 "EmailLib.c"
3150int __ste_email_isEncrypted0 = 0;
3151#line 127 "EmailLib.c"
3152int __ste_email_isEncrypted1 = 0;
3153#line 129 "EmailLib.c"
3154int isEncrypted(int handle )
3155{ int retValue_acc ;
3156
3157 {
3158#line 136 "EmailLib.c"
3159 if (handle == 1) {
3160#line 1126
3161 retValue_acc = __ste_email_isEncrypted0;
3162#line 1128
3163 return (retValue_acc);
3164 } else {
3165#line 1130
3166 if (handle == 2) {
3167#line 1135
3168 retValue_acc = __ste_email_isEncrypted1;
3169#line 1137
3170 return (retValue_acc);
3171 } else {
3172#line 1143 "EmailLib.c"
3173 retValue_acc = 0;
3174#line 1145
3175 return (retValue_acc);
3176 }
3177 }
3178#line 1152 "EmailLib.c"
3179 return (retValue_acc);
3180}
3181}
3182#line 139 "EmailLib.c"
3183void setEmailIsEncrypted(int handle , int value )
3184{
3185
3186 {
3187#line 145
3188 if (handle == 1) {
3189#line 141
3190 __ste_email_isEncrypted0 = value;
3191 } else {
3192#line 142
3193 if (handle == 2) {
3194#line 143
3195 __ste_email_isEncrypted1 = value;
3196 } else {
3197
3198 }
3199 }
3200#line 1183 "EmailLib.c"
3201 return;
3202}
3203}
3204#line 147 "EmailLib.c"
3205int __ste_email_encryptionKey0 = 0;
3206#line 149 "EmailLib.c"
3207int __ste_email_encryptionKey1 = 0;
3208#line 151 "EmailLib.c"
3209int getEmailEncryptionKey(int handle )
3210{ int retValue_acc ;
3211
3212 {
3213#line 158 "EmailLib.c"
3214 if (handle == 1) {
3215#line 1208
3216 retValue_acc = __ste_email_encryptionKey0;
3217#line 1210
3218 return (retValue_acc);
3219 } else {
3220#line 1212
3221 if (handle == 2) {
3222#line 1217
3223 retValue_acc = __ste_email_encryptionKey1;
3224#line 1219
3225 return (retValue_acc);
3226 } else {
3227#line 1225 "EmailLib.c"
3228 retValue_acc = 0;
3229#line 1227
3230 return (retValue_acc);
3231 }
3232 }
3233#line 1234 "EmailLib.c"
3234 return (retValue_acc);
3235}
3236}
3237#line 161 "EmailLib.c"
3238void setEmailEncryptionKey(int handle , int value )
3239{
3240
3241 {
3242#line 167
3243 if (handle == 1) {
3244#line 163
3245 __ste_email_encryptionKey0 = value;
3246 } else {
3247#line 164
3248 if (handle == 2) {
3249#line 165
3250 __ste_email_encryptionKey1 = value;
3251 } else {
3252
3253 }
3254 }
3255#line 1265 "EmailLib.c"
3256 return;
3257}
3258}
3259#line 169 "EmailLib.c"
3260int __ste_email_isSigned0 = 0;
3261#line 171 "EmailLib.c"
3262int __ste_email_isSigned1 = 0;
3263#line 173 "EmailLib.c"
3264int isSigned(int handle )
3265{ int retValue_acc ;
3266
3267 {
3268#line 180 "EmailLib.c"
3269 if (handle == 1) {
3270#line 1290
3271 retValue_acc = __ste_email_isSigned0;
3272#line 1292
3273 return (retValue_acc);
3274 } else {
3275#line 1294
3276 if (handle == 2) {
3277#line 1299
3278 retValue_acc = __ste_email_isSigned1;
3279#line 1301
3280 return (retValue_acc);
3281 } else {
3282#line 1307 "EmailLib.c"
3283 retValue_acc = 0;
3284#line 1309
3285 return (retValue_acc);
3286 }
3287 }
3288#line 1316 "EmailLib.c"
3289 return (retValue_acc);
3290}
3291}
3292#line 183 "EmailLib.c"
3293void setEmailIsSigned(int handle , int value )
3294{
3295
3296 {
3297#line 189
3298 if (handle == 1) {
3299#line 185
3300 __ste_email_isSigned0 = value;
3301 } else {
3302#line 186
3303 if (handle == 2) {
3304#line 187
3305 __ste_email_isSigned1 = value;
3306 } else {
3307
3308 }
3309 }
3310#line 1347 "EmailLib.c"
3311 return;
3312}
3313}
3314#line 191 "EmailLib.c"
3315int __ste_email_signKey0 = 0;
3316#line 193 "EmailLib.c"
3317int __ste_email_signKey1 = 0;
3318#line 195 "EmailLib.c"
3319int getEmailSignKey(int handle )
3320{ int retValue_acc ;
3321
3322 {
3323#line 202 "EmailLib.c"
3324 if (handle == 1) {
3325#line 1372
3326 retValue_acc = __ste_email_signKey0;
3327#line 1374
3328 return (retValue_acc);
3329 } else {
3330#line 1376
3331 if (handle == 2) {
3332#line 1381
3333 retValue_acc = __ste_email_signKey1;
3334#line 1383
3335 return (retValue_acc);
3336 } else {
3337#line 1389 "EmailLib.c"
3338 retValue_acc = 0;
3339#line 1391
3340 return (retValue_acc);
3341 }
3342 }
3343#line 1398 "EmailLib.c"
3344 return (retValue_acc);
3345}
3346}
3347#line 205 "EmailLib.c"
3348void setEmailSignKey(int handle , int value )
3349{
3350
3351 {
3352#line 211
3353 if (handle == 1) {
3354#line 207
3355 __ste_email_signKey0 = value;
3356 } else {
3357#line 208
3358 if (handle == 2) {
3359#line 209
3360 __ste_email_signKey1 = value;
3361 } else {
3362
3363 }
3364 }
3365#line 1429 "EmailLib.c"
3366 return;
3367}
3368}
3369#line 213 "EmailLib.c"
3370int __ste_email_isSignatureVerified0 ;
3371#line 215 "EmailLib.c"
3372int __ste_email_isSignatureVerified1 ;
3373#line 217 "EmailLib.c"
3374int isVerified(int handle )
3375{ int retValue_acc ;
3376
3377 {
3378#line 224 "EmailLib.c"
3379 if (handle == 1) {
3380#line 1454
3381 retValue_acc = __ste_email_isSignatureVerified0;
3382#line 1456
3383 return (retValue_acc);
3384 } else {
3385#line 1458
3386 if (handle == 2) {
3387#line 1463
3388 retValue_acc = __ste_email_isSignatureVerified1;
3389#line 1465
3390 return (retValue_acc);
3391 } else {
3392#line 1471 "EmailLib.c"
3393 retValue_acc = 0;
3394#line 1473
3395 return (retValue_acc);
3396 }
3397 }
3398#line 1480 "EmailLib.c"
3399 return (retValue_acc);
3400}
3401}
3402#line 227 "EmailLib.c"
3403void setEmailIsSignatureVerified(int handle , int value )
3404{
3405
3406 {
3407#line 233
3408 if (handle == 1) {
3409#line 229
3410 __ste_email_isSignatureVerified0 = value;
3411 } else {
3412#line 230
3413 if (handle == 2) {
3414#line 231
3415 __ste_email_isSignatureVerified1 = value;
3416 } else {
3417
3418 }
3419 }
3420#line 1511 "EmailLib.c"
3421 return;
3422}
3423}
3424#line 1 "DecryptForward_spec.o"
3425#pragma merger(0,"DecryptForward_spec.i","")
3426#line 11 "DecryptForward_spec.c"
3427void __utac_acc__DecryptForward_spec__1(int msg )
3428{ int tmp ;
3429
3430 {
3431 {
3432#line 13
3433 puts("before forward\n");
3434#line 14
3435 tmp = isReadable(msg);
3436 }
3437#line 14
3438 if (tmp) {
3439
3440 } else {
3441 {
3442#line 15
3443 __automaton_fail();
3444 }
3445 }
3446#line 15
3447 return;
3448}
3449}
3450#line 1 "scenario.o"
3451#pragma merger(0,"scenario.i","")
3452#line 20 "scenario.c"
3453void rjhSetAutoRespond(void) ;
3454#line 33
3455void rjhEnableForwarding(void) ;
3456#line 40
3457void bobSetAddressBook(void) ;
3458#line 48
3459#line 54
3460void bobToRjh(void) ;
3461#line 1 "scenario.c"
3462void test(void)
3463{ int op1 ;
3464 int op2 ;
3465 int op3 ;
3466 int op4 ;
3467 int op5 ;
3468 int op6 ;
3469 int op7 ;
3470 int op8 ;
3471 int op9 ;
3472 int op10 ;
3473 int op11 ;
3474 int splverifierCounter ;
3475 int tmp ;
3476 int tmp___0 ;
3477 int tmp___1 ;
3478 int tmp___2 ;
3479 int tmp___3 ;
3480 int tmp___4 ;
3481 int tmp___5 ;
3482 int tmp___6 ;
3483 int tmp___7 ;
3484 int tmp___8 ;
3485 int tmp___9 ;
3486
3487 {
3488#line 2
3489 op1 = 0;
3490#line 3
3491 op2 = 0;
3492#line 4
3493 op3 = 0;
3494#line 5
3495 op4 = 0;
3496#line 6
3497 op5 = 0;
3498#line 7
3499 op6 = 0;
3500#line 8
3501 op7 = 0;
3502#line 9
3503 op8 = 0;
3504#line 10
3505 op9 = 0;
3506#line 11
3507 op10 = 0;
3508#line 12
3509 op11 = 0;
3510#line 13
3511 splverifierCounter = 0;
3512 {
3513#line 14
3514 while (1) {
3515 while_3_continue: ;
3516#line 14
3517 if (splverifierCounter < 4) {
3518
3519 } else {
3520 goto while_3_break;
3521 }
3522#line 15
3523 splverifierCounter = splverifierCounter + 1;
3524#line 16
3525 if (! op1) {
3526 {
3527#line 16
3528 tmp___9 = __VERIFIER_nondet_int();
3529 }
3530#line 16
3531 if (tmp___9) {
3532#line 17
3533 op1 = 1;
3534 } else {
3535 goto _L___8;
3536 }
3537 } else {
3538 _L___8:
3539#line 18
3540 if (! op2) {
3541 {
3542#line 18
3543 tmp___8 = __VERIFIER_nondet_int();
3544 }
3545#line 18
3546 if (tmp___8) {
3547 {
3548#line 20
3549 rjhSetAutoRespond();
3550#line 21
3551 op2 = 1;
3552 }
3553 } else {
3554 goto _L___7;
3555 }
3556 } else {
3557 _L___7:
3558#line 22
3559 if (! op3) {
3560 {
3561#line 22
3562 tmp___7 = __VERIFIER_nondet_int();
3563 }
3564#line 22
3565 if (tmp___7) {
3566#line 24
3567 op3 = 1;
3568 } else {
3569 goto _L___6;
3570 }
3571 } else {
3572 _L___6:
3573#line 25
3574 if (! op4) {
3575 {
3576#line 25
3577 tmp___6 = __VERIFIER_nondet_int();
3578 }
3579#line 25
3580 if (tmp___6) {
3581#line 27
3582 op4 = 1;
3583 } else {
3584 goto _L___5;
3585 }
3586 } else {
3587 _L___5:
3588#line 28
3589 if (! op5) {
3590 {
3591#line 28
3592 tmp___5 = __VERIFIER_nondet_int();
3593 }
3594#line 28
3595 if (tmp___5) {
3596#line 30
3597 op5 = 1;
3598 } else {
3599 goto _L___4;
3600 }
3601 } else {
3602 _L___4:
3603#line 31
3604 if (! op6) {
3605 {
3606#line 31
3607 tmp___4 = __VERIFIER_nondet_int();
3608 }
3609#line 31
3610 if (tmp___4) {
3611 {
3612#line 33
3613 rjhEnableForwarding();
3614#line 34
3615 op6 = 1;
3616 }
3617 } else {
3618 goto _L___3;
3619 }
3620 } else {
3621 _L___3:
3622#line 35
3623 if (! op7) {
3624 {
3625#line 35
3626 tmp___3 = __VERIFIER_nondet_int();
3627 }
3628#line 35
3629 if (tmp___3) {
3630#line 37
3631 op7 = 1;
3632 } else {
3633 goto _L___2;
3634 }
3635 } else {
3636 _L___2:
3637#line 38
3638 if (! op8) {
3639 {
3640#line 38
3641 tmp___2 = __VERIFIER_nondet_int();
3642 }
3643#line 38
3644 if (tmp___2) {
3645 {
3646#line 40
3647 bobSetAddressBook();
3648#line 41
3649 op8 = 1;
3650 }
3651 } else {
3652 goto _L___1;
3653 }
3654 } else {
3655 _L___1:
3656#line 42
3657 if (! op9) {
3658 {
3659#line 42
3660 tmp___1 = __VERIFIER_nondet_int();
3661 }
3662#line 42
3663 if (tmp___1) {
3664#line 44
3665 op9 = 1;
3666 } else {
3667 goto _L___0;
3668 }
3669 } else {
3670 _L___0:
3671#line 45
3672 if (! op10) {
3673 {
3674#line 45
3675 tmp___0 = __VERIFIER_nondet_int();
3676 }
3677#line 45
3678 if (tmp___0) {
3679#line 47
3680 op10 = 1;
3681 } else {
3682 goto _L;
3683 }
3684 } else {
3685 _L:
3686#line 48
3687 if (! op11) {
3688 {
3689#line 48
3690 tmp = __VERIFIER_nondet_int();
3691 }
3692#line 48
3693 if (tmp) {
3694#line 50
3695 op11 = 1;
3696 } else {
3697 goto while_3_break;
3698 }
3699 } else {
3700 goto while_3_break;
3701 }
3702 }
3703 }
3704 }
3705 }
3706 }
3707 }
3708 }
3709 }
3710 }
3711 }
3712 }
3713 while_3_break: ;
3714 }
3715 {
3716#line 54
3717 bobToRjh();
3718 }
3719#line 155 "scenario.c"
3720 return;
3721}
3722}
3723#line 1 "Test.o"
3724#pragma merger(0,"Test.i","")
3725#line 2 "Test.h"
3726int bob ;
3727#line 5 "Test.h"
3728int rjh ;
3729#line 8 "Test.h"
3730int chuck ;
3731#line 11
3732void setup_bob(int bob___0 ) ;
3733#line 14
3734void setup_rjh(int rjh___0 ) ;
3735#line 17
3736void setup_chuck(int chuck___0 ) ;
3737#line 26
3738void rjhToBob(void) ;
3739#line 32
3740void setup(void) ;
3741#line 35
3742int main(void) ;
3743#line 18 "Test.c"
3744void setup_bob(int bob___0 )
3745{
3746
3747 {
3748 {
3749#line 19
3750 setClientId(bob___0, bob___0);
3751 }
3752#line 1312 "Test.c"
3753 return;
3754}
3755}
3756#line 26 "Test.c"
3757void setup_rjh(int rjh___0 )
3758{
3759
3760 {
3761 {
3762#line 27
3763 setClientId(rjh___0, rjh___0);
3764 }
3765#line 1332 "Test.c"
3766 return;
3767}
3768}
3769#line 33 "Test.c"
3770void setup_chuck(int chuck___0 )
3771{
3772
3773 {
3774 {
3775#line 34
3776 setClientId(chuck___0, chuck___0);
3777 }
3778#line 1352 "Test.c"
3779 return;
3780}
3781}
3782#line 44 "Test.c"
3783void bobToRjh(void)
3784{ int tmp ;
3785 int tmp___0 ;
3786 int tmp___1 ;
3787
3788 {
3789 {
3790#line 46
3791 puts("Please enter a subject and a message body.\n");
3792#line 47
3793 sendEmail(bob, rjh);
3794#line 48
3795 tmp___1 = is_queue_empty();
3796 }
3797#line 48
3798 if (tmp___1) {
3799
3800 } else {
3801 {
3802#line 49
3803 tmp = get_queued_email();
3804#line 49
3805 tmp___0 = get_queued_client();
3806#line 49
3807 outgoing(tmp___0, tmp);
3808 }
3809 }
3810#line 1379 "Test.c"
3811 return;
3812}
3813}
3814#line 56 "Test.c"
3815void rjhToBob(void)
3816{
3817
3818 {
3819 {
3820#line 58
3821 puts("Please enter a subject and a message body.\n");
3822#line 59
3823 sendEmail(rjh, bob);
3824 }
3825#line 1401 "Test.c"
3826 return;
3827}
3828}
3829#line 63 "Test.c"
3830#line 70 "Test.c"
3831void setup(void)
3832{ char const * __restrict __cil_tmp1 ;
3833 char const * __restrict __cil_tmp2 ;
3834 char const * __restrict __cil_tmp3 ;
3835
3836 {
3837 {
3838#line 71
3839 bob = 1;
3840#line 72
3841 setup_bob(bob);
3842#line 73
3843 __cil_tmp1 = (char const * __restrict )"bob: %d\n";
3844#line 73
3845 printf(__cil_tmp1, bob);
3846#line 75
3847 rjh = 2;
3848#line 76
3849 setup_rjh(rjh);
3850#line 77
3851 __cil_tmp2 = (char const * __restrict )"rjh: %d\n";
3852#line 77
3853 printf(__cil_tmp2, rjh);
3854#line 79
3855 chuck = 3;
3856#line 80
3857 setup_chuck(chuck);
3858#line 81
3859 __cil_tmp3 = (char const * __restrict )"chuck: %d\n";
3860#line 81
3861 printf(__cil_tmp3, chuck);
3862 }
3863#line 1472 "Test.c"
3864 return;
3865}
3866}
3867#line 87 "Test.c"
3868int main(void)
3869{ int retValue_acc ;
3870 int tmp ;
3871
3872 {
3873 {
3874#line 88
3875 select_helpers();
3876#line 89
3877 select_features();
3878#line 90
3879 tmp = valid_product();
3880 }
3881#line 90
3882 if (tmp) {
3883 {
3884#line 91
3885 setup();
3886#line 92
3887 test();
3888 }
3889 } else {
3890
3891 }
3892#line 1503 "Test.c"
3893 return (retValue_acc);
3894}
3895}
3896#line 100 "Test.c"
3897void rjhSetAutoRespond(void)
3898{
3899
3900 {
3901 {
3902#line 101
3903 setClientAutoResponse(rjh, 1);
3904 }
3905#line 1527 "Test.c"
3906 return;
3907}
3908}
3909#line 106 "Test.c"
3910void bobSetAddressBook(void)
3911{
3912
3913 {
3914 {
3915#line 107
3916 setClientAddressBookSize(bob, 1);
3917#line 108
3918 setClientAddressBookAlias(bob, 0, rjh);
3919#line 109
3920 setClientAddressBookAddress(bob, 0, rjh);
3921#line 110
3922 setClientAddressBookAddress(bob, 1, chuck);
3923 }
3924#line 1553 "Test.c"
3925 return;
3926}
3927}
3928#line 116 "Test.c"
3929void rjhEnableForwarding(void)
3930{
3931
3932 {
3933 {
3934#line 117
3935 setClientForwardReceiver(rjh, chuck);
3936 }
3937#line 1573 "Test.c"
3938 return;
3939}
3940}