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