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