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