5e5bbca1d2
Correctly align description of option
2017-03-23 18:56:05 +00:00
a35731baa6
Remove -show-reachable-properties
...
The same effect can now be achieved by
--show-properties --drop-unused-functions
2017-03-23 18:56:05 +00:00
e8ec160168
Add --drop-unused-functions option
...
The default behaviour of CBMC for the options --show-goto-functions,
--show-properties and --cover is to consider all functions. This
is particularly annoying for --cover where coverage goals are
reported from functions that are trivially unreachable from the entry point.
Also, --show-reachable-properties has been introduced in the past
to hide such properties.
We could change the default behaviour to slicing away everything
that is trivially unreachable from the entry point. However, this would
require an extra option to be able to view all functions and properties.
This commit preserves the default behaviour and enables focussing
the output of --show-goto-functions --show-properties and --cover
on functions that are not trivially unreachable using --drop-unused-functions.
2017-03-23 18:56:00 +00:00
6edd2b3c58
Merge pull request #637 from NathanJPhillips/bugfix/file_util
...
delete_directory fails silently if it contains subfolders
2017-03-21 17:56:08 +00:00
d4d44db701
Merge pull request #648 from NathanJPhillips/bugfix/lint-work-across-repos
...
Bugfix/lint infrastructure improvements
2017-03-21 15:04:02 +00:00
36dee831ad
Check that filter_lint_by_diff.py exists
2017-03-21 14:09:44 +00:00
6bba4ab110
Work across repos
...
Use the path of the containing repository of the current path, not the one the script is downloaded into
2017-03-21 14:09:26 +00:00
5fef8411b1
Work with submodules
...
Made linter use paths relative to current submodule, not the lowest containing repository
2017-03-21 14:07:56 +00:00
9cd9843d36
Comment in lint filter
2017-03-21 14:07:56 +00:00
88816e9998
Ignore stdout, only pass errors to filter script
2017-03-21 14:05:48 +00:00
d110db0cb1
Version to work on Windows
2017-03-21 12:29:33 +00:00
b63228c675
delete_directory fails silently on subfolders
2017-03-21 10:22:21 +00:00
a7663cb997
increased version number to 5.7
2017-03-19 17:18:34 +00:00
7b8a4e651b
Merge pull request #654 from danpoe/inlining-no-caching
...
Option to disable caching for inlining
2017-03-19 15:25:37 +00:00
0f0ab68e31
progress output
2017-03-19 13:32:47 +00:00
775bbef2ad
new option --no-caching for use with inlining to disable caching of intermediate results
2017-03-19 13:32:47 +00:00
7a8961e0d0
avoid a warning
2017-03-19 11:28:49 +00:00
f04d40a299
removed dependency on linking module
2017-03-19 11:17:09 +00:00
d03aa42d0a
re-added missing inline keywords
2017-03-19 11:16:46 +00:00
f9689685ca
convenient zero factories for floating point and fixed point types
2017-03-19 11:10:15 +00:00
4b1b62729a
we don't use libzip any more
2017-03-19 10:16:31 +00:00
30c63df49d
Merge branch 'master' of github.com:diffblue/cbmc
2017-03-18 22:13:13 +00:00
f0824193a8
compilation instructions
2017-03-18 22:13:05 +00:00
6bbe8313ca
make tests pass on 32-bit systems
2017-03-18 21:20:45 +00:00
1ca2b70d36
make tests pass on 32-bit systems
2017-03-18 21:13:08 +00:00
09091152ac
Merge pull request #653 from danpoe/sharing-map
...
Map with sharing
2017-03-18 19:59:33 +00:00
e0905ae3f0
map with sharing
2017-03-18 19:13:48 +00:00
1215d7f7f5
Merge pull request #487 from danpoe/dependence-graph-dominator-use-fix
...
Dependency graph fix to compute dominators per function
2017-03-18 16:02:30 +00:00
88b87d37e4
Merge pull request #527 from martin-cs/pointer-analysis-tidy
...
Pointer analysis tidy
2017-03-18 15:59:48 +00:00
4da4b1fa16
Merge pull request #650 from thk123/bugfix/missing-include
...
Missing forward declaration
2017-03-18 15:58:26 +00:00
60d0782363
Missing forward declaration
...
This caused this to not compile if included before whatever brings in
goto_modelt.
2017-03-16 17:21:18 +00:00
fee04d637d
Merge pull request #644 from thk123/bugfix/lint-non-ascii-crash
...
Fixed crash on non-ascii diff
2017-03-15 18:18:41 +00:00
835277b01a
Fixed crash on non-ascii diff
...
Sometimes the diff file would contain a unicode character. Since we were
opening the file, this meant that unidiff was reading the file in the
wrong format. By letting unidiff handle reading the file we slightly
simplify the code and fix this problem.
2017-03-15 16:27:25 +00:00
409f97ecaf
Merge pull request #630 from lucasccordeiro/fix-full-slice-01
...
Fixed test cases slice02 and slice14 from goto-instrument regression
2017-03-15 14:43:00 +00:00
415c324d0d
Merge pull request #578 from cristina-david/tag-exceptional-return-as-output
...
Tag exceptional return as output
2017-03-15 14:42:38 +00:00
1cea18f731
Merge pull request #627 from NathanJPhillips/cleanup/minor
...
Minor cleanups
2017-03-15 14:42:12 +00:00
7d5a610497
Merge pull request #599 from smowton/sss_infix
...
Add string-infix utility
2017-03-15 14:40:40 +00:00
c1d8ff3c0e
Merge pull request #638 from mgudemann/bugfix/load_java_lang_class
...
adds java.lang.Class to load queue
2017-03-15 14:39:27 +00:00
0e1b194fe9
Merge pull request #523 from smowton/factor_fresh_symbol
...
Factor out fresh symbol generation
2017-03-15 14:38:43 +00:00
92d589afe7
Tag the exceptional return of the entry function as output
2017-03-15 11:17:14 +00:00
1a88570e18
adds java.lang.Class to load queue
...
java.lang.Class can be used without explicit reference (cf. regression test
classtest1), therefore it has to be added explicitly to the loading queue.
2017-03-15 09:23:54 +01:00
1855bcddf7
Comment on potential gotcha
...
Added comment on hard to track potential error caused by #define in irep_hash
This could save external users time (internal users shouldn't encounter this as we don't use Boost)
2017-03-14 10:20:58 +00:00
5f272f790c
Remove unnecessary casts from json.h
2017-03-14 10:20:21 +00:00
30fe7c8708
Added IDE files to .gitignore
2017-03-14 10:20:06 +00:00
211cb901d9
Invoked full_slicer after generic property intrumentation
...
Invoked the full_slicer method just after generic property instrumentation
so that CBMC can properly slice the program w.r.t. a given assertion in the program.
Additionally, replaced returns from goto functions in goto_instrument_parse_options,
as done similarly in cbmc_parse_options
2017-03-14 09:25:45 +00:00
0139558ba4
Merge pull request #570 from zemanlx/feature/compile-on-musl
...
Support for non-glibc linux which use musl-libc
2017-03-13 15:28:19 +00:00
eb93231018
Merge pull request #526 from martin-cs/fix-cfg-dominator-top
...
Fix cfg dominator top
2017-03-13 15:26:36 +00:00
aeb99e86fd
Merge pull request #558 from rjmunro/feature/cpplint-sed-format
...
cpplint sed format improvements
2017-03-13 15:26:01 +00:00
36c2e2dee2
Merge pull request #604 from mgudemann/limit_class_loading
...
Limit class loading
2017-03-13 15:20:38 +00:00
272bce3b0b
Merge pull request #506 from cristina-david/exception-handling
...
Java exception handling
2017-03-11 16:48:47 +00:00
Peter Schrammel