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