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