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