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