Merge pull request #497 from thk123/refactor/coding-standards-makefile-program-flags

Extended the coding standard

Author: Daniel Kroening

CODING_STANDARD

@@ -92,6 +92,35 @@ Header files:
   of the header file rather than in line
 - Guard headers with #ifndef CPROVER_DIRECTORIES_FILE_H, etc
 
+Make files
+- Each source file should appear on a separate line
+- The final source file should still be followed by a trailing slash
+- The last line should be a comment to not be deleted, i.e. should look like:
+```
+SRC = source_file.cpp \
+      source_file2.cpp \
+      # Empty last line
+```
+- This ensures the Makefiles can be easily merged.
+
+Program Command Line Options
+- Each program contains a program_name_parse_optionst class which should
+  contain a define PROGRAM_NAME_PARSE_OPTIONS which is a string of all the
+  parse options in brackets (with a colon after the bracket if it takes a
+  parameter)
+- Each parameter should be one per line to yield easy merging
+- If parameters are shared between programs, they should be pulled out into
+  a common file and then included using a define
+- The defines should be OPT_FLAG_NAMES which should go into the OPTIONS define
+- The defines should include HELP_FLAG_NAMES which should contain the help
+  output of the format:
+  ```
+  " --flag                explanations\n" \
+  " --another flag        more explanation\n" \
+   <-------30 chars------>
+- The defines may include PARSE_OPTIONS_FLAG_NAMES which move the options
+  from the command line into the options
+
 C++ features:
 - Do not use namespaces.
 - Prefer use of 'typedef' insted of 'using'.
@@ -143,3 +172,13 @@ Output:
 - Use '\n' instead of std::endl
 
 You are allowed to break rules if you have a good reason to do so.
+
+Pre-commit hook to run cpplint locally
+--------------------------------------
+To install the hook
+cp .githooks/pre-commit .git/hooks/pre-commit
+or use a symbolic link.
+Then, when running git commit, you should get the linter output
+(if any) before being prompted to enter a commit message.
+To bypass the check (e.g. if there was a false positive),
+add the option --no-verify.

src/analyses/Makefile

@@ -1,13 +1,30 @@
-SRC = natural_loops.cpp is_threaded.cpp dirty.cpp interval_analysis.cpp \
-      invariant_set.cpp invariant_set_domain.cpp invariant_propagation.cpp \
-      static_analysis.cpp uninitialized_domain.cpp local_may_alias.cpp \
-      locals.cpp goto_check.cpp call_graph.cpp interval_domain.cpp \
-      goto_rw.cpp reaching_definitions.cpp ai.cpp local_cfg.cpp \
-      local_bitvector_analysis.cpp dependence_graph.cpp \
-      constant_propagator.cpp replace_symbol_ext.cpp \
-      flow_insensitive_analysis.cpp \
-      custom_bitvector_analysis.cpp escape_analysis.cpp global_may_alias.cpp \
+SRC = ai.cpp \
+      call_graph.cpp \
+      constant_propagator.cpp \
+      custom_bitvector_analysis.cpp \
+      dependence_graph.cpp \
+      dirty.cpp \
       does_remove_const.cpp \
+      escape_analysis.cpp \
+      flow_insensitive_analysis.cpp \
+      global_may_alias.cpp \
+      goto_check.cpp \
+      goto_rw.cpp \
+      interval_analysis.cpp \
+      interval_domain.cpp \
+      invariant_propagation.cpp \
+      invariant_set.cpp \
+      invariant_set_domain.cpp \
+      is_threaded.cpp \
+      local_bitvector_analysis.cpp \
+      local_cfg.cpp \
+      local_may_alias.cpp \
+      locals.cpp \
+      natural_loops.cpp \
+      reaching_definitions.cpp \
+      replace_symbol_ext.cpp \
+      static_analysis.cpp \
+      uninitialized_domain.cpp \
       # Empty last line
 
 INCLUDES= -I ..

src/ansi-c/Makefile

@@ -1,20 +1,44 @@
-SRC = c_typecast.cpp ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_parser.cpp \
-      expr2c.cpp ansi_c_language.cpp c_sizeof.cpp ansi_c_scope.cpp \
-      c_types.cpp ansi_c_typecheck.cpp \
-      c_preprocess.cpp c_storage_spec.cpp \
-      c_typecheck_base.cpp c_typecheck_initializer.cpp \
-      c_typecheck_typecast.cpp c_typecheck_code.cpp \
-      c_typecheck_expr.cpp c_typecheck_type.cpp string_constant.cpp \
-      c_qualifiers.cpp c_typecheck_argc_argv.cpp ansi_c_parse_tree.cpp \
-      preprocessor_line.cpp ansi_c_convert_type.cpp \
-      type2name.cpp cprover_library.cpp anonymous_member.cpp \
-      printf_formatter.cpp ansi_c_internal_additions.cpp padding.cpp \
-      ansi_c_declaration.cpp designator.cpp ansi_c_entry_point.cpp \
-      literals/parse_float.cpp literals/unescape_string.cpp \
-      literals/convert_float_literal.cpp \
+SRC = anonymous_member.cpp \
+      ansi_c_convert_type.cpp \
+      ansi_c_declaration.cpp \
+      ansi_c_entry_point.cpp \
+      ansi_c_internal_additions.cpp \
+      ansi_c_language.cpp \
+      ansi_c_lex.yy.cpp \
+      ansi_c_parse_tree.cpp \
+      ansi_c_parser.cpp \
+      ansi_c_scope.cpp \
+      ansi_c_typecheck.cpp \
+      ansi_c_y.tab.cpp \
+      c_misc.cpp \
+      c_preprocess.cpp \
+      c_qualifiers.cpp \
+      c_sizeof.cpp \
+      c_storage_spec.cpp \
+      c_typecast.cpp \
+      c_typecheck_argc_argv.cpp \
+      c_typecheck_base.cpp \
+      c_typecheck_code.cpp \
+      c_typecheck_expr.cpp \
+      c_typecheck_initializer.cpp \
+      c_typecheck_type.cpp \
+      c_typecheck_typecast.cpp \
+      c_types.cpp \
+      cprover_library.cpp \
+      designator.cpp \
+      expr2c.cpp \
       literals/convert_character_literal.cpp \
+      literals/convert_float_literal.cpp \
       literals/convert_integer_literal.cpp \
-      literals/convert_string_literal.cpp c_misc.cpp
+      literals/convert_string_literal.cpp \
+      literals/parse_float.cpp \
+      literals/unescape_string.cpp \
+      padding.cpp \
+      preprocessor_line.cpp \
+      printf_formatter.cpp \
+      string_constant.cpp \
+      type2name.cpp \
+      # Empty last line
 
 INCLUDES= -I ..
 

src/assembler/Makefile

@@ -1,5 +1,6 @@
-SRC = assembler_lex.yy.cpp assembler_parser.cpp
-
+SRC = assembler_lex.yy.cpp \
+      assembler_parser.cpp \
+      # Empty last line
 INCLUDES= -I ..
 
 include ../config.inc

src/cbmc/Makefile

@@ -1,8 +1,19 @@
-SRC = cbmc_main.cpp cbmc_parse_options.cpp bmc.cpp cbmc_dimacs.cpp \
-      cbmc_languages.cpp counterexample_beautification.cpp \
-      bv_cbmc.cpp symex_bmc.cpp show_vcc.cpp cbmc_solvers.cpp \
-      xml_interface.cpp bmc_cover.cpp all_properties.cpp \
-      fault_localization.cpp symex_coverage.cpp
+SRC = all_properties.cpp \
+      bmc.cpp \
+      bmc_cover.cpp \
+      bv_cbmc.cpp \
+      cbmc_dimacs.cpp \
+      cbmc_languages.cpp \
+      cbmc_main.cpp \
+      cbmc_parse_options.cpp \
+      cbmc_solvers.cpp \
+      counterexample_beautification.cpp \
+      fault_localization.cpp \
+      show_vcc.cpp \
+      symex_bmc.cpp \
+      symex_coverage.cpp \
+      xml_interface.cpp \
+      # Empty last line
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \