29542059e6
aggressive slicer regression tests
2018-07-24 10:48:03 +02:00
c98c9df24d
Merge branch 'develop' into cbmc_trace_options
2018-07-23 10:35:19 +02:00
8edc5ee762
C front-end: constant folding for floating-point
2018-07-18 08:04:38 +01:00
bb7ea783cd
Merge pull request #2528 from tautschnig/dev-null
...
goto-gcc: run original compiler even when output is /dev/null
2018-07-17 12:29:04 +01:00
8966f0986e
Merge pull request #2560 from tautschnig/force-inline
...
Support Visual Studio's __forceinline
2018-07-17 10:43:19 +01:00
15f44c7662
Revert "Mark tests which fail due to invariant violations"
...
This reverts commit d423c65705
2018-07-09 18:14:12 +01:00
ea9dc15f36
goto-gcc: run original compiler even when output is /dev/null
2018-07-09 18:05:23 +01:00
754b36d6d0
Accept more mismatching function definition/declaration pairs
...
As long as the bit-width of parameters matches, we should be able to obtain sane
results. Xen does this sort of type conversion.
2018-07-09 09:33:05 +01:00
36d13f7e7e
Support Visual Studio's __forceinline
...
It was previously treated the same as inline/__inline, but Windows header files
come with multiple implementations of functions defined in the same file, with
an expected behaviour similar to "extern inline" in GCC.
2018-07-08 22:53:46 +01:00
c6f92318e9
Merge pull request #2553 from tautschnig/always-inline-partial-revert
...
Partial revert of #1898 (always_inline support, second attempt)
2018-07-08 08:12:36 +01:00
61a6acd787
Name resolution may require further template instantiation
2018-07-07 13:30:50 +01:00
4c6cfc03ef
Merge pull request #2448 from tautschnig/c++-delayed-body
...
Fix delayed method body conversion for templates
2018-07-07 12:37:00 +01:00
425db26d63
Merge pull request #2530 from tautschnig/debian3
...
Fix tests that are only correct on little-endian architectures
2018-07-07 11:42:43 +01:00
e501317b53
Additional regression tests for always_inline
...
The previous attempt of implementing support for always_inline broke each of
those in different ways.
2018-07-07 10:02:57 +00:00
016ad92b3d
Revert "Fully interpret __attribute__((always_inline))"
...
This partly reverts commit 9c93f59593
2018-07-07 09:56:19 +00:00
ee9444f9be
Merge pull request #2532 from tautschnig/debian2
...
Regression test should succeed even if char is an unsigned type
2018-07-07 10:44:35 +01:00
26803f7ee4
Test only works with simplification enabled
...
... and simplification is only performed for byte_extract_little_endian.
2018-07-07 07:08:52 +01:00
cd6127a3e6
Regression test should succeed even if char is an unsigned type
2018-07-07 07:04:12 +01:00
dab6a6e18a
Fix tests that are only correct on little-endian architectures
2018-07-07 06:39:01 +01:00
6409eae64f
Merge pull request #2449 from tautschnig/c++-template-cleanup
...
Clean up unused template instantiation symbols
2018-07-06 10:14:52 +01:00
180e066993
add option to show code in CBMC trace
2018-07-06 08:07:57 +02:00
4fbc10da0f
Add option to show function calls and returns in CBMC trace
2018-07-06 08:07:57 +02:00
f532b4bd6f
allow unsigned long instead of unsigned in regression test for hex_trace
2018-07-06 08:07:57 +02:00
94cacc66d9
represent numerical values in CBMC trace in hex
2018-07-06 08:07:57 +02:00
a354513634
Merge pull request #2510 from polgreen/hex_trace
...
represent numerical values in CBMC trace in hex
2018-07-05 16:22:11 +01:00
a018652885
allow unsigned long instead of unsigned in regression test for hex_trace
2018-07-05 10:42:28 +02:00
d5bbdd8af0
represent numerical values in CBMC trace in hex
2018-07-05 10:42:28 +02:00
19bddce081
Do not ignore --full-slice
2018-07-04 21:02:28 +01:00
0c20014e56
Merge pull request #2513 from tautschnig/clean
...
Regression test clean target and test.pl fix
2018-07-03 12:55:40 +01:00
2be11f37c4
Make "clean" target in regression tests do full cleanup
2018-07-03 10:56:05 +00:00
97e9314c91
Do not hardcode tests.log as option -s <suffix> may be in use
...
With -s <suffix> the output log file is actually tests-<suffix>.log.
2018-07-03 10:56:05 +00:00
15d430732d
Evaluate expressions that delimit GCC switch/case ranges
...
Type casts may reasonably occur in here (and maybe also other expressions that
evaluate to constants). The regression test addionally covers the case of enum
values being used, which works fine (even without this change).
2018-07-03 10:26:23 +00:00
34bd58f3e9
Clean up unused template instantiation symbols
2018-06-25 00:11:02 +00:00
02e38408e1
Fix delayed method body conversion for templates
...
Do not add method body on declaration - they are handled upon use.
2018-06-25 00:10:22 +00:00
ee2421a6fc
Test passes
...
Some prior fix to the C++ front-end has addressed this.
2018-06-24 23:41:52 +00:00
0cf27c611d
type_traits requires C++ 11
2018-06-24 23:41:52 +00:00
9fd3434c96
Use local-safe-pointers analysis to improve Symex pointer resolution
...
This uses local_safe_pointerst to determine when symex dereferences a pointer
that cannot be null. When it does the null result is excluded from the possible
values, and therefore a $invalid_object reference may be excluded from the result
of dereferencing such a pointer. This can improve constant propagation.
2018-06-24 17:39:50 +01:00
8078569175
Add local-safe-pointers analysis
...
This approaches the safe-pointers problem from the opposite direction compared to local-
bitvector-analysis -- local-bitvector tries to establish a pointer is safe because it
definitely points to known object, whereas local-safe-pointers tries to establish a
particular usage is certainly safe because it is trivially dominated by a not-null test,
which at present means a conditional GOTO or an ASSUME.
2018-06-24 17:39:50 +01:00
c0dd633854
Merge pull request #2376 from diffblue/gcc_attributes5_KNOWNBUG
...
gcc/clang treat __attribute__((aligned())) differently
2018-06-21 12:56:00 +01:00
3423e44fd3
gcc/clang treat __attribute__((aligned())) differently
...
The change of the given alignment from 8 to 16 prevents spurious passing,
since 16 is not the default alignment on any platform.
2018-06-21 12:54:37 +01:00
ac02bbc0d0
Merge pull request #2243 from diffblue/no-warning-ptr-array
...
ignore size of arrays on ptr-to-array conversions
2018-06-20 22:20:17 +01:00
b603a6374f
make test independent of index type
2018-06-20 17:05:45 +01:00
f7cd161c6c
Merge pull request #2371 from diffblue/fix-tests2
...
make test independent of index type
2018-06-20 14:39:49 +01:00
82753bc70f
make test independent of index type
2018-06-20 12:46:30 +01:00
f5f32da572
Merge pull request #2364 from smowton/smowton/fix/autodetect-default-cxx-dialect
...
C/C++ frontends: select standard using the same rules as the compiler we emulate
2018-06-20 12:30:36 +01:00
d46a55c3e3
Add new goto-instrument option print-global-state-size
2018-06-20 09:38:30 +01:00
5ca741056d
ignore size of arrays on ptr-to-array conversions
2018-06-19 22:22:59 +01:00
bcc3bef4a4
make regression/cbmc/bounds_check1 independent of types used
2018-06-19 20:51:32 +01:00
4de45388fa
switch regression/cbmc/Typecast2 to preprocessed code
...
This avoids the need for a cross-compiler to 64 bit when run on a 32-bit
system.
2018-06-19 20:51:14 +01:00
91a9c646af
Amend two tests that explicitly target C++98
...
These were previously broken on g++-6 and above, as the compiler defaults to C++14 mode.
2018-06-19 17:22:20 +01:00
Polgreen