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