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