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