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