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