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