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