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