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