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