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