-
Notifications
You must be signed in to change notification settings - Fork 62
Expand file tree
/
Copy pathdaikon.texinfo
More file actions
9406 lines (7706 loc) · 361 KB
/
Copy pathdaikon.texinfo
File metadata and controls
9406 lines (7706 loc) · 361 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
\input texinfo @c -*-texinfo-*-
@c %**start of header
@setfilename daikon.info
@settitle The Daikon Invariant Detector User Manual
@c %**end of header
@c To update all the nodes and menus all at once: C-u C-c C-u m
@c You shouldn't need to do that, though; makeinfo does it for you.
@c I can't get this to work, don't know why. MDE 4/2001.
@c @alias directory = file
@c Note about ``@table @option''.
@c Unfortunately, @option{} adds quotes in the Info and printed output
@c which is not necessary in a table. However, @t and @code compress any
@c two adjacent hyphens to one in Info and HTML output, which is even worse.
@c Problem: with texinfo 4.0, the HTML formatting leaves the "{}" after
@c uses of the macro. (Formatting seems fine for info, for printing, etc.)
@c So for now, I have inlined all instances of the macro. Yuck.
@c Another solution would be to use "makeinfo -E" (then process the
@c resulting file with "makeinfo --html").
@macro daikonemail{}
@email{daikon-developers@@googlegroups}
@end macro
@macro nospellcheck{text}
\text\
@end macro
@tex
\global\tableindent=.4in
@end tex
@c set overall document style
@c @setchapternewpage odd
@paragraphindent 1
@firstparagraphindent insert
@codequotebacktick on
@c default value for example indentation
@set exin 4
@c default value for example indentation within an @enumerate
@set exinenum 1
@exampleindent 4
@c Avoid black boxes marking overfull hboxes in TeX output.
@finalout
@c Start of Document
@titlepage
@sp 10
@c Could also use @title, @subtitle, @author here.
@center @titlefont{Daikon Invariant Detector User Manual}
@sp 2
@center Daikon version 5.6.7
@sp 1
@ifset final
@c FINAL version
@c Print out the Daikon version 5.6.7 release date
@center July 2, 2018
@end ifset
@ifclear final
@c DRAFT version
@center DRAFT Version @today{}
@end ifclear
@sp 5
@c reads daikon-logo.{eps,pdf} (not .txt, .png, or .jpg, because info
@c and HTML don't get the title page)
@image{images/daikon-logo,4in,}
@c The following two commands start the copyright page.
@page
@vskip 0pt plus 1filll
Copyright @copyright{} 1998-2014
@end titlepage
@c set document heading/footing style
@c The texinfo support for headings is too broken to use;
@c perhaps we could fix texinfo.tex some day.
@c @headings off
@c @evenheading @thispage @| @thischaptername @| Chapter @thischapternum
@c @oddheading Section @thissectionnum @| @thissectionname @| @thispage
@c @oddheading Chapter @thischapternum: @thischaptername @| @| @thispage
@c @evenheading @thispage @| @| Section @thissectionnum: @thissectionname
@ifclear final
@c DRAFT version
@everyfooting DRAFT @| @| @today{}
@end ifclear
@html
@image{images/daikon-logo}
@end html
@c Putting this lower in the HTML version looks a little bit strange,
@c but it's acceptable.
@ifnothtml
@contents
@end ifnothtml
@ifnottex
@node Top
@top Daikon Invariant Detector User Manual
This is the user manual for the Daikon invariant detector.
It describes Daikon version 5.6.7, released July 2, 2018.
@menu
* Introduction::
* Installing Daikon::
* Example usage::
* Running Daikon::
* Daikon output::
* Enhancing Daikon output::
* Front ends (instrumentation)::
* Tools::
* Troubleshooting::
* Details::
* General Index::
@c Putting end menu here is not how it's supposed to be done,
@c but it seems to fix the html toc indentation bug.
@end menu
@end ifnottex
@ifhtml
@contents
@end ifhtml
@node Introduction
@chapter Introduction
@c If you edit the introduction, then re-generate daikon.html and insert
@c its ``Introduction'' section into $DAIKONDIR/doc/www/index.html .
@uref{http://plse.cs.washington.edu/daikon/, ,Daikon} is an implementation of
dynamic detection of likely invariants; that is, the Daikon invariant
detector reports likely program invariants. An invariant is a property
that holds at a certain point or points in a program; these are often
seen in assert statements, documentation, and formal specifications.
Invariants can be useful in program understanding and a host of other
applications. Examples include @samp{x.field > abs(y)}; @samp{y = 2*x+3};
@samp{array a is sorted}; @samp{for all list objects lst, lst.next.prev =
lst}; @samp{for all treenode objects n, n.left.value < n.right.value}; @samp{p
!= null => p.content in myArray}; and many more. You can extend Daikon
to add new properties (@pxref{Enhancing Daikon output}, or
@pxref{New invariants,,,developer,Daikon Developer Manual}).
Dynamic invariant detection runs a program, observes the values that the
program computes, and then reports properties that were true over the
observed executions.
@c Daikon's output, which is sometimes called an ``operational abstraction'',
@c looks like a formal specification, or the contents of assert statements.
Daikon can detect properties in C, C++, C#, Eiffel, F#, Java, Perl, and
Visual Basic programs;
in spreadsheet files; and in other data sources. (Dynamic invariant
detection is a machine learning technique that can be applied to
arbitrary data.) It is easy to extend Daikon to other applications.
Daikon is freely available for download from
@uref{http://plse.cs.washington.edu/daikon/download/, ,download-site}. The distribution
includes both source code and
@uref{http://plse.cs.washington.edu/daikon/download/doc/, ,documentation},
and Daikon's license permits unrestricted use (@pxref{License}). Many
researchers and practitioners have used Daikon; those uses, and Daikon
itself, are described in various
@uref{http://plse.cs.washington.edu/daikon/pubs/, ,publications}.
For more information on Daikon,
@pxref{Top, , Introduction, developer, Daikon Developer Manual}.
For instance, the @cite{Daikon Developer Manual} indicates how to
extend Daikon with new invariants, new derived variables, and front
ends for new languages. It also contains information about the
implementation and about debugging flags.
@menu
* Mailing lists::
@end menu
@node Mailing lists
@section Mailing lists
@cindex mailing lists
@cindex daikon-announce mailing list
@cindex daikon-discuss mailing list
@cindex daikon-developers mailing list
The following mailing lists (and their archives) are available:
@table @samp
@item daikon-announce@@googlegroups.com
A low-volume, announcement-only list. For example,
announcements of new releases are sent to this list.
To subscribe, visit
@uref{https://groups.google.com/forum/#!forum/daikon-announce}.
@item daikon-discuss@@googlegroups.com
A moderated list for the community of Daikon users. Use it to share
tips and successes, and to get help with questions or problems (after
checking the documentation). To subscribe, visit
@uref{https://groups.google.com/forum/#!forum/daikon-discuss}.
@item daikon-developers@@googlegroups.com
This list goes to the Daikon maintainers. Use it for bug reports,
suggestions, and the like. If you are an active contributor to Daikon,
you may send mail to the list asking to be added.
@end table
Do @emph{not} send the same message to multiple mailing lists. Doing so is
antisocial: it causes confusion and extra work. If you do so, your
question will not be answered.
@node Installing Daikon
@chapter Installing Daikon
@cindex installing Daikon
Shortcut for the impatient: skip directly to the installation instructions
for @ref{Unix/Linux/MacOSX installation}, or @ref{Windows installation}.
The main way to install Daikon is from a release, as explained in this
section.
(Alternately,
@pxref{Version control repository,,,developer,Daikon Developer Manual},
to obtain the latest Daikon source code from its version control repository.)
Here is an overview of the steps.
@enumerate
@item
Download Daikon.
@item
Place three commands in your shell initialization file.
@item
Optionally, customize your installation.
@item
Compile Daikon and build other tools.
@end enumerate
Details appear below; select the
instructions for your operating system.
Differences from previous versions of Daikon appear
in the file @url{CHANGES,,@file{doc/CHANGES}} in the distribution.
To be notified of new releases, or to join discussions about Daikon,
subscribe to one of the mailing lists (@pxref{Mailing lists}).
@menu
* Requirements::
* Unix/Linux/MacOSX installation::
* Windows installation::
* Running Daikon under Windows::
@end menu
@node Requirements
@section Requirements for running Daikon
In order to run Daikon, you must have a Java 7 (or later) JDK, including a
@uref{http://www.oracle.com/technetwork/java/javase/overview/index.html,,
Java Virtual Machine} and a Java compiler.
If you wish to analyze C or C++ programs, you need a C or C++
compiler such as @command{gcc}.
If you wish to edit the Daikon source code and re-compile Daikon,
@pxref{Compiling Daikon,,,developer,Daikon Developer Manual}.
@c The explicit installation instructions, segregated by OS type, is
@c helpful to users.
@node Unix/Linux/MacOSX installation
@section Unix/Linux/MacOSX installation
@exampleindent 1
@enumerate
@item
Choose the directory where you want to install Daikon; we'll call this
the @var{daikonparent} directory. In this directory, download and
unpack Daikon.
@example
cd @var{daikonparent}
wget http://plse.cs.washington.edu/daikon/download/daikon-5.6.7.tar.gz
tar zxf daikon-5.6.7.tar.gz
@end example
@noindent
This creates a @file{@var{daikonparent}/daikon-5.6.7/} subdirectory.
@item
Place three commands in your shell initialization file:
set two environment variables
and source a Daikon startup file.
We will assume that you are using the bash shell or one of its variants.
Add commands like these to your @file{~/.bashrc} or @file{~/.bash_profile} file:
@example
# The absolute pathname of the directory that contains Daikon
export DAIKONDIR=@var{daikonparent}/daikon-5.6.7
# The absolute pathname of the directory that contains the Java JDK
export JAVA_HOME=@var{/usr/lib/jvm/java}
source $DAIKONDIR/scripts/daikon.bashrc
@end example
A setting of @env{JAVA_HOME} that @emph{sometimes} works (it might not
because @command{java} might be the version in the JDK or in the JRE) is:
@exampleindent 0
@smallexample
export JAVA_HOME=$@{JAVA_HOME:-$(dirname $(dirname $(dirname $(readlink -f $(/usr/bin/which java)))))@}
@end smallexample
@exampleindent 1
After editing your shell initialization file, either execute the commands
you placed in it, or else log out and log back in to achieve the same
effect.
@item
Optionally, customize other variables. The customizable variables are
listed in the Daikon startup file: @file{$DAIKONDIR/scripts/daikon.bashrc}.
You may customize them by setting environment variables, or by adding a
@file{Makefile.user} file to directory @file{$DAIKONDIR/java} (it is
automatically read at the beginning of the main Makefile, and prevents
you from having to edit the main Makefile directly).
@item
Compile Daikon and build other tools.
First, make sure that you have satisfied the requirements in
@ref{Requirements for compiling Daikon,,,developer,Daikon Developer Manual}
and
@ref{Requirements for compiling Kvasir,,,developer,Daikon Developer Manual}.
Then, run:
@c Note that this step is @emph{not} required if you only want to use Daikon
@c with its .NET front end (Celeriac).
@c This step is required for using
@c Daikon with its C/C++ front end (Kvasir), and for other tools such as DynComp.
@example
make -C $DAIKONDIR rebuild-everything
@end example
@noindent
This builds the various executables used by Daikon, such as the
C/C++ front end Kvasir (@pxref{Installing Kvasir}) and the
JDK for use with DynComp (@pxref{Instrumenting the JDK with DynComp}).
If you need more
information about compiling Daikon, see
@ref{Compiling Daikon,,,developer,Daikon Developer Manual}.
If you have trouble compiling the C/C++ front end Kvasir, see
@xref{Installing Kvasir}.
Note that running this make command may take 20 minutes or more,
depending on your computer.
Optionally, download other executables, such as
the Simplify theorem prover (@pxref{Installing Simplify}).
@end enumerate
@exampleindent 4
@node Windows installation
@section Windows installation
If you use Windows, an easy way to use Daikon is to run it under Windows
Subsystem for Linux (WSL).
The remainder of this section describes how to proceed if you prefer to use
Daikon under Windows.
To perform a complete install on
Windows, it is necessary to install the Cygwin toolset.
After you have installed Daikon, you can run it using either Cygwin or
the regular Windows shell (@pxref{Running Daikon under Windows}).
The Cygwin toolset (available at
@uref{http://cygwin.com/}) contains everything you need
to compile and run Linux programs under Windows. You can install Cygwin
by running the appropriate setup program; either
@uref{http://cygwin.com/setup-x86.exe} or
@uref{http://cygwin.com/setup-x86_64.exe},
as determined by your machine type.
The default installation of Cygwin is sufficient for installing Daikon.
@exampleindent 1
@enumerate
@item
Choose the directory where you want to install Daikon; we'll call this
the @var{daikonparent} directory. In this directory, download and
unpack Daikon. (Substitute the current version number for @file{#.#.#}.)
@example
cd @var{daikonparent}
wget http://plse.cs.washington.edu/daikon/download/daikon-5.6.7.tar.gz
tar zxf daikon-5.6.7.tar.gz
@end example
@noindent
This creates a @file{@var{daikonparent}/daikon-5.6.7/} subdirectory.
@item
Place three commands in your shell initialization file @file{~/.bashrc}:
set two environment variables
and source a Daikon startup file.
Do not use a Windows shell; use the Cygwin bash shell instead.
@example
# The full pathname of the directory that contains Daikon
export DAIKONDIR=@var{daikonparent}/daikon-5.6.7
# The full Linux pathname of the directory that contains the Java JDK
export JAVA_HOME=/cygdrive/c/Program Files/Java/jdk1.7.0_45
source $DAIKONDIR/scripts/daikon.bashrc
@end example
@noindent
Use the Cygwin/Linux path style (e.g., @code{/cygdrive/c/daikon}) rather than the
windows path style (@code{C:\daikon}).
Some users have reported problems when using pathnames
with spaces. You can avoid the problem by using the @command{ln} command to add a
symbolic link without spaces to @code{Program Files}.
@example
cd /cygdrive/c
ln -s "Program Files" program_files
@end example
@noindent
and then the JAVA_HOME line becomes:
@example
export JAVA_HOME=/cygdrive/c/program_files/Java/jdk1.7.0_45
@end example
@c You can also
@c set the environment variables in the registry (right-click My Computer,
@c and then click Properties; click the Advanced tab; click Environment
@c variables), but that only reduces the number of steps you have to do for
@c each shell from 3 (two variables plus running the @file{daikonenv.bat}
@c file) to 1 (running the @file{daikonenv.bat} file).
After editing your shell initialization file, either execute the commands
you placed in it, or else log out and log back in to achieve the same
effect.
@item
Optionally, customize other variables. The customizable variables are
listed in the Daikon startup file: @file{$DAIKONDIR/scripts/daikon.bashrc}.
You may customize them by setting environment variables, or by adding a
@file{Makefile.user} file to directory @file{$DAIKONDIR/java} (it is
automatically read at the beginning of the main Makefile, and prevents
you from having to edit the main Makefile directly).
The one variable you must customize is
to define the @env{OSTYPE} variable to be @samp{cygwin}.
@example
OSTYPE = cygwin
@end example
@item
Compile Daikon and build other tools.
@c Note that this step is @emph{not} required if you only want to use Daikon
@c with its .NET front end (Celeriac).
@c This step is required for using other tools such as DynComp.
@example
make -C $DAIKONDIR rebuild-everything
@end example
@noindent
This builds the various executables used by Daikon, such as the
JDK for use with DynComp (@pxref{Instrumenting the JDK with DynComp}).
If you need more
information about compiling Daikon, see
@ref{Compiling Daikon,,,developer,Daikon Developer Manual}.
If you have trouble compiling the C/C++ front end Kvasir, see
@xref{Installing Kvasir}. Note that
Kvasir does not work under Cygwin.
Note that running this make command may take 20 minutes or more,
depending on your computer.
On Windows, running @command{make} requires
that @uref{http://www.cygwin.com/,Cygwin} be installed.
Optionally, download other executables, such as
the Simplify theorem prover (@pxref{Installing Simplify}).
@end enumerate
@exampleindent 4
@node Running Daikon under Windows
@section Running Daikon under Windows
@cindex Windows
@cindex Microsoft Windows
After you have installed Daikon under Windows (@pxref{Windows
installation}), you can run it either using native Windows utilities, or
using the Cygwin environment --- it's your choice.
Daikon is a @strong{command-line application} (and so are its related
programs, such as Chicory). You should invoke them from a command shell
--- either a Windows command shell or a Cygwin command shell --- rather
than by double-clicking their icons. In any event, double-clicking
would not supply the proper arguments to the program.
First, a little background/review. Java on Linux separates its
@env{CLASSPATH} entries using the colon (@samp{:}) while Java on Windows
separates the entries with a semi-colon (@samp{;}). There is a good reason
for this; on Windows the colon would have been impractical as it is
used in file paths (@file{c:\}); on Linux the semi-colon is impractical,
as it is used to end a command line. The tricky bit is that Cygwin
provides a Linux like environment on top of Windows. So Cygwin mainly
wants colon separators but @command{java} is a Windows application, so it wants
semi-colons. Another point is that when a Cygwin shell starts up,
it copies the Windows environment into its Linux like environment with
no changes --- except for the @env{PATH} variable. This it converts
to Linux format (with colons) and adds "/usr/local/bin:/usr/bin:" to
the front. Hence, it is all set to run both Cygwin and existing
Windows applications.
@menu
* Windows command line::
* Cygwin shell::
@end menu
@node Windows command line
@subsection Windows command line
The first option is to run Daikon using native Windows utilities.
The is done in the normal fashion. However, getting the correct
value for @env{CLASSPATH} can be confusing. As noted above, it
must be
specified in Windows format (Windows paths and semicolon separators).
It must include either @file{$DAIKONDIR/daikon.jar} or
@file{$DAIKONDIR/java} (if you
have recompiled the Daikon source). A typical example for
@env{CLASSPATH} might be:
@exampleindent 1
@example
C:\cygwin64\home\user\invariants\daikon\daikon.jar;.;C:\Program Files
(x86)\QuickTime\QTSystem\QTJava.zip;C:\Program Files\Java\jdk1.7.0_45\
jre\lib\rt.jar;C:\Program Files\Java\jdk1.7.0_45\lib\tools.jar
@end example
@exampleindent 4
@noindent
With this done, one may enter: @command{java daikon.Daikon} in any
directory and Daikon should start up correctly.
@node Cygwin shell
@subsection Cygwin shell
@cindex Cygwin toolset
The second option for Windows (and the one we recommend) is to run
Daikon using the Cygwin toolset
(available at @uref{http://cygwin.com/}), which
contains everything you need to compile and run Linux programs under
Windows. You can install Cygwin by simply running one of the setup
programs (based on your machine type) found
at @uref{http://cygwin.com/}.
As noted above, when running any Java program (such as Daikon or Chicory),
the @env{CLASSPATH} must be specified in Windows format. Your initial
install of the Java JDK will have set the basics for the @env{CLASSPATH}.
When you installed Daikon, you were instructed to place into your
shell initialization file commands to set @env{JAVA_HOME}
and then @command{source $DAIKONDIR/scripts/daikon.bashrc}. This will
set @env{CLASSPATH} properly each time you start a Bash shell. The
result should be a value for @env{CLASSPATH} that looks something like:
@exampleindent 1
@example
C:\cygwin64\home\user\invariants\daikon\daikon.jar;.;C:\Program Files
(x86)\QuickTime\QTSystem\QTJava.zip;C:\Program Files\Java\jdk1.7.0_45\
jre\lib\rt.jar;C:\Program Files\Java\jdk1.7.0_45\lib\tools.jar
@end example
@exampleindent 4
If you wish to override @env{CLASSPATH} by using the @option{-classpath}
(or @option{-cp}) option, you need to remember that the result must be
in Windows format. This can get confusing because the Cygwin
bash interpreter is going to process the command line prior to handing it
off to @command{java}. Hence:
@exampleindent 1
@example
java -cp c:\cygwin64\home\user\invariants\daikon\daikon.jar daikon.Daikon
@end example
@exampleindent 4
@noindent
will fail as the backslash @samp{\} is processed by bash and removed. Any of
the following will work:
@tex
\global\hfuzz=35pt
@end tex
@exampleindent 1
@example
java -cp c:\\cygwin64\\home\\user\\invariants\\daikon\\daikon.jar daikon.Daikon
java -cp "c:\cygwin64\home\user\invariants\daikon\daikon.jar" daikon.Daikon
java -cp c:/cygwin64/home/user/invariants/daikon/daikon.jar daikon.Daikon
@end example
@exampleindent 4
@tex
\global\hfuzz=1pt
@end tex
The last is interesting as this is almost the same as on ``real'' Linux. Windows
accepts either forward (@samp{/}) or backward (@samp{\}) slashes as directory separators
in paths. There are similar command parsing issues with parenthesis and blanks.
These are legal in Windows paths, but will cause bash to get confused.
In general, enclosing a valid Windows path within double quotes (@samp{"})
is the preferred way to avoid these problems.
If you find it more convenient to use Linux paths, or want to use an
existing environment variable that contains a Linux path, the @command{cygpath} tool
will do the job. Thus, instead of:
@exampleindent 1
@example
java -cp $HOME/invariants/daikon/daikon.jar daikon.Daikon
@end example
@exampleindent 4
@noindent
(which will fail), use
@exampleindent 1
@example
java -cp `cygpath -wp $HOME/invariants/daikon/daikon.jar` daikon.Daikon
@end example
@exampleindent 4
@noindent
(note the back quotes @samp{`}) and everything should work as expected. Or even better:
@exampleindent 1
@example
java -cp "`cygpath -wp $HOME/invariants/daikon/daikon.jar`" daikon.Daikon
@end example
@exampleindent 4
@noindent
since there may be some Windows path characters contained in the environment variables.
@node Example usage
@chapter Example usage for Java, C/C++, C#/F#/Visual Basic, Perl, and Eiffel
Detecting invariants involves two steps:
@enumerate
@item
Obtain one or more data trace files by running your program under the control of a
front end (also known as an instrumenter or tracer) that records information about
variable values. You can run your program over one or more inputs of your own
choosing, such as regression tests or a typical user input session.
You may choose to obtain trace data for only part of
your program; this can avoid inundating you with
output, and can also improve performance.
@item
Run the Daikon invariant detector over the data trace files
(@pxref{Running Daikon}). This detects invariants in the recorded
information. You can view the invariants textually, or process them
with a variety of tools.
@end enumerate
This section briefly describes how to obtain data traces for Java, C,
C#, Perl, and Eiffel programs, and how to run Daikon. For detailed
information about these and other front ends that are available for
Daikon, @pxref{Front ends (instrumentation)}.
@menu
* Detecting invariants in Java programs::
* Detecting invariants in C/C++ programs::
* Detecting invariants in C# programs::
* Detecting invariants in Perl programs::
* Detecting invariants in Eiffel programs::
* Detecting invariants in Simulink/Stateflow programs::
@end menu
@node Detecting invariants in Java programs
@section Detecting invariants in Java programs
In order to detect invariants in a Java program, you will run the program
twice --- once using DynComp (@pxref{DynComp for Java}) to create a
@file{.decls} file and once using Chicory (@pxref{Chicory}) to create a
data trace file.
Then, run Daikon on the data trace file to detect invariants.
With the @option{--daikon} option to Chicory, a single command performs
the last two steps.
@exampleindent 1
For example, if you usually run
@example
java mypackage.MyClass arg1 arg2 arg3
@end example
@noindent
then instead you would run
@example
java daikon.DynComp mypackage.MyClass arg1 arg2 arg3
java daikon.Chicory --daikon \
--comparability-file=MyClass.decls-DynComp \
mypackage.MyClass arg1 arg2 arg3
@end example
@exampleindent 4
@noindent
and the Daikon output is written to the terminal.
@menu
* StackAr example::
* Detecting invariants when running a Java program from a jar file::
* Understanding the invariants::
* Second Java example::
@end menu
@c Commented out as of summer 2005, because David Cok doesn't seem likely
@c to pick this up again, and we don't want to lead users astray or
@c discourage them with non-functional software.
@c @node Eclipse plug-in
@c @subsection Eclipse plug-in
@c @cindex Eclipse plug-in
@c @cindex GUI, Eclipse
@c
@c Daikon is integrated with the
@c @uref{http://eclipse.org/, ,
@c Eclipse} IDE (Integrated Development Environment) for Java.
@c The Daikon plug-in provides a convenient way to instrument files,
@c obtain trace information, analyze those traces,
@c and create appropriately annotated Java source code.
@c For
@c details, see the @uref{daikonHelp.html, , Daikon Eclipse plug-in
@c documentation}.
@c
@c As of this writing (February 11, 2005), the plug-in only works with
@c Daikon 3 (for instance, version 3.1.7), not with Daikon 4. Support for
@c Daikon 4 is underway.
@c
@c For brief troubleshooting information, see @ref{Eclipse plug-in problems}.
@node StackAr example
@subsection StackAr example
The Daikon distribution contains some sample programs that will help
you get practice in running Daikon.
To detect invariants in the @file{StackAr} sample program, perform the
following steps after installing Daikon (@pxref{Installing Daikon}).
@exampleindent 1
@enumerate
@item
Compile the program with the @option{-g} switch to enable debugging
symbols. (The program and test suite appear in the
@file{DataStructures} subdirectory.)
@example
cd examples/java-examples/StackAr
javac -g DataStructures/*.java
@end example
@item
Run the program under the control of DynComp to generate comparability
information in the file @file{StackArTester.decls-DynComp}.
@example
java -cp .:$CLASSPATH daikon.DynComp DataStructures.StackArTester
@end example
@noindent
If you have not yet set the CLASSPATH, you may add it to the command
line for now --- but don't forget to set it later.
@exampleindent 0
@smallexample
java -cp "../../../daikon.jar:." daikon.DynComp DataStructures.StackArTester
@end smallexample
@exampleindent 1
@item
Run the program a second time, under the control of the Chicory front end.
Chicory observes the variable values and passes the information to Daikon.
Daikon infers invariants, prints them, and writes a binary representation
of them to file @file{StackArTester.inv.gz}.
@example
java -cp .:$CLASSPATH daikon.Chicory --daikon \
--comparability-file=StackArTester.decls-DynComp \
DataStructures.StackArTester
@end example
@noindent
Alternately, replacing the @option{--daikon} argument by
@option{--daikon-online} has the same effect, but does not write a data
trace file to disk.
@end enumerate
If you wish to have more control over the invariant detection process,
you can split the third step above into multiple steps. Then, step 3
would become:
@enumerate 3
@item
Run the program under the control of the Chicory front end
in order to create a trace file named
@file{StackArTester.dtrace.gz}.
@example
java -cp .:$CLASSPATH daikon.Chicory \
--comparability-file=StackArTester.decls-DynComp \
DataStructures.StackArTester
@end example
@item
Run Daikon on the trace file.
@example
java daikon.Daikon StackArTester.dtrace.gz
@end example
(Note the classpath (@option{-cp}) argument is not needed as we are not
running the @command{StackArTester} program.)
Daikon can analyze multiple runs (executions) of the program. You can
supply Daikon with multiple trace files:
@exampleindent 0
@smallexample
java daikon.Chicory --dtrace-file=StackArTester1.dtrace.gz \
--comparability-file=StackArTester.decls-DynComp DataStructures.StackArTester
java daikon.Chicory --dtrace-file=StackArTester2.dtrace.gz \
--comparability-file=StackArTester.decls-DynComp DataStructures.StackArTester
java daikon.Chicory --dtrace-file=StackArTester3.dtrace.gz \
--comparability-file=StackArTester.decls-DynComp DataStructures.StackArTester
java daikon.Daikon StackArTester*.dtrace.gz
@end smallexample
@exampleindent 1
@c @noindent
@c or, you can append information from multiple runs in a single trace file
@c (but in this case you cannot use a compressed trace file):
@c
@c @example
@c java -DDTRACEAPPEND=1 daikon.Chicory --dtrace-file=StackArTester.dtrace DataStructures.StackArTester
@c java -DDTRACEAPPEND=1 daikon.Chicory --dtrace-file=StackArTester.dtrace DataStructures.StackArTester
@c java -DDTRACEAPPEND=1 daikon.Chicory --dtrace-file=StackArTester.dtrace DataStructures.StackArTester
@c java daikon.Daikon StackArTester.dtrace
@c @end example
@noindent
(In this example, all the runs are identical, so multiple runs yield the
same invariants as one run.)
@item
Examine the invariants. (They were also printed to standard out
by the previous step.)
There are various ways to do this.
@itemize @bullet
@item
Examine the output from running Daikon. (You may find it
convenient to capture the output in a file; add @samp{> StackAr.txt}
to the end of the command that runs Daikon.)
@item
Use the @command{PrintInvariants} program to display the invariants.
@example
java daikon.PrintInvariants StackArTester.inv.gz
@end example
For more options to the @command{PrintInvariants} program, see @ref{Printing
invariants}.
@item
Use the Annotate program to insert the invariants as comments
into the Java source program.
@example
cd ..
java daikon.tools.jtb.Annotate StackArTester.inv.gz \
DataStructures/StackAr.java
@end example
(Here and elsewhere in the manual, the continuation character @samp{\} is
used to split a long command across lines. Windows uses the @samp{^}
character instead.)
Now examine file @file{DataStructures/StackAr.java-escannotated}.
For more information about the Annotate program, see @ref{Annotate}.
@end itemize
@end enumerate
@exampleindent 4
@node Detecting invariants when running a Java program from a jar file
@subsection Detecting invariants when running a Java program from a jar file
If your Java program is run directly from a @file{jar} file,
such as either of:
@exampleindent 1
@example
java mypackage.jar arguments
java -cp <originalclasspath> mypackage.jar arguments
@end example
@noindent
then to detect invariants in that Java program,
run these commands:
@example
java -cp mypackage.jar:<original classpath> daikon.DynComp <MyMain> arguments
java -cp mypackage.jar:<original classpath> daikon.Chicory --daikon \
--comparability-file=<MyMain>.decls-DynComp <MyMain> arguments
@end example
@noindent
where @command{<MyMain>} is the Main-class of the @file{jar} file, which you
can determine by running the command:
@example
unzip -p mypackage.jar META-INF/MANIFEST.MF | grep '^Main-Class:'
@end example
@exampleindent 4
@node Understanding the invariants
@subsection Understanding the invariants
This section examines some of the invariants for the @file{StackAr} example.
For more help interpreting invariants, see @ref{Interpreting output}.
The @file{StackAr} example is an array-based stack implementation. Take a
look at @file{DataStructures/StackAr.java} to get a sense of the
implementation. Now, look at the sixth section of Daikon output.
@exampleindent 1
@example
======================================================================
StackAr:::OBJECT
this.theArray != null
this.theArray.getClass().getName() == java.lang.Object[].class
this.topOfStack >= -1
this.topOfStack <= size(this.theArray[])-1
======================================================================
@end example
These four annotations describe the representation invariant. The
array is never null, and its runtime type is @code{Object[]}. The
@code{topOfStack} index is at least -1 and is less than the length
of the array.
Next, look at the invariants for the @code{top()} method.
@code{top()} has two different exit points, at lines 74 and 75
in the original source. There is a set of invariants for each exit
point, as well as a set of invariants that hold for all exit points.
Look at the invariants when @code{top()} returns at line 75.
@example
======================================================================
StackAr.top():::EXIT75
return == this.theArray[this.topOfStack]
return == this.theArray[orig(this.topOfStack)]
return == orig(this.theArray[post(this.topOfStack)])
return == orig(this.theArray[this.topOfStack])
this.topOfStack >= 0
return != null
======================================================================
@end example
The return value is never null, and is equal to the array element at
index @code{topOfStack}. The top of the stack is at least 0.
@exampleindent 4
@node Second Java example
@subsection A second Java example