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