```
public final class Daikon
extends Object
```
The main(java.lang.String[]) method is the main entry point for the Daikon invariant detector. The mainHelper(java.lang.String[]) method is the entry point, when called programmatically.

Nested Class Summary

Nested Classes
Modifier and Type	Class	Description
`static class`	`Daikon.BugInDaikon`	Indicates that Daikon has terminated abnormally, indicating a bug in Daikon.
`static class`	`Daikon.DaikonTerminationException`	Indicates the need for Daikon to terminate.
`static class`	`Daikon.FileIOProgress`	Outputs FileIO progress information.
`static class`	`Daikon.FileOptions`
`static class`	`Daikon.NormalTermination`	Indicates that Daikon has terminated normally.
`static class`	`Daikon.ParseError`	A parser error that should be reported, with better context, by the caller.
`static class`	`Daikon.UserError`	Indicates a user error.

Field Summary

Fields
Modifier and Type	Field	Description
`static PptMap`	`all_ppts`	A PptMap (mapping from String to PptTopLevel) that contains all the program points.
`static boolean`	`check_program_types`
`static String`	`conf_limit_SWITCH`
`static String`	`config_option_SWITCH`
`static String`	`config_SWITCH`
`static @Nullable Invariant`	`current_inv`	current invariant (used for debugging)
`static String`	`debug_SWITCH`
`static String`	`debugAll_SWITCH`
`static Logger`	`debugEquality`
`static Logger`	`debugInit`	Debug tracer for ppt initialization.
`static Logger`	`debugProgress`
`static Logger`	`debugStats`	Prints out statistics concerning equality sets, suppressions, etc.
`static Logger`	`debugTrace`	Debug tracer.
`static String`	`disable_all_invariants_SWITCH`
`static boolean`	`disable_modbit_check_error`	Not a good idea to set this to true, as it is too easy to ignore the warnings and the modbit problem can cause an error later.
`static boolean`	`disable_modbit_check_message`
`static String`	`disc_reason_SWITCH`
`static boolean`	`dkconfig_calc_possible_invs`	Boolean.
`static @Interned String`	`dkconfig_guardNulls`	If "always", then invariants are always guarded.
`static boolean`	`dkconfig_output_conditionals`	Boolean.
`static int`	`dkconfig_ppt_perc`	Integer.
`static boolean`	`dkconfig_print_sample_totals`	Boolean.
`static int`	`dkconfig_progress_delay`	The amount of time to wait between updates of the progress display, measured in milliseconds.
`static int`	`dkconfig_progress_display_width`	The number of columns of progress information to display.
`static boolean`	`dkconfig_quiet`	Boolean.
`static boolean`	`dkconfig_undo_opts`	Boolean.
`static String`	`files_from_SWITCH`
`static String`	`format_SWITCH`	option format
`static String`	`help_SWITCH`	option help
`static boolean`	`ignore_comparability`
`static @Nullable File`	`inv_file`
`static boolean`	`invariants_check_canBeMissing`
`static boolean`	`invariants_check_canBeMissing_arrayelt`
`static boolean`	`isInferencing`	Whether Daikon is in its inferencing loop.
`static String`	`lineSep`
`static String`	`list_type_SWITCH`
`static String`	`mem_stat_SWITCH`
`static String`	`no_dataflow_hierarchy_SWITCH`
`static String`	`no_show_progress_SWITCH`	option no-show-progress
`static boolean`	`no_text_output`	When true, don't print textual output.
`static String`	`no_text_output_SWITCH`	option no-text-output
`static boolean`	`noversion_output`	Whether Daikon should print its version number and date.
`static String`	`noversion_SWITCH`	option noversion
`static boolean`	`omit_from_output`	When true, omit certain invariants from the output `.inv` file.
`static String`	`omit_from_output_SWITCH`
`static boolean[]`	`omit_types`	An array of flags, indexed by characters, in which a true entry means that invariants of that sort should be omitted from the output `.inv` file.
`static OutputFormat`	`output_format`
`static boolean`	`output_num_samples`
`static String`	`output_num_samples_SWITCH`
`static @Nullable String`	`ppt_max_name`	If set, only ppts less than ppt_max_name are included.
`static @Nullable Pattern`	`ppt_omit_regexp`
`static String`	`ppt_omit_regexp_SWITCH`
`static @Nullable Pattern`	`ppt_regexp`
`static String`	`ppt_regexp_SWITCH`
`static String`	`progress`	Human-friendly progress status message.
`static ArrayList<Invariant>`	`proto_invs`
`static String`	`release_date`	The date for the current version of Daikon.
`static String`	`release_string`	A description of the Daikon release (version number, date, and URL).
`static String`	`release_version`	The current version of Daikon.
`static @MonotonicNonNull File`	`server_dir`
`static String`	`server_SWITCH`
`static String`	`show_detail_progress_SWITCH`	option show-detail-progress
`static boolean`	`show_progress`	When true, show how much time each Daikon phase took.
`static String`	`show_progress_SWITCH`	option show-progress
`static boolean`	`suppress_redundant_invariants_with_simplify`	Whether to use the bottom up implementation of the dataflow hierarchy.
`static String`	`suppress_redundant_SWITCH`
`static String`	`track_SWITCH`
`static boolean`	`use_dataflow_hierarchy`	Whether to associate the program points in a dataflow hierarchy, as via Nimmer's thesis.
`static boolean`	`use_equality_optimization`	Whether to use the "new" equality set mechanism for handling equality, using canonicals to have instantiation of invariants only over equality sets.
`static String`	`user_defined_invariant_SWITCH`
`static boolean`	`using_DaikonSimple`	Boolean.
`static @Nullable Pattern`	`var_omit_regexp`
`static String`	`var_omit_regexp_SWITCH`
`static @Nullable Pattern`	`var_regexp`
`static String`	`var_regexp_SWITCH`
`static String`	`wrap_xml_SWITCH`

Method Summary

All Methods Static Methods Concrete Methods
Modifier and Type	Method	Description
`static void`	`cleanup()`	Cleans up static variables so that mainHelper can be called more than once.
`static void`	`create_combined_exits(PptMap ppts)`	Create EXIT program points as needed for EXITnn program points.
`static void`	`create_splitters(Set<File> spinfo_files)`	Create user-defined splitters.
`static void`	`createUpperPpts(PptMap all_ppts)`	Creates invariants for upper program points by merging together the invariants from all of the lower points.
`static String`	`getOptarg(Getopt g)`	Just like `g.getOptarg()`, but only to be called in circumstances when the programmer knows that the return value is non-null.
`static void`	`handleDaikonTerminationException(Daikon.DaikonTerminationException e)`	Handle DaikonTerminationExceptions.
`static void`	`init_ppt(PptTopLevel ppt, PptMap all_ppts)`	Setup splitters.
`static void`	`main(String[] args)`	The arguments to daikon.Daikon are file names.
`static void`	`mainHelper(String[] args)`	This does the work of `main(java.lang.String[])`, but it never calls System.exit, so it is appropriate to be called progrmmatically.
`static void`	`ppt_stats(PptMap all_ppts)`	Print out basic statistics (samples, invariants, variables, etc) about each ppt.
`static void`	`setup_NISuppression()`	Initialize NIS suppression.
`static void`	`setup_proto_invs()`	Creates the list of prototype invariants for all Daikon invariants.
`static void`	`setup_splitters(PptTopLevel ppt)`	Sets up splitting on all ppts.
`static void`	`setupEquality(PptTopLevel ppt)`	Initialize the equality sets for each variable.
`static void`	`undoOpts(PptMap all_ppts)`	Undoes the invariants suppressed for the dynamic constant, suppression and equality set optimizations (should yield the same invariants as the simple incremental algorithm.

Methods inherited from class Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

- Field Detail
  - dkconfig_progress_delay
```
public static int dkconfig_progress_delay
```
    The amount of time to wait between updates of the progress display, measured in milliseconds. A value of -1 means do not print the progress display at all.
  - release_version
```
public static final String release_version
```
    The current version of Daikon.
    
    See Also:
    
    Constant Field Values
  - release_date
```
public static final String release_date
```
    The date for the current version of Daikon.
    
    See Also:
    
    Constant Field Values
  - release_string
```
public static final String release_string
```
    A description of the Daikon release (version number, date, and URL).
    
    See Also:
    
    Constant Field Values
  - dkconfig_output_conditionals
```
public static boolean dkconfig_output_conditionals
```
    Boolean. Controls whether conditional program points are displayed.
  - dkconfig_calc_possible_invs
```
public static boolean dkconfig_calc_possible_invs
```
    Boolean. Just print the total number of possible invariants and exit.
  - dkconfig_ppt_perc
```
public static int dkconfig_ppt_perc
```
    Integer. Percentage of program points to process. All program points are sorted by name, and all samples for the first ppt_perc program points are processed. A percentage of 100 matches all program points.
  - dkconfig_print_sample_totals
```
public static boolean dkconfig_print_sample_totals
```
    Boolean. Controls whether or not the total samples read and processed are printed at the end of processing.
  - lineSep
```
public static final String lineSep
```
  - dkconfig_quiet
```
public static boolean dkconfig_quiet
```
    Boolean. Controls whether or not processing information is printed out. Setting this variable to true also automatically sets progress_delay to -1.
  - check_program_types
```
public static final boolean check_program_types
```
    See Also:
    
    Constant Field Values
  - invariants_check_canBeMissing
```
public static final boolean invariants_check_canBeMissing
```
    See Also:
    
    Constant Field Values
  - invariants_check_canBeMissing_arrayelt
```
public static final boolean invariants_check_canBeMissing_arrayelt
```
    See Also:
    
    Constant Field Values
  - disable_modbit_check_message
```
public static final boolean disable_modbit_check_message
```
    See Also:
    
    Constant Field Values
  - disable_modbit_check_error
```
public static final boolean disable_modbit_check_error
```
    Not a good idea to set this to true, as it is too easy to ignore the warnings and the modbit problem can cause an error later.
    
    See Also:
    
    Constant Field Values
  - no_text_output
```
public static boolean no_text_output
```
    When true, don't print textual output.
  - show_progress
```
public static boolean show_progress
```
    When true, show how much time each Daikon phase took. Has no effect if System.console() is not connected to a terminal. If option show-detail-progress was used, also show how much time each program point took.
  - use_equality_optimization
```
public static boolean use_equality_optimization
```
    Whether to use the "new" equality set mechanism for handling equality, using canonicals to have instantiation of invariants only over equality sets.
  - dkconfig_undo_opts
```
public static boolean dkconfig_undo_opts
```
    Boolean. Controls whether the Daikon optimizations (equality sets, suppressions) are undone at the end to create a more complete set of invariants. Output does not include conditional program points, implications, reflexive and partially reflexive invariants.
  - using_DaikonSimple
```
public static boolean using_DaikonSimple
```
    Boolean. Indicates to Daikon classes and methods that the methods calls should be compatible to DaikonSimple because Daikon and DaikonSimple share methods. Default value is 'false'.
  - dkconfig_guardNulls
```
public static @Interned String dkconfig_guardNulls
```
    If "always", then invariants are always guarded. If "never", then invariants are never guarded. If "missing", then invariants are guarded only for variables that were missing ("can be missing") in the dtrace (the observed executions). If "default", then use "missing" mode for Java output and "never" mode otherwise.
    Guarding means adding predicates that ensure that variables can be dereferenced. For instance, if a can be null --- that is, if a.b can be nonsensical --- then the guarded version of
    a.b == 5
    is
    (a != null) ⇒ (a.b == 5)
    .
    (To do: Some configuration option (maybe this one) should add guards for other reasons that lead to nonsensical values (@pxref{Variable names}).)
  - use_dataflow_hierarchy
```
public static boolean use_dataflow_hierarchy
```
    Whether to associate the program points in a dataflow hierarchy, as via Nimmer's thesis. Deactivate only for languages and analyses where flow relation is nonsensical.
  - suppress_redundant_invariants_with_simplify
```
public static boolean suppress_redundant_invariants_with_simplify
```
    Whether to use the bottom up implementation of the dataflow hierarchy. This mechanism builds invariants initially only at the leaves of the partial order. Upper points are calculated by joining the invariants from each of their children points.
  - output_format
```
public static OutputFormat output_format
```
  - output_num_samples
```
public static boolean output_num_samples
```
  - ignore_comparability
```
public static boolean ignore_comparability
```
  - ppt_regexp
```
public static @Nullable Pattern ppt_regexp
```
  - ppt_omit_regexp
```
public static @Nullable Pattern ppt_omit_regexp
```
  - var_regexp
```
public static @Nullable Pattern var_regexp
```
  - var_omit_regexp
```
public static @Nullable Pattern var_omit_regexp
```
  - ppt_max_name
```
public static @Nullable String ppt_max_name
```
    If set, only ppts less than ppt_max_name are included. Used by the configuration option dkconfig_ppt_percent to only work on a specified percent of the ppts.
  - inv_file
```
public static @Nullable File inv_file
```
  - noversion_output
```
public static boolean noversion_output
```
    Whether Daikon should print its version number and date.
  - isInferencing
```
public static boolean isInferencing
```
    Whether Daikon is in its inferencing loop. Used only for assertion checks.
  - omit_from_output
```
public static boolean omit_from_output
```
    When true, omit certain invariants from the output .inv file. Generally these are invariants that wouldn't be printed in any case; but by default, they're retained in the .inv file in case they would be useful for later processing. (For instance, we might at some point in the future support resuming processing with more data from an .inv file). These invariants can increase the size of the .inv file, though, so when only limited further processing is needed, it can save space to omit them.
  - omit_types
```
public static boolean[] omit_types
```
    An array of flags, indexed by characters, in which a true entry means that invariants of that sort should be omitted from the output .inv file.
  - help_SWITCH
```
public static final String help_SWITCH
```
    option help
    
    See Also:
    
    Constant Field Values
  - no_text_output_SWITCH
```
public static final String no_text_output_SWITCH
```
    option no-text-output
    
    See Also:
    
    Constant Field Values
  - format_SWITCH
```
public static final String format_SWITCH
```
    option format
    
    See Also:
    
    Constant Field Values
  - show_progress_SWITCH
```
public static final String show_progress_SWITCH
```
    option show-progress
    
    See Also:
    
    Constant Field Values
  - show_detail_progress_SWITCH
```
public static final String show_detail_progress_SWITCH
```
    option show-detail-progress
    
    See Also:
    
    Constant Field Values
  - no_show_progress_SWITCH
```
public static final String no_show_progress_SWITCH
```
    option no-show-progress
    
    See Also:
    
    Constant Field Values
  - noversion_SWITCH
```
public static final String noversion_SWITCH
```
    option noversion
    
    See Also:
    
    Constant Field Values
  - output_num_samples_SWITCH
```
public static final String output_num_samples_SWITCH
```
    See Also:
    
    Constant Field Values
  - files_from_SWITCH
```
public static final String files_from_SWITCH
```
    See Also:
    
    Constant Field Values
  - omit_from_output_SWITCH
```
public static final String omit_from_output_SWITCH
```
    See Also:
    
    Constant Field Values
  - conf_limit_SWITCH
```
public static final String conf_limit_SWITCH
```
    See Also:
    
    Constant Field Values
  - list_type_SWITCH
```
public static final String list_type_SWITCH
```
    See Also:
    
    Constant Field Values
  - user_defined_invariant_SWITCH
```
public static final String user_defined_invariant_SWITCH
```
    See Also:
    
    Constant Field Values
  - disable_all_invariants_SWITCH
```
public static final String disable_all_invariants_SWITCH
```
    See Also:
    
    Constant Field Values
  - no_dataflow_hierarchy_SWITCH
```
public static final String no_dataflow_hierarchy_SWITCH
```
    See Also:
    
    Constant Field Values
  - suppress_redundant_SWITCH
```
public static final String suppress_redundant_SWITCH
```
    See Also:
    
    Constant Field Values
  - ppt_regexp_SWITCH
```
public static final String ppt_regexp_SWITCH
```
    See Also:
    
    Constant Field Values
  - ppt_omit_regexp_SWITCH
```
public static final String ppt_omit_regexp_SWITCH
```
    See Also:
    
    Constant Field Values
  - var_regexp_SWITCH
```
public static final String var_regexp_SWITCH
```
    See Also:
    
    Constant Field Values
  - var_omit_regexp_SWITCH
```
public static final String var_omit_regexp_SWITCH
```
    See Also:
    
    Constant Field Values
  - server_SWITCH
```
public static final String server_SWITCH
```
    See Also:
    
    Constant Field Values
  - config_SWITCH
```
public static final String config_SWITCH
```
    See Also:
    
    Constant Field Values
  - config_option_SWITCH
```
public static final String config_option_SWITCH
```
    See Also:
    
    Constant Field Values
  - debugAll_SWITCH
```
public static final String debugAll_SWITCH
```
    See Also:
    
    Constant Field Values
  - debug_SWITCH
```
public static final String debug_SWITCH
```
    See Also:
    
    Constant Field Values
  - track_SWITCH
```
public static final String track_SWITCH
```
    See Also:
    
    Constant Field Values
  - disc_reason_SWITCH
```
public static final String disc_reason_SWITCH
```
    See Also:
    
    Constant Field Values
  - mem_stat_SWITCH
```
public static final String mem_stat_SWITCH
```
    See Also:
    
    Constant Field Values
  - wrap_xml_SWITCH
```
public static final String wrap_xml_SWITCH
```
    See Also:
    
    Constant Field Values
  - server_dir
```
public static @MonotonicNonNull File server_dir
```
  - all_ppts
```
public static PptMap all_ppts
```
    A PptMap (mapping from String to PptTopLevel) that contains all the program points. Set in mainHelper().
  - current_inv
```
public static @Nullable Invariant current_inv
```
    current invariant (used for debugging)
  - proto_invs
```
public static ArrayList<Invariant> proto_invs
```
  - debugTrace
```
public static final Logger debugTrace
```
    Debug tracer.
  - debugProgress
```
public static final Logger debugProgress
```
  - debugEquality
```
public static final Logger debugEquality
```
  - debugInit
```
public static final Logger debugInit
```
    Debug tracer for ppt initialization.
  - debugStats
```
public static final Logger debugStats
```
    Prints out statistics concerning equality sets, suppressions, etc.
  - dkconfig_progress_display_width
```
public static int dkconfig_progress_display_width
```
    The number of columns of progress information to display. In many Unix shells, this can be set to an appropriate value by --config_option daikon.Daikon.progress_display_width=$COLUMNS.
  - progress
```
public static String progress
```
    Human-friendly progress status message. If fileio_progress is non-null, then this is ignored. So this is primarily for progress reports that are not IO-related.
- Method Detail
  - main
```
public static void main(String[] args)
```
    The arguments to daikon.Daikon are file names. Declaration file names end in ".decls", and data trace file names end in ".dtrace".
  - handleDaikonTerminationException
```
public static void handleDaikonTerminationException(Daikon.DaikonTerminationException e)
```
    Handle DaikonTerminationExceptions. Others are left to be handled by the default handler, which prints a more informative stack trace.
  - mainHelper
```
public static void mainHelper(String[] args)
```
    This does the work of main(java.lang.String[]), but it never calls System.exit, so it is appropriate to be called progrmmatically.
    
    Parameters:
    
    args - the command-line arguments
  - cleanup
```
public static void cleanup()
```
    Cleans up static variables so that mainHelper can be called more than once.
  - getOptarg
```
@Pure
public static String getOptarg(Getopt g)
```
    Just like g.getOptarg(), but only to be called in circumstances when the programmer knows that the return value is non-null.
    
    Parameters:
    
    g - a command-line argument processor
    
    Returns:
    
    the value for an argument found by g
  - setup_proto_invs
```
public static void setup_proto_invs()
```
    Creates the list of prototype invariants for all Daikon invariants. New invariants must be added to this list.
  - createUpperPpts
```
public static void createUpperPpts(PptMap all_ppts)
```
    Creates invariants for upper program points by merging together the invariants from all of the lower points.
  - init_ppt
```
public static void init_ppt(PptTopLevel ppt,
                            PptMap all_ppts)
```
    Setup splitters. Add orig and derived variables. Recursively call init_ppt on splits.
  - create_combined_exits
```
public static void create_combined_exits(PptMap ppts)
```
    Create EXIT program points as needed for EXITnn program points.
  - setup_splitters
```
public static void setup_splitters(PptTopLevel ppt)
```
    Sets up splitting on all ppts. Currently only binary splitters over boolean returns or exactly two return statements are enabled by default (though other splitters can be defined by the user).
    
    Parameters:
    
    ppt - the program point to add conditions to
  - ppt_stats
```
public static void ppt_stats(PptMap all_ppts)
```
    Print out basic statistics (samples, invariants, variables, etc) about each ppt.
  - setup_NISuppression
```
@EnsuresNonNull({"daikon.suppress.NIS.suppressor_map","daikon.suppress.NIS.suppressor_map_suppression_count","daikon.suppress.NIS.all_suppressions","daikon.suppress.NIS.suppressor_proto_invs"})
public static void setup_NISuppression()
```
    Initialize NIS suppression.
  - setupEquality
```
public static void setupEquality(PptTopLevel ppt)
```
    Initialize the equality sets for each variable.
  - create_splitters
```
public static void create_splitters(Set<File> spinfo_files)
                             throws IOException
```
    Create user-defined splitters. For each file in the input, add a SpinfoFile to the spinfoFiles variable.
    
    Throws:
    
    IOException
  - undoOpts
```
@RequiresNonNull({"daikon.suppress.NIS.all_suppressions","daikon.suppress.NIS.suppressor_map"})
public static void undoOpts(PptMap all_ppts)
```
    Undoes the invariants suppressed for the dynamic constant, suppression and equality set optimizations (should yield the same invariants as the simple incremental algorithm.

Class Daikon

Nested Class Summary

Field Summary

Method Summary

Methods inherited from class Object

Field Detail

dkconfig_progress_delay

release_version

release_date

release_string

dkconfig_output_conditionals

dkconfig_calc_possible_invs

dkconfig_ppt_perc

dkconfig_print_sample_totals

lineSep

dkconfig_quiet

check_program_types

invariants_check_canBeMissing

invariants_check_canBeMissing_arrayelt

disable_modbit_check_message

disable_modbit_check_error

no_text_output

show_progress

use_equality_optimization

dkconfig_undo_opts

using_DaikonSimple

dkconfig_guardNulls

use_dataflow_hierarchy

suppress_redundant_invariants_with_simplify

output_format

output_num_samples

ignore_comparability

ppt_regexp

ppt_omit_regexp

var_regexp

var_omit_regexp

ppt_max_name

inv_file

noversion_output

isInferencing

omit_from_output

omit_types

help_SWITCH

no_text_output_SWITCH

format_SWITCH

show_progress_SWITCH

show_detail_progress_SWITCH

no_show_progress_SWITCH

noversion_SWITCH

output_num_samples_SWITCH

files_from_SWITCH

omit_from_output_SWITCH

conf_limit_SWITCH

list_type_SWITCH

user_defined_invariant_SWITCH

disable_all_invariants_SWITCH

no_dataflow_hierarchy_SWITCH

suppress_redundant_SWITCH

ppt_regexp_SWITCH

ppt_omit_regexp_SWITCH

var_regexp_SWITCH

var_omit_regexp_SWITCH

server_SWITCH

config_SWITCH

config_option_SWITCH

debugAll_SWITCH

debug_SWITCH

track_SWITCH

disc_reason_SWITCH

mem_stat_SWITCH

wrap_xml_SWITCH

server_dir

all_ppts

current_inv

proto_invs

debugTrace

debugProgress

debugEquality

debugInit

debugStats