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