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