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