95eae591bf
CMake support is no longer experimental
2018-08-23 17:29:02 +01:00
2e9bcb4491
Update compilation and development docs
2018-08-21 16:37:29 +01:00
dbd6988d67
Merge pull request #2750 from johnnonweiler/documentation-structure
...
Improve developer documentation structure
2018-08-21 02:36:08 +02:00
24cbfc63ed
Merge pull request #2765 from diffblue/jar_pool
...
factor out jar pool class
2018-08-20 19:15:00 +01:00
76dbb2a1d0
Remove links to classes from high level overview
2018-08-20 17:34:55 +01:00
384f0d44da
use jar_poolt in java_class_loadert
2018-08-20 12:58:20 +01:00
d601a44114
factor out pool for JARs into jar_poolt
2018-08-20 12:58:19 +01:00
4dddd0cd32
Merge pull request #2760 from diffblue/jar_pool_cleanup
...
java_class_loadert: remove unused parameter
2018-08-20 12:23:24 +01:00
dbc95f8e7d
java_class_loadert: remove unused parameter
2018-08-20 11:45:03 +01:00
8640288662
Merge pull request #2698 from diffblue/clang-builtins
...
two further clang builtins
2018-08-18 09:01:48 +01:00
4ffc2a475e
Merge pull request #2744 from danpoe/feature/invariants-with-diagnostic-information
...
Invariant macros with diagnostic information
2018-08-17 14:14:41 +01:00
d0be38551b
Merge pull request #2619 from JohnDumbell/jd/bugfix/java_annotation_array_fix
...
Parse java arrays in annotations properly
2018-08-17 13:56:36 +01:00
ac6c7d4ed9
Parse java arrays in annotations properly
...
Previously the value from the arrays was being parsed correctly but into an object which was then immediately thrown away, so the value was never really used.
2018-08-17 12:56:30 +01:00
cb090bf26a
add clang's __builtin_ia32_undefX and __builtin_nontemporal_store and __builtin_nontemporal_load
2018-08-17 12:48:52 +01:00
1ad6b5d926
Merge pull request #2754 from antlechner/antonia/ci-lazy-loading-rec-clinit
...
Fix lazy loading of enum static initializers
2018-08-17 11:19:32 +01:00
03bdf37bae
Merge pull request #2755 from diffblue/COMPILING-again
...
Update compilation instructions
2018-08-17 10:28:42 +01:00
df0605e64d
Add test for enum field of argument type
2018-08-17 09:08:04 +01:00
ad1b1d8ff9
Red Hat and Fedora now use dnf instead of yum
2018-08-17 08:58:08 +01:00
c1ef758e5f
jbmc build now uses Maven, not unzip
2018-08-17 08:57:44 +01:00
aa1de8447c
implement clang's builtin_convertvector
2018-08-17 08:50:18 +01:00
49089b1fde
Fix lazy loading of enum static initializers
...
Rather than calling clinit_wrapper on every parameter to the entry
method that is an enum, we should first load all the classes that may
be needed before we enter the entry method, and then call
clinit_wrapper on all of those which are enums. For example, the case of
an enum field of an argument to the entry method would have previously
hit an invariant violation.
2018-08-17 00:22:48 +01:00
e1fc49facb
Merge pull request #2720 from tautschnig/replace_symbol-cleanup1
...
replace_symbolt: hide {expr,type}_map
2018-08-16 20:38:36 +01:00
e327ef2b1a
replace_symbolt: hide {expr,type}_map
...
Values should only be added via insert. Add expr_map access functions as some
code still does access the expr_map.
2018-08-16 18:08:26 +00:00
3f487c3e97
Merge pull request #2724 from tautschnig/replace-symbolt-unit-test
...
Unit test of replace_symbolt
2018-08-16 19:07:36 +01:00
c55d032395
Unit test of replace_symbolt
2018-08-16 16:05:05 +00:00
544671e765
Move 'Flattening' section in solvers/README.md
2018-08-16 15:11:20 +01:00
794ba031f4
Change heading in java-bytecode docs
2018-08-16 15:05:30 +01:00
1e2fda3e5d
Workaround for Visual Studio not expanding __VA_ARGS__ on macro invocation
2018-08-16 15:01:14 +01:00
f2f2156c72
Tests for invariant macros with diagnostic output
2018-08-16 14:56:15 +01:00
8a37a2dd73
Invariant macros with diagnostic information
...
This overloads the invariant macros to take an additional optional argument to
include diagnostic information. This can e.g. be useful when debugging an
invariant violation without having access to the goto binary on which cbmc was
run on. For example, one can now do both of
DATA_INVARIANT(expr.operands().size() == 2, "binary expression")
DATA_INVARIANT(expr.operands().size() == 2, "binary expression", expr.pretty())
2018-08-16 14:56:15 +01:00
bcb7c76e6c
Merge pull request #2747 from diffblue/cleanup-message-handler
...
Cleanup message handler
2018-08-16 14:21:17 +01:00
0d8ea2c8c9
remove sequence number from message_handler interface
2018-08-16 13:11:37 +01:00
4557374a85
use size_t for message counts
2018-08-16 13:11:37 +01:00
ccf3c501bd
Add outline to module docs
2018-08-16 12:05:59 +01:00
0b7c4fb6f1
Add sections to java_bytecode/README.md
2018-08-16 10:55:12 +01:00
85a81ea263
Merge pull request #2594 from thk123/array_type_check
...
Introduce can_cast_type for array_typet
2018-08-16 10:29:39 +01:00
2becafd272
Merge pull request #2738 from diffblue/remove-memory-models
...
remove memory-models
2018-08-16 09:59:50 +01:00
c2825efae2
Merge pull request #2741 from diffblue/remove_asm_function_id
...
properly set function id on instructions added by remove_asm
2018-08-16 09:59:37 +01:00
aa7b89f7d0
Merge pull request #2742 from diffblue/symbol_type_fix
...
two further instances of symbol_type
2018-08-16 09:59:10 +01:00
1f06cde8a6
Merge pull request #2743 from tautschnig/boolbv-width
...
Fix boolbv_widtht::get_entry and fail for unknown types
2018-08-15 18:53:25 +01:00
ba57a14e1a
remove memory-models
2018-08-15 18:48:24 +01:00
4e950606d3
Merge pull request #2739 from diffblue/remove-clobber
...
remove clobber
2018-08-15 17:58:37 +01:00
066107590d
Delete one word ('testing')
2018-08-15 17:23:50 +01:00
d6755b003c
Move solvers API description to solvers module
2018-08-15 17:11:10 +01:00
f7bcd0a990
Move java_bytecode explanations to module doc
2018-08-15 16:59:42 +01:00
ccaa87cef8
Move examples from code-walkthrough to linked module
2018-08-15 16:44:17 +01:00
d33628e854
Fix boolbv_widtht::get_entry and fail for unknown types
...
It was missing the ID_symbol -> ID_symbol_type change. To guard for future bugs
of this kind, add a catch-all "UNIMPLEMENTED" as final branch.
2018-08-15 14:56:28 +00:00
4f5e14883c
Merge pull request #2713 from thk123/dump/expr2c-configuration
...
Configurable expr2c
2018-08-15 13:44:29 +01:00
01b7418ca6
Merge pull request #2710 from thomasspriggs/tas/struct_component
...
Add support for getting components by name to `struct_exprt`
2018-08-15 12:36:12 +01:00
a1d59d28fc
remove clobber
2018-08-15 12:26:28 +01:00
Owen Jones