diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-05 08:26:37 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-05 08:26:37 +0000 |
commit | 88b52c971b43248e6ceacf1c8140a06427d0418d (patch) | |
tree | 4ee443c898a858fcdd658f3f043e4180eddd8784 /contrib/code-checker | |
parent | 29cc307cdf2c42bebf4f5615874a864783f47fd0 (diff) |
* public/private code untangled (smt/smt_engine.h no longer #includes
expr/node.h). This removes the warnings we had during compilation,
and heads off a number of potential linking errors due to improper
inlining of private (library-only) stuff in client (out-of-library)
code.
* "configure" now takes some options as part of a "bare-option" build
type (e.g., "./configure debug-coverage" or "./configure production-muzzle").
* split cdo.h, cdlist.h, cdmap.h, and cdset.h from context.h
* split cdlist_black unit test from context_black
* implement CDMap<>.
* give ExprManagers ownership of the context (and have SmtEngine share
that one)
* fix main driver to properly report file-not-found
* fix MemoryMappedInputBuffer class to report reasons for
"errno"-returned system errors
* src/expr/attribute.h: context-dependent attribute kinds now
supported
* test/unit/expr/node_white.h: context-dependent attribute tests
* src/prop/cnf_conversion.h and associated parts of src/util/options.h
and src/main/getopt.cpp: obsolete command-line option, removed.
* src/util/Assert.h: assertions are now somewhat more useful (in debug
builds, anyway) during stack unwinding.
* test/unit/theory/theory_black.h: test context-dependent behavior of
registerTerm() attribute for theories
* src/expr/node_builder.h: formatting, fixes for arithmetic
convenience node builders, check memory allocations
* test/unit/expr/node_builder_black.h: add tessts for addition,
subtraction, unary minus, and multiplication convenience node
builders
* src/expr/attribute.h: more comments
* (various) code formatting, comment cleanup, added throws specifier
to some destructors
* contrib/code-checker: prototype perl script to test (some) code policy
* contrib/indent-settings: command line for GNU indent to indent using
CVC4 style (sort of; this is a work in progress)
* COPYING: legal stuff
* DESIGN_QUESTIONS: obsolete, removed
Diffstat (limited to 'contrib/code-checker')
-rwxr-xr-x | contrib/code-checker | 96 |
1 files changed, 96 insertions, 0 deletions
diff --git a/contrib/code-checker b/contrib/code-checker new file mode 100755 index 000000000..a40dc61af --- /dev/null +++ b/contrib/code-checker @@ -0,0 +1,96 @@ +#!/usr/bin/perl -w + +use strict; + +while($#ARGV >= 0) { + my %FP; + my $file = shift @ARGV; + + local $/ = undef; + + open(FP, $file) || die "can't read $file"; + print "checking $file...\n"; + binmode FP; + my $buf = <FP>; + close FP; + + print "file named incorrectly; use *.h: $file\n" if $file =~ /\.(hpp|H|hh)$/; + print "file named incorrectly; use *.cpp: $file\n" if $file =~ /\.(C|cc)$/; + if($file =~ /\.(h|hpp|H)$/) { + check_as_header($buf); + } elsif($file =~ /\.(h|cpp|C)$/) { + check_as_source($buf); + } else { + die "$file not checked (unknown type of file)"; + } + open(FP, "cpp -nostdinc \"$file\" 2>/dev/null |") || die "can't cpp $file"; + binmode FP; + $buf = <FP>; + close FP; + + if($file =~ /\.(h|hpp|H)$/) { + check_as_header_cpp($buf); + } elsif($file =~ /\.(h|cpp|C)$/) { + check_as_source_cpp($buf); + } else { + die "$file not checked (unknown type of file)"; + } +} + +sub check_as_any { + my($buf) = @_; + + print "no file head comment\n" unless $buf =~ m,^/*\*\*\*,; +} + +sub check_as_header { + my($buf) = @_; + check_as_any($buf); +} + +sub check_as_source { + my($buf) = @_; + check_as_any($buf); +} + +sub check_as_any_cpp { + my($buf) = @_; + + print "need space between tokens ) and {\n" if $buf =~ /\)\{/; + print "need space between tokens 'const' and {\n" if $buf =~ /\bconst\{/; + print "need space between tokens ) and 'const'\n" if $buf =~ /\)const\b/; + print "need space between tokens 'template' and <\n" if $buf =~ /\btemplate</; + print "need space between tokens } and 'else'\n" if $buf =~ /\}else\b/; + print "need space between tokens 'else' and {\n" if $buf =~ /\belse\{/; + print "need space between tokens 'do' and {\n" if $buf =~ /\bdo\{/; + print "need space between tokens } and 'while'\n" if $buf =~ /\}while\b/; + + print "no space permitted before ;\n" if $buf =~ /\s+;/; + print "no space permitted between tokens 'if' and (\n" if $buf =~ /\bif\s\(/; + print "no space permitted between tokens 'while' and (\n" if $buf =~ /\bwhile\s\(/; + print "no space permitted between tokens 'for' and (\n" if $buf =~ /\bfor\s\(/; + + my $code = $buf; + $code =~ s,\\.,.,g; + $code =~ s,"[^"]*","",g; + + #print "'if' blocks must be braced, '{' should be last character on block opening line\n" if $code =~ /\bif\b.*[^{]\s*$/m; + #print "'while' blocks must be braced, '{' should be last character on block opening line\n" if $code =~ /\bwhile\b.*[^{]\s*$/m; + #print "'for' blocks must be braced, '{' should be last character on block opening line\n" if $code =~ /\bfor\b.*[^{]\s*$/m; + print "'else' cannot start a line (should follow preceding '}')\n" if $code =~ /^\s+else\b/m; +} + +sub check_as_header_cpp { + my($buf) = @_; + check_as_any_cpp($buf); +} + +sub check_as_source_cpp { + my($buf) = @_; + check_as_any_cpp($buf); +} + +## Local Variables: +## perl-indent-level: 2 +## perl-brace-offset: 0 +## End: |