Skip to content

Commit 75331b6

Browse files
author
klaas
committed
Merge resolved.
2 parents a7545c4 + 2bea6fc commit 75331b6

File tree

189 files changed

+3675
-291
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

189 files changed

+3675
-291
lines changed

‎.travis.yml

Lines changed: 22 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -46,17 +46,35 @@ jobs:
4646
before_cache:
4747

4848
- stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test
49-
env: NAME="DOXYGEN-CHECK"
49+
env:
50+
NAME: "DOXYGEN-CHECK"
51+
DOXYGEN_VERSION: "1.8.14"
5052
addons:
5153
apt:
5254
sources:
5355
- sourceline: 'deb http://packages.cloud.google.com/apt cloud-sdk-trusty main'
5456
key_url: 'https://packages.cloud.google.com/apt/doc/apt-key.gpg'
5557
packages:
56-
- doxygen
58+
- cmake
5759
- google-cloud-sdk
60+
cache:
61+
directories:
62+
- ${TRAVIS_BUILD_DIR}/doxygen/build/bin
5863
install:
59-
script: scripts/travis_doxygen.sh
64+
- |
65+
# Build doxygen if it is not in Travis cache
66+
if ! [ -x doxygen/build/bin/doxygen ]
67+
then
68+
mkdir -p doxygen/build \
69+
&& wget http://ftp.stack.nl/pub/users/dimitri/doxygen-${DOXYGEN_VERSION}.src.tar.gz -O- | tar -xz --strip-components=1 --directory doxygen \
70+
&& ( cd doxygen/build && cmake .. ) \
71+
&& make -j4 -C doxygen/build
72+
fi
73+
- export PATH="$PATH:${TRAVIS_BUILD_DIR}/doxygen/build/bin"
74+
script:
75+
- echo $PATH
76+
- doxygen --version
77+
- scripts/travis_doxygen.sh
6078
before_cache:
6179
after_success:
6280
# Google Cloud Integration
@@ -288,6 +306,7 @@ notifications:
288306
webhooks:
289307
urls:
290308
- http://dashboard.diffblue.com/api/travis-webhooks
309+
- https://us-central1-dev-user-joelallred.cloudfunctions.net/trigger-testgen-from-cbmc
291310
on_success: always
292311
on_failure: always
293312
on_start: never

‎appveyor.yml

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ install:
4242
& 7z x minisat2_2.2.1.orig.tar.gz
4343
&7z x minisat2_2.2.1.orig.tar
4444
}
45-
if (!(Test-Path jml)) {
45+
if (!(Test-Path java-models-library-master\.gitignore)) {
4646
& appveyor downloadfile https://github.com/diffblue/java-models-library/archive/master.zip -FileName jml.zip
4747
& 7z x jml.zip
4848
}
@@ -74,6 +74,7 @@ test_script:
7474
rmdir /s /q ansi-c\Universal_characters1
7575
rmdir /s /q ansi-c\function_return1
7676
rmdir /s /q ansi-c\gcc_attributes7
77+
rmdir /s /q ansi-c\gcc_version1
7778
rmdir /s /q ansi-c\struct6
7879
rmdir /s /q ansi-c\struct7
7980
rmdir /s /q cbmc\Malloc23
@@ -89,6 +90,9 @@ test_script:
8990
rmdir /s /q cpp\Decltype1
9091
rmdir /s /q cpp\Decltype2
9192
rmdir /s /q cpp\Function_Overloading1
93+
rmdir /s /q cpp\Resolver10
94+
rmdir /s /q cpp\Resolver11
95+
rmdir /s /q cpp\Template_Parameters1
9296
rmdir /s /q cpp\enum2
9397
rmdir /s /q cpp\enum7
9498
rmdir /s /q cpp\enum8

‎jbmc/regression/jdiff/java-clinit-wrapper/new.jar

79 KB
Binary file not shown.

‎jbmc/regression/jdiff/java-clinit-wrapper/old.jar

79.2 KB
Binary file not shown.

‎jbmc/regression/jdiff/java-clinit-wrapper/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
new.jar
3+
old.jar
4+
EXIT=0
5+
SIGNAL=0
6+
--
7+
java::java\.nio\.charset\.StandardCharsets::clinit_wrapper$
8+
java::org\.apache\.tika\.mime\.MediaType::clinit_wrapper$

‎jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -760,15 +760,12 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
760760

761761
const irep_idt clone_name=
762762
id2string(symbol_type_identifier)+".clone:()Ljava/lang/Object;";
763-
code_typet clone_type;
764-
clone_type.return_type()=
765-
java_reference_type(symbol_typet("java::java.lang.Object"));
766763
code_typet::parametert this_param;
767764
this_param.set_identifier(id2string(clone_name)+"::this");
768765
this_param.set_base_name("this");
769766
this_param.set_this();
770767
this_param.type()=java_reference_type(symbol_type);
771-
clone_type.parameters().push_back(this_param);
768+
code_typet clone_type({this_param}, java_lang_object_type());
772769

773770
parameter_symbolt this_symbol;
774771
this_symbol.name=this_param.get_identifier();

‎jbmc/src/java_bytecode/java_entry_point.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -31,8 +31,7 @@ static void create_initialize(symbol_table_baset &symbol_table)
3131
initialize.base_name=INITIALIZE_FUNCTION;
3232
initialize.mode=ID_java;
3333

34-
code_typet type;
35-
type.return_type()=empty_typet();
34+
code_typet type({}, empty_typet());
3635
initialize.type=type;
3736

3837
code_blockt init_code;
@@ -688,8 +687,7 @@ bool generate_java_start_function(
688687
// we just built and register it in the symbol table
689688
symbolt new_symbol;
690689

691-
code_typet main_type;
692-
main_type.return_type()=empty_typet();
690+
code_typet main_type({}, empty_typet());
693691

694692
new_symbol.name=goto_functionst::entry_point();
695693
new_symbol.type.swap(main_type);

‎jbmc/src/java_bytecode/java_static_initializers.cpp

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -293,11 +293,7 @@ static void create_clinit_wrapper_symbols(
293293

294294
// Create symbol for the "clinit_wrapper"
295295
symbolt wrapper_method_symbol;
296-
code_typet wrapper_method_type;
297-
wrapper_method_type.return_type() = void_typet();
298-
// Ensure the parameters property is there
299-
// to avoid trouble in irept comparisons
300-
wrapper_method_type.parameters();
296+
code_typet wrapper_method_type({}, void_typet());
301297
wrapper_method_symbol.name = clinit_wrapper_name(class_name);
302298
wrapper_method_symbol.pretty_name = wrapper_method_symbol.name;
303299
wrapper_method_symbol.base_name = "clinit_wrapper";
@@ -717,8 +713,7 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
717713
"a class cannot be both incomplete, and so have stub static fields, and "
718714
"also define a static initializer");
719715

720-
code_typet thunk_type;
721-
thunk_type.return_type() = void_typet();
716+
code_typet thunk_type({}, void_typet());
722717

723718
symbolt static_init_symbol;
724719
static_init_symbol.name = static_init_name;

‎jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1611,9 +1611,7 @@ codet java_string_library_preprocesst::make_object_get_class_code(
16111611
"java::java.lang.Class.forName:(Ljava/lang/String;)Ljava/lang/Class;");
16121612
fun_call.lhs()=class1;
16131613
fun_call.arguments().push_back(string1);
1614-
code_typet fun_type;
1615-
fun_type.parameters().push_back(code_typet::parametert(string_ptr_type));
1616-
fun_type.return_type()=class_type;
1614+
code_typet fun_type({code_typet::parametert(string_ptr_type)}, class_type);
16171615
fun_call.function().type()=fun_type;
16181616
code.add(fun_call, loc);
16191617

‎jbmc/src/java_bytecode/java_types.cpp

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -493,24 +493,21 @@ typet java_type_from_string(
493493
if(e_pos==std::string::npos)
494494
return nil_typet();
495495

496-
code_typet result;
497-
498-
result.return_type()=
499-
java_type_from_string(
500-
std::string(src, e_pos+1, std::string::npos),
501-
class_name_prefix);
496+
typet return_type = java_type_from_string(
497+
std::string(src, e_pos + 1, std::string::npos), class_name_prefix);
502498

503499
std::vector<typet> param_types =
504500
parse_list_types(src.substr(0, e_pos + 1), class_name_prefix, '(', ')');
505501

506502
// create parameters for each type
503+
code_typet::parameterst parameters;
507504
std::transform(
508505
param_types.begin(),
509506
param_types.end(),
510-
std::back_inserter(result.parameters()),
507+
std::back_inserter(parameters),
511508
[](const typet &type) { return code_typet::parametert(type); });
512509

513-
return result;
510+
return code_typet(std::move(parameters), std::move(return_type));
514511
}
515512

516513
case '[': // array type

‎jbmc/unit/java-testing-utils/module_dependencies.txt

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
goto-programs
2+
java_bytecode
3+
java-testing-utils
4+
langapi # should go away
5+
testing-utils
6+
util

‎jbmc/unit/java_bytecode/ci_lazy_methods/module_dependencies.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
ci_lazy_methods
2+
java-testing-utils
3+
testing-utils

‎jbmc/unit/java_bytecode/goto-programs/module_dependencies.txt

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
goto-programs
2+
java-testing-utils
3+
testing-utils
4+
util

‎jbmc/unit/java_bytecode/goto_program_generics/module_dependencies.txt

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
goto_program_generics
2+
java-testing-utils
3+
testing-utils
4+
util

‎jbmc/unit/java_bytecode/inherited_static_fields/module_dependencies.txt

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
inherited_static_fields
2+
java-testing-utils
3+
testing-utils
4+
util

‎jbmc/unit/java_bytecode/java_bytecode_convert_class/module_dependencies.txt

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
11
java-testing-utils
22
testing-utils
33
java_bytecode
4+
util

‎jbmc/unit/java_bytecode/java_bytecode_convert_method/module_dependencies.txt

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
goto-programs
2+
java_bytecode
3+
java_bytecode_convert_method
4+
java-testing-utils
5+
testing-utils
6+
util

‎jbmc/unit/java_bytecode/java_bytecode_parse_generics/module_dependencies.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
java_bytecode_parse_generics
2+
java-testing-utils
3+
testing-utils

‎jbmc/unit/java_bytecode/java_bytecode_parse_lambdas/module_dependencies.txt

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
java_bytecode
2+
java_bytecode_parse_lambdas
3+
java-testing-utils
4+
langapi # should go away
5+
testing-utils
6+
util

‎jbmc/unit/java_bytecode/java_object_factory/module_dependencies.txt

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
java_bytecode
2+
java_object_factory
3+
langapi # should go away
4+
testing-utils
5+
util

‎jbmc/unit/java_bytecode/java_replace_nondet/module_dependencies.txt

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
goto-instrument
2+
goto-programs
3+
java_bytecode
4+
java_replace_nondet
5+
java-testing-utils
6+
testing-utils
7+
util

‎jbmc/unit/java_bytecode/java_string_library_preprocess/module_dependencies.txt

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
java_bytecode
2+
java_string_library_preprocess
3+
langapi # should go away
4+
testing-utils
5+
util

‎jbmc/unit/java_bytecode/java_types/module_dependencies.txt

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
java_bytecode
2+
java_types
3+
testing-utils

‎jbmc/unit/java_bytecode/java_virtual_functions/module_dependencies.txt

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
goto-instrument
2+
goto-programs
3+
java_bytecode
4+
java_virtual_functions
5+
java-testing-utils
6+
testing-utils
7+
util

‎jbmc/unit/java_bytecode/module_dependencies.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
java_bytecode
2+
testing-utils

‎jbmc/unit/pointer-analysis/module_dependencies.txt

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
goto-programs
2+
java_bytecode
3+
langapi # should go away
4+
pointer-analysis
5+
testing-utils
6+
util

‎jbmc/unit/solvers/refinement/string_constraint_instantiation/module_dependencies.txt

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
java_bytecode
2+
langapi # should go away
3+
solvers/refinement
4+
solvers/sat
5+
string_constraint_instantiation
6+
testing-utils
7+
util

‎jbmc/unit/solvers/refinement/string_refinement/dependency_graph.cpp

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,12 @@ SCENARIO("dependency_graph", "[core][solvers][refinement][string_refinement]")
5858
const symbol_exprt lhs("lhs", unsignedbv_typet(32));
5959
const symbol_exprt lhs2("lhs2", unsignedbv_typet(32));
6060
const symbol_exprt lhs3("lhs3", unsignedbv_typet(32));
61-
code_typet fun_type;
61+
code_typet fun_type(
62+
{code_typet::parametert(length_type()),
63+
code_typet::parametert(pointer_type(java_char_type())),
64+
code_typet::parametert(string_type),
65+
code_typet::parametert(string_type)},
66+
unsignedbv_typet(32));
6267

6368
// fun1 is s3 = s1.concat(s2)
6469
function_application_exprt fun1(fun_type);

‎jbmc/unit/solvers/refinement/string_refinement/module_dependencies.txt

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
java_bytecode
2+
langapi # should go away
3+
string_refinement
4+
solvers/refinement
5+
testing-utils
6+
util

‎jbmc/unit/util/module_dependencies.txt

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
java_bytecode
2+
java-testing-utils
3+
testing-utils
4+
util

‎regression/CMakeLists.txt

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,7 @@ add_subdirectory(goto-instrument)
3030
add_subdirectory(cpp)
3131
add_subdirectory(cbmc-cover)
3232
add_subdirectory(goto-instrument-typedef)
33+
add_subdirectory(smt2_solver)
3334
add_subdirectory(strings)
3435
add_subdirectory(invariants)
3536
add_subdirectory(goto-diff)
@@ -41,4 +42,4 @@ endif()
4142
add_subdirectory(goto-cc-cbmc)
4243
add_subdirectory(cbmc-cpp)
4344
add_subdirectory(goto-cc-goto-analyzer)
44-
45+
add_subdirectory(systemc)

‎regression/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ DIRS = cbmc \
1818
goto-cc-cbmc \
1919
cbmc-cpp \
2020
goto-cc-goto-analyzer \
21+
systemc \
2122
contracts \
2223
# Empty last line
2324

‎regression/ansi-c/float_constant1/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ STATIC_ASSERT(0X.0p+1f == 0);
1212

1313
// 32-bit, 64-bit and 128-bit constants, GCC proper only,
1414
// clang doesn't have it
15-
#if defined(__GNUC__) && !defined(__clang__)
15+
#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ >= 7
1616
STATIC_ASSERT(__builtin_types_compatible_p(_Float32, __typeof(1.0f32)));
1717
STATIC_ASSERT(__builtin_types_compatible_p(_Float64, __typeof(1.0f64)));
1818
STATIC_ASSERT(__builtin_types_compatible_p(_Float128, __typeof(1.0f128)));

‎regression/ansi-c/gcc_types_compatible_p1/main.c

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -67,8 +67,8 @@ STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot) *, int *));
6767
STATIC_ASSERT(__builtin_types_compatible_p(typeof (hot), typeof (janette)));
6868
STATIC_ASSERT(__builtin_types_compatible_p(__int128, signed __int128));
6969

70-
#ifndef __clang__
7170
// clang doesn't have these
71+
#if !defined(__clang__) && __GNUC__ >= 7
7272
#if defined(__x86_64__) || defined(__i386__)
7373
STATIC_ASSERT(__builtin_types_compatible_p(__float128, _Float128));
7474
#endif
@@ -95,16 +95,19 @@ STATIC_ASSERT(!__builtin_types_compatible_p(long int, int));
9595
STATIC_ASSERT(!__builtin_types_compatible_p(long long int, long int));
9696
STATIC_ASSERT(!__builtin_types_compatible_p(unsigned, signed));
9797

98-
#ifndef __clang__
98+
STATIC_ASSERT(!__builtin_types_compatible_p(__int128, unsigned __int128));
99+
99100
// clang doesn't have these
101+
#if !defined(__clang__)
102+
#if __GNUC__ >= 7
100103
STATIC_ASSERT(!__builtin_types_compatible_p(_Float32, float));
101104
STATIC_ASSERT(!__builtin_types_compatible_p(_Float64, double));
102105
STATIC_ASSERT(!__builtin_types_compatible_p(_Float32x, float));
103106
STATIC_ASSERT(!__builtin_types_compatible_p(_Float64x, double));
107+
#endif
104108
STATIC_ASSERT(!__builtin_types_compatible_p(__float80, double));
105109
STATIC_ASSERT(!__builtin_types_compatible_p(__float128, long double));
106110
STATIC_ASSERT(!__builtin_types_compatible_p(__float128, double));
107-
STATIC_ASSERT(!__builtin_types_compatible_p(__int128, unsigned __int128));
108111
#endif
109112
#endif
110113

‎regression/ansi-c/gcc_version1/fake-gcc-4

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
#!/bin/sh
2+
3+
gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=4 -D __GNUC_MINOR__=9 -D __GNUC_PATCHLEVEL__=1 $*
4+

‎regression/ansi-c/gcc_version1/fake-gcc-7

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
#!/bin/sh
2+
3+
gcc -Wno-macro-redefined -U __clang_major__ -D __GNUC__=7 -D __GNUC_MINOR__=0 -D __GNUC_PATCHLEVEL__=0 $*
4+

‎regression/ansi-c/gcc_version1/gcc-4.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
typedef double _Float64;
2+

‎regression/ansi-c/gcc_version1/gcc-7.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
_Float64 some_var;
2+

‎regression/ansi-c/gcc_version1/test-gcc-4.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
gcc-4.c
3+
--native-compiler ./fake-gcc-4
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^CONVERSION ERROR$

0 commit comments

Comments
 (0)