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