Skip to content

Extended the coding standard #497

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 39 additions & 0 deletions CODING_STANDARD
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

May I suggest the additional suggestion of having those lists lexicographically sorted?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This sounds good - but it is sort of meaningless until they are all sorted (where as this change can come in to effect gradually I think). If someone wants to go through and fix this (probably with a script I guess...) then this sounds like a good rule.

That said, I'm not sure I see a big benefit though, Makefiles are mainly for the computer rather than the developer to read.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The benefit would only show when it becomes easier to tell whether any duplicates arise. (An issue we have already had with #include files, which we currently don't sort in any particular way.)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you think it is worth adding the rule now, given that everything is out of order? If so how do you want to tackle it? I suppose it wouldn't be too hard to write a script to apply these changes to all the Makefiles and check in en masse.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am also for ordering. @thk123, can you make a PR that orders them once and for all? Then, having the rule makes sense.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@peterschrammel I can do, but don't know when I will be able to get to it; probably won't be a priority until after February


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'.
Expand Down Expand Up @@ -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.
35 changes: 26 additions & 9 deletions src/analyses/Makefile
Original file line number Diff line number Diff line change
@@ -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 ..
Expand Down
54 changes: 39 additions & 15 deletions src/ansi-c/Makefile
Original file line number Diff line number Diff line change
@@ -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 ..

Expand Down
5 changes: 3 additions & 2 deletions src/assembler/Makefile
Original file line number Diff line number Diff line change
@@ -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
Expand Down
21 changes: 16 additions & 5 deletions src/cbmc/Makefile
Original file line number Diff line number Diff line change
@@ -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) \
Expand Down
Loading