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