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