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