replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Moved unit tests to separate directory 

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@6332 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2016-02-16 13:00:54 +00:00
parent c92bda895d
commit dc7c4e3b9b
17 changed files with 84 additions and 76 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
src/cpp/Makefile
View File

@ -28,25 +28,11 @@ INCLUDES= -I ..
include ../config.inc
include ../common
CLEANFILES = cpp$(LIBEXT) \
cpp_parser_test$(EXEEXT) cpp_scanner_test$(EXEEXT) \
cpp_parser_test$(OBJEXT) cpp_scanner_test$(OBJEXT) \
cpp_parser_test.d cpp_scanner_test.d
CLEANFILES = cpp$(LIBEXT)
all: cpp$(LIBEXT) cpp_parser_test$(EXEEXT) cpp_scanner_test$(EXEEXT)
all: cpp$(LIBEXT)
###############################################################################
cpp$(LIBEXT): $(OBJ)
$(LINKLIB)
cpp_parser_test$(EXEEXT): cpp_parser_test$(OBJEXT) $(OBJ) ../util/util$(LIBEXT) \
../ansi-c/ansi-c$(LIBEXT) ../big-int/big-int$(LIBEXT) ../linking/linking$(LIBEXT) \
../langapi/langapi$(LIBEXT)
$(LINKBIN)
cpp_scanner_test$(EXEEXT): cpp_scanner_test$(OBJEXT) $(OBJ) ../util/util$(LIBEXT) \
../ansi-c/ansi-c$(LIBEXT) ../big-int/big-int$(LIBEXT) ../linking/linking$(LIBEXT) \
../langapi/langapi$(LIBEXT)
$(LINKBIN)

19
src/goto-programs/Makefile
View File

@ -21,17 +21,7 @@ INCLUDES= -I ..
include ../config.inc
include ../common
LIBS = ../ansi-c/ansi-c$(LIBEXT) \
../cpp/cpp$(LIBEXT) \
../linking/linking$(LIBEXT) \
../util/util$(LIBEXT) \
../big-int/big-int$(LIBEXT) \
../pointer-analysis/pointer-analysis$(LIBEXT) \
../langapi/langapi$(LIBEXT) \
../assembler/assembler$(LIBEXT) \
../analyses/analyses$(LIBEXT)
CLEANFILES = goto-programs$(LIBEXT) test_wp$(EXEEXT) osx_fat_reader_test$(EXEEXT)
CLEANFILES = goto-programs$(LIBEXT)
all: goto-programs$(LIBEXT)
@ -39,10 +29,3 @@ all: goto-programs$(LIBEXT)
goto-programs$(LIBEXT): $(OBJ)
$(LINKLIB)
test_wp$(EXEEXT): test_wp$(OBJEXT) goto-programs$(LIBEXT)
$(LINKBIN)
osx_fat_reader_test$(EXEEXT): osx_fat_reader_test$(OBJEXT) goto-programs$(LIBEXT)
$(LINKBIN)

8
src/json/Makefile
View File

@ -6,10 +6,9 @@ include ../config.inc
include ../common
CLEANFILES=json$(LIBEXT) json_y.tab.h json_y.tab.cpp json_lex.yy.cpp \
json_y.tab.cpp.output json_y.output \
json_test$(EXEEXT) json_test$(OBJEXT) json_test.d
json_y.tab.cpp.output json_y.output
all: json$(LIBEXT) json_test$(EXEEXT)
all: json$(LIBEXT)
###############################################################################
@ -32,6 +31,3 @@ generated_files: json_lex.yy.cpp json_y.tab.cpp json_y.tab.h
json_y.tab$(OBJEXT): json_y.tab.cpp json_y.tab.h
json_lex.yy$(OBJEXT): json_y.tab.cpp json_lex.yy.cpp json_y.tab.h
json_test$(EXEEXT): json_test$(OBJEXT) $(OBJ) ../util/util$(LIBEXT) ../big-int/big-int$(LIBEXT)
$(LINKBIN)

11
src/solvers/Makefile
View File

@ -125,12 +125,9 @@ INCLUDES= -I .. \
$(SMVSAT_INCLUDE) $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \
$(PRECOSAT_INCLUDE) $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE)
CLEANFILES = solvers$(LIBEXT) \
smt2/smt2_parser_test$(EXEEXT) \
smt2/smt2_parser_test$(OBJEXT) \
smt2/smt2_parser_test.d \
CLEANFILES = solvers$(LIBEXT)
all: solvers$(LIBEXT) smt2/smt2_parser_test$(EXEEXT)
all: solvers$(LIBEXT)
ifneq ($(SQUOLEM2),)
CP_CXXFLAGS += -DHAVE_QBF_CORE
@ -150,7 +147,3 @@ solvers$(LIBEXT): $(OBJ) $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \
$(MINISAT2_LIB) $(SMVSAT_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \
$(PRECOSAT_LIB) $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB)
$(LINKLIB)
smt2/smt2_parser_test$(EXEEXT): smt2/smt2_parser$(OBJEXT) smt2/smt2_parser_test$(OBJEXT)
$(LINKBIN)

10
src/util/Makefile
View File

@ -25,17 +25,14 @@ SRC = arith_tools.cpp base_type.cpp cmdline.cpp config.cpp symbol_table.cpp \
INCLUDES= -I ..
LIBS = ../big-int/bigint$(OBJEXT) ../big-int/bigint-func$(OBJEXT)
include ../config.inc
include ../common
CLEANFILES = util$(LIBEXT) \
irep_ids.h irep_ids.inc \
ieee_float_test$(EXEEXT) ieee_float_test$(OBJEXT) ieee_float_test.d \
irep_ids_convert$(EXEEXT) irep_ids_convert$(OBJEXT) irep_ids_convert.d
all: util$(LIBEXT) ieee_float_test$(EXEEXT)
all: util$(LIBEXT)
###############################################################################
@ -58,8 +55,3 @@ $(OBJ): irep_ids.h
util$(LIBEXT): $(OBJ)
$(LINKLIB)
ieee_float_test$(OBJEXT): irep_ids.h
ieee_float_test$(EXEEXT): ieee_float_test$(OBJEXT) util$(LIBEXT)
$(LINKBIN)

57
unit/Makefile Normal file
View File

@ -0,0 +1,57 @@
SRC = cpp_parser.cpp cpp_scanner.cpp elf_reader.cpp float_utils.cpp \
ieee_float.cpp json.cpp miniBDD.cpp osx_fat_reader.cpp \
smt2_parser.cpp wp.cpp
INCLUDES= -I ../src/
include ../src/config.inc
include ../src/common
LIBS = ../src/ansi-c/ansi-c$(LIBEXT) \
../src/cpp/cpp$(LIBEXT) \
../src/json/json$(LIBEXT) \
../src/linking/linking$(LIBEXT) \
../src/util/util$(LIBEXT) \
../src/big-int/big-int$(LIBEXT) \
../src/goto-programs/goto-programs$(LIBEXT) \
../src/pointer-analysis/pointer-analysis$(LIBEXT) \
../src/langapi/langapi$(LIBEXT) \
../src/assembler/assembler$(LIBEXT) \
../src/analyses/analyses$(LIBEXT) \
../src/solvers/solvers$(LIBEXT) \
CLEANFILES = $(SRC:.cpp=$(EXEEXT))
all: $(SRC:.cpp=$(EXEEXT))
###############################################################################
cpp_parser$(EXEEXT): cpp_parser$(OBJEXT)
$(LINKBIN)
cpp_scanner$(EXEEXT): cpp_scanner$(OBJEXT)
$(LINKBIN)
elf_reader$(EXEEXT): elf_reader$(OBJEXT)
$(LINKBIN)
float_utils$(EXEEXT): float_utils$(OBJEXT)
$(LINKBIN)
ieee_float$(EXEEXT): ieee_float$(OBJEXT)
$(LINKBIN)
json$(EXEEXT): json$(OBJEXT)
$(LINKBIN)
miniBDD$(EXEEXT): miniBDD$(OBJEXT)
$(LINKBIN)
osx_fat_reader$(EXEEXT): osx_fat_reader$(OBJEXT)
$(LINKBIN)
smt2_parser$(EXEEXT): smt2_parser$(OBJEXT)
$(LINKBIN)
wp$(EXEEXT): wp$(OBJEXT)
$(LINKBIN)

4
src/cpp/cpp_parser_test.cpp → unit/cpp_parser.cpp
View File

@ -2,7 +2,7 @@
#include <util/config.h>
#include "cpp_parser.h"
#include <cpp/cpp_parser.h>
/*******************************************************************\
@ -26,5 +26,7 @@ int main(int argc, const char *argv[])
cpp_parser.in=&in;
cpp_parser.parse();
return 0;
}

6
src/cpp/cpp_scanner_test.cpp → unit/cpp_scanner.cpp
View File

@ -4,8 +4,8 @@
#include <util/config.h>
#include <ansi-c/ansi_c_parser.h>
#include "cpp_parser.h"
#include "cpp_token_buffer.h"
#include <cpp/cpp_parser.h>
#include <cpp/cpp_token_buffer.h>
/*******************************************************************\
@ -39,5 +39,7 @@ int main(int argc, const char *argv[])
while(cpp_parser.token_buffer.get_token(tk))
std::cout << tk.text << '\n';
return 0;
}

2
src/goto-programs/elf_reader_test.cpp → unit/elf_reader.cpp
View File

@ -1,7 +1,7 @@
#include <iostream>
#include <fstream>
#include "elf_reader.h"
#include <goto-programs/elf_reader.h>
int main(int argc, char **argv)
{

2
src/solvers/floatbv/float_utils_test.cpp → unit/float_utils.cpp
View File

@ -1,7 +1,7 @@
#include <iostream>
#include <solvers/sat/satcheck.h>
#include "float_utils.h"
#include <solvers/floatbv/float_utils.h>
float random_float()
{

4
src/util/ieee_float_test.cpp → unit/ieee_float.cpp
View File

@ -11,7 +11,7 @@
#define nextafterf(a, b) (throw "no nextafterf", 0);
#endif
#include "ieee_float.h"
#include <util/ieee_float.h>
#define PINF (std::numeric_limits<float>::infinity())
#define NINF (-std::numeric_limits<float>::infinity())
@ -294,7 +294,7 @@ int main()
srand(time(0));
check_minmax();
for(unsigned i=0; i<100000000; i++)
for(unsigned i=0; i<100000; i++)
{
if(i%10000==0) std::cout << "*********** " << i << std::endl;
check_arithmetic(i);

2
src/json/json_test.cpp → unit/json.cpp
View File

@ -2,7 +2,7 @@
#include <util/cout_message.h>
#include "json_parser.h"
#include <json/json_parser.h>
int yyjsonlex();
extern char *yyjsontext;

9
src/solvers/miniBDD/test_miniBDD.cpp → unit/miniBDD.cpp
View File

@ -1,6 +1,6 @@
#include <iostream>
#include "miniBDD.h"
#include <solvers/miniBDD/miniBDD.h>
using namespace miniBDD;
@ -50,18 +50,16 @@ void test3()
//mgr.DumpTable(std::cout);
}
#if 0
#include <langapi/language_util.h>
#include <langapi/mode.h>
#include <ansi-c/ansi_c_language.h>
// link against
// ../langapi/langapi$(LIBEXT) ../ansi-c/ansi-c$(LIBEXT) ../linking/linking$(LIBEXT)
#include <util/std_expr.h>
#include <util/symbol_table.h>
#include <util/namespace.h>
#include <solvers/prop/bdd_expr.h>
void test4()
{
register_language(new_ansi_c_language);
@ -81,7 +79,6 @@ void test4()
std::cout << from_expr(ns, "", t.as_expr()) << std::endl;
}
#endif
int main()
{

2
src/goto-programs/osx_fat_reader_test.cpp → unit/osx_fat_reader.cpp
View File

@ -1,6 +1,6 @@
#include <iostream>
#include "osx_fat_reader.h"
#include <goto-programs/osx_fat_reader.h>
int main(int argc, char **argv)
{

2
src/solvers/smt2/smt2_parser_test.cpp → unit/smt2_parser.cpp
View File

@ -4,7 +4,7 @@
#include <iostream>
#include "smt2_parser.h"
#include <solvers/smt2/smt2_parser.h>
/*******************************************************************\

4
src/goto-programs/test_wp.cpp → unit/wp.cpp
View File

@ -10,8 +10,8 @@
#include <ansi-c/ansi_c_language.h>
#include <ansi-c/expr2c.h>
#include "goto_convert_functions.h"
#include "wp.h"
#include <goto-programs/goto_convert_functions.h>
#include <goto-programs/wp.h>
int main(int argc, const char **argv)
{

0
src/goto-programs/test_wp_in1.c → unit/wp_in1.c
View File