initial commit

git-svn-id: http://www.cprover.org/svn/cbmc/trunk@1 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

CODING_STANDARD

@@ -0,0 +1,17 @@
+Here a few minimalistic coding rules for the cprover source tree:
+
+a) 2 spaces indent, no tabs
+b) no "using namespace std;"
+c) Avoid new/delete, use containers instead.
+d) Avoid unnecessary #includes, especially in header files
+e) No lines wider than 80 chars
+f) Put matching { } into the same column
+g) If a method is bigger than a page, break it into parts
+h) Avoid destructive updates if possible. The irept has
+   constant time copy.
+
+Architecture-specific code:
+
+a) Avoid if possible.
+b) Use __LINUX__, __MACH__, and _WIN32 to distinguish the architectures.
+c) Don't include architecture-specific header files without #ifdef ...

LICENSE

@@ -0,0 +1,40 @@
+(C) 2001-2011, Daniel Kroening, Edmund Clarke,
+Computer Science Department, Oxford University
+Computer Systems Institute, ETH Zurich
+Computer Science Department, Carnegie Mellon University
+
+All rights reserved. Redistribution and use in source and binary forms, with
+or without modification, are permitted provided that the following
+conditions are met:
+
+  1. Redistributions of source code must retain the above copyright
+     notice, this list of conditions and the following disclaimer.
+
+  2. Redistributions in binary form must reproduce the above copyright
+     notice, this list of conditions and the following disclaimer in the
+     documentation and/or other materials provided with the distribution.
+
+  3. All advertising materials mentioning features or use of this software
+     must display the following acknowledgement:
+
+     This product includes software developed by Daniel Kroening,
+     Edmund Clarke,
+     Computer Science Department, Oxford University
+     Computer Systems Institute, ETH Zurich
+     Computer Science Department, Carnegie Mellon University
+
+  4. Neither the name of the University nor the names of its contributors
+     may be used to endorse or promote products derived from this software
+     without specific prior written permission.
+
+
+THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS `AS IS'' AND ANY
+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED.  IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE FOR ANY
+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
+THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

src/Makefile

@@ -0,0 +1,163 @@
+DIRS = ansi-c big-int cbmc cprover csp ebmc hoare \
+       infrules intrep solvers pvs separate smvlang util verilog \
+       vhdl langapi netlist cpp pascal symex termination \
+       satqe satmc satabs explain specc xmllang promela \
+       goto-programs bplang vcegar hw-cbmc vsynth \
+       boppo pointer-analysis cogent goto-instrument \
+       goto-symex ipp prover trans bv_refinement mcp goto-cc \
+       smtlang php cemc interpolation scoot floatbv cover \
+       scratch ai k-induction
+
+all: cprover.dir cbmc.dir ebmc.dir cogent.dir \
+     satabs.dir hw-cbmc.dir promela.dir \
+     boppo.dir goto-cc.dir goto-instrument.dir cover.dir
+
+include config.inc
+include common
+
+###############################################################################
+
+util.dir: big-int.dir
+
+languages: util.dir langapi.dir \
+           ansi-c.dir intrep.dir smvlang.dir \
+           xmllang.dir promela.dir bplang.dir
+
+goto-instrument.dir: goto-programs.dir languages pointer-analysis.dir
+
+cogent.dir: ansi-c.dir util.dir solvers.dir
+
+cprover.dir: languages
+
+cbmc.dir: languages solvers.dir goto-symex.dir \
+          pointer-analysis.dir goto-programs.dir goto-symex.dir
+
+cover.dir: cbmc.dir
+
+ivt.dir: languages solvers.dir goto-symex.dir \
+         pointer-analysis.dir goto-programs.dir goto-symex.dir
+
+cemc.dir: cbmc.dir
+
+scoot.dir: satabs.dir languages
+
+goto-cc.dir: languages pointer-analysis.dir goto-programs.dir
+
+hw-cbmc.dir: cbmc.dir trans.dir
+
+boppo.dir: langapi.dir bplang.dir promela.dir util.dir \
+           solvers.dir languages
+
+explain.dir: cbmc.dir
+
+satabs.dir: languages goto-symex.dir goto-programs.dir \
+            pointer-analysis.dir solvers.dir
+
+vcegar.dir: languages satqe.dir solvers.dir ebmc.dir
+
+vsynth.dir: langapi.dir verilog.dir util.dir vhdl.dir netlist.dir
+
+ebmc.dir: solvers.dir languages trans.dir
+
+satmc.dir: solvers.dir smvlang.dir util.dir verilog.dir languages \
+           intrep.dir vhdl.dir netlist.dir trans.dir satqe.dir
+k-induction.dir: cbmc.dir ai.dir
+
+scratch.dir: k-induction.dir
+
+ai.dir: cbmc.dir
+
+ifdef MODULE_INTERPOLATION
+ebmc.dir: interpolation.dir
+interpolation.dir: solvers.dir langapi.dir util.dir
+endif
+
+ifdef MODULE_PROVER
+satabs.dir: prover.dir
+ebmc.dir: prover.dir
+endif
+
+ifdef MODULE_IPP
+satabs.dir: ipp.dir
+endif
+
+ifdef MODULE_BV_REFINEMENT
+cbmc.dir: bv_refinement.dir
+endif
+
+ifdef MODULE_SATQE
+satabs.dir: satqe.dir
+all: satmc.dir
+endif
+
+ifdef MODULE_SMTLANG
+languages: smtlang.dir
+endif
+
+ifdef MODULE_CPP
+languages: cpp.dir
+endif
+
+ifdef MODULE_PHP
+languages: php.dir
+endif
+
+ifdef MODULE_CSP
+languages: csp.dir
+endif
+
+ifdef MODULE_PVS
+languages: pvs.dir
+endif
+
+ifdef MODULE_VERILOG
+languages: verilog.dir
+endif
+
+ifdef MODULE_VHDL
+languages: vhdl.dir
+endif
+
+ifdef MODULE_NETLIST
+languages: netlist.dir
+endif
+
+ifdef MODULE_SPECC
+languages: specc.dir
+endif
+
+ifdef MODULE_PASCAL
+languages: pascal.dir
+endif
+
+ifdef MODULE_HWCBMC
+satabs: hw-cbmc.dir
+all: hw-cbmc.dir
+endif
+
+ifdef MODULE_CEMC
+all: cemc.dir
+endif
+
+ifdef MODULE_FLOATBV
+solvers.dir: floatbv.dir
+endif
+
+$(patsubst %, %.dir, $(DIRS)):
+	## Entering $(basename $@)
+	$(MAKE) $(MAKEARGS) -C $(basename $@)
+
+clean: $(patsubst %, %_clean, $(DIRS))
+	rm -f *.o
+
+dep: $(patsubst %, %_dep, $(DIRS))
+
+$(patsubst %, %_clean, $(DIRS)):
+	if [ -e $(patsubst %_clean, %, $@)/. ] ; then \
+		$(MAKE) $(MAKEARGS) -C $(patsubst %_clean, %, $@) clean ; \
+	fi
+
+$(patsubst %, %_dep, $(DIRS)):
+	if [ -e $(patsubst %_dep, %, $@)/. ] ; then \
+		$(MAKE) $(MAKEARGS) -C $(patsubst %_dep, %, $@) dep ; \
+	fi

src/ansi-c/Makefile

@@ -0,0 +1,63 @@
+SRC = c_typecast.cpp y.tab.cpp lex.yy.cpp ansi_c_parser.cpp \
+      expr2c.cpp ansi_c_language.cpp c_sizeof.cpp c_main.cpp \
+      c_types.cpp c_final.cpp trans_unit.cpp ansi_c_typecheck.cpp \
+      c_link.cpp c_preprocess.cpp c_link_type_eq.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.cpp ansi_c_convert_type.cpp \
+      type2name.cpp cprover_library.cpp \
+      printf_formatter.cpp internal_additions.cpp \
+      ansi_c_declaration.cpp designator.cpp concatenate_strings.cpp \
+      literals/parse_float.cpp literals/unescape_string.cpp \
+      literals/convert_float_literal.cpp \
+      literals/convert_character_literal.cpp \
+      literals/convert_integer_literal.cpp \
+      literals/convert_string_literal.cpp 
+
+OBJ = $(SRC:.cpp=$(OBJEXT))
+
+INCLUDES= -I .. -I ../util
+
+include ../config.inc
+include ../common
+
+all: ansi-c$(LIBEXT) library/converter$(EXEEXT)
+
+###############################################################################
+
+y.tab.cpp: parser.y
+	$(YACC) $(YFLAGS) $$flags -pyyansi_c -d parser.y -o y.tab.cpp
+
+y.tab.h: y.tab.cpp
+	if [ -e y.tab.hpp ] ; then mv y.tab.hpp y.tab.h ; else \
+        mv y.tab.cpp.h y.tab.h ; fi
+
+lex.yy.cpp: scanner.l
+	$(LEX) -Pyyansi_c -olex.yy.cpp scanner.l
+
+# extra dependencies
+y.tab$(OBJEXT): y.tab.cpp y.tab.h
+lex.yy$(OBJEXT): y.tab.cpp lex.yy.cpp y.tab.h
+cprover_library$(OBJEXT): cprover_library.inc
+
+###############################################################################
+
+library/converter$(EXEEXT):
+	$(CXX) $(LINKFLAGS) -o $@ library/converter.cpp
+
+cprover_library.inc: library/converter library/*.c
+	cat library/*.c | library/converter > $@
+
+cprover_library.cpp: cprover_library.inc
+
+###############################################################################
+
+ansi-c$(LIBEXT): $(OBJ) 
+	$(LINKLIB)
+
+clean:
+	rm -f $(OBJ) ansi-c$(LIBEXT)
+	rm -f y.tab.h y.tab.cpp lex.yy.cpp y.tab.cpp.output y.output
+	rm -f library/converter$(EXEEXT) cprover_library.inc

src/ansi-c/README

@@ -0,0 +1,10 @@
+CodeWarrior C Compilers Reference 3.2:
+
+http://cache.freescale.com/files/soft_dev_tools/doc/ref_manual/CCOMPILERRM.pdf
+
+http://cache.freescale.com/files/soft_dev_tools/doc/ref_manual/ASMX86RM.pdf
+
+ARM 4.1 Compiler Reference:
+
+http://infocenter.arm.com/help/topic/com.arm.doc.dui0491c/DUI0491C_arm_compiler_reference.pdf
+