Skip to content

Merge develop to security scanner support #1354

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 89 commits into from
Sep 8, 2017
Merged

Merge develop to security scanner support #1354

Changes from 1 commit
Commits
Show all changes
89 commits
Select commit Hold shift + click to select a range
10a0c01
Pointers returned by getenv must not be manipulated
tautschnig Aug 15, 2017
6d68345
ansi-c library: explicit non-det initialisation, cleanup, syntax fixes
tautschnig Aug 15, 2017
e49c751
Improve ansi-c library syntax check and run via travis
tautschnig Aug 15, 2017
b142da4
Check for memory leaks in C++ new/delete
tautschnig Jan 5, 2017
b934a13
Flag java internal functions as internal in JSON/XML output
peterschrammel Aug 31, 2017
94ec790
Clarified INVARIANT message in get_message_handler
NathanJPhillips Aug 31, 2017
45a97aa
Merge pull request #1313 from NathanJPhillips/bugfix/invariant-message
kroening Aug 31, 2017
d5a5045
HAVE_BV_REFINEMENT and HAVE_JAVA_BYTECODE are no longer needed
kroening Aug 31, 2017
02ed3bf
Merge pull request #1318 from diffblue/HAVE_JAVA_BYTECODE_cleanup
kroening Sep 1, 2017
5fb4cbf
Merge pull request #1243 from tautschnig/ansi-c-library-fixes
kroening Sep 1, 2017
4be7685
Do not add an "l" prefix to double constants when double==long double
tautschnig Sep 1, 2017
e8129a0
Merge basic blocks that are chains of unconditional gotos
peterschrammel Aug 15, 2017
6a8b46f
Instruction to be instrumented representative for basic block
peterschrammel Aug 15, 2017
317f7e8
Protect internals of basic_blockst
peterschrammel Aug 30, 2017
60eb74e
Factor out updating of covered lines in block
peterschrammel Aug 31, 2017
f9ac37a
Select basic block representative instruction
peterschrammel Aug 15, 2017
7f374b3
Warn about anomalies in basic block instrumentation
peterschrammel Aug 15, 2017
99d9613
Expect existing coverage file only to contain array of goals
peterschrammel Aug 21, 2017
5e7a328
List existing goals
peterschrammel Aug 21, 2017
e641d76
Use target source location for java code branches
peterschrammel Aug 16, 2017
d8fdbdb
Regex match on files to be coverage-instrumented
peterschrammel Aug 29, 2017
45ca408
Do not instrument java array built-in functions
peterschrammel Aug 29, 2017
6fee437
Debug info for unique bytecode instrumentation selection
peterschrammel Aug 31, 2017
b85624e
Add missing function ids to instrumented instructions
peterschrammel Aug 31, 2017
bbc99d9
Remove redundant function name from goal descriptions
peterschrammel Aug 31, 2017
e54bc47
Tests for unique java bytecode instrumentation selection
peterschrammel Aug 31, 2017
b6ef688
Fix and run cbmc-cover tests
peterschrammel Aug 31, 2017
15a67e4
Merge pull request #1320 from tautschnig/double-output
kroening Sep 1, 2017
4c94e7c
goto-instrument model-argc-argv: place environment in __CPROVER__start
tautschnig Apr 12, 2017
e8e1677
dump-c: output a generated environment via --harness
tautschnig Apr 12, 2017
a01eeb7
Use invariant annotations instead of asserts
tautschnig Jun 28, 2017
4466408
Replace 3-valued char by enum
tautschnig Aug 23, 2017
48845af
Interpreter: constify mp_integer typed address parameters
tautschnig Aug 23, 2017
f39e5ab
Merge pull request #810 from tautschnig/harness-output
tautschnig Sep 1, 2017
052c149
Merge pull request #1255 from peterschrammel/bugfix/java-unambiguous-…
peterschrammel Sep 1, 2017
8254a3f
Merge pull request #1312 from peterschrammel/bugfix/java-is-internal
peterschrammel Sep 1, 2017
52d1e04
Do not use default arguments for json(...)
tautschnig Aug 23, 2017
4d35274
Simplify pointer_offset(constant)
tautschnig Aug 23, 2017
27fd210
Use generic simplify_expr instead of local simplification rules
tautschnig Aug 23, 2017
28fb804
Merge pull request #1288 from tautschnig/develop-json
tautschnig Sep 2, 2017
6c56f19
Do not attempt to compute union sizes when not required
kroening Aug 25, 2017
165ec47
Test alignment of unions
kroening Aug 25, 2017
4349d91
Merge pull request #1297 from diffblue/union-padding-fix
tautschnig Sep 2, 2017
003482a
MetaChar: use std::stringstream for incremental escaped-string constr…
tautschnig May 13, 2017
8555871
member_offset_bits: express member offset in bits instead of bytes
tautschnig May 13, 2017
3fdcae4
Merge pull request #1331 from tautschnig/cleanup-metachar
kroening Sep 3, 2017
75bdd63
Merge pull request #1332 from tautschnig/member_offset_bits
kroening Sep 3, 2017
4c1b3b3
target name wrong for signed variant of goto-diff
kroening Sep 3, 2017
db77596
Merge pull request #1289 from tautschnig/develop-interpreter-fixes
kroening Sep 3, 2017
52cbfe8
Merge pull request #1334 from diffblue/goto-diff-signed
tautschnig Sep 3, 2017
5bfe346
use ranged for
kroening Aug 29, 2017
29f1e2a
eliminate constrained BP calls
kroening Aug 29, 2017
9e43500
remove assert()
kroening Aug 29, 2017
ede380f
goto-gcc removes CPROVER macros for native gcc
karkhaz Jun 21, 2017
c8f69b5
Merge pull request #1108 from karkhaz/kk-neu-cprover-remove
tautschnig Sep 4, 2017
1fd8b87
Add header for magic numbers
karkhaz Jul 14, 2017
85521b0
goto-gcc reads definitions from linker scripts
karkhaz Jun 5, 2017
cb467c9
Merge pull request #1173 from karkhaz/kk-synthesise-linker-symbols
tautschnig Sep 4, 2017
3947228
Do not overwrite non-zero return codes
tautschnig Sep 4, 2017
433e139
Fix verbosity in goto-gcc
kroening Aug 24, 2017
94ce608
Merge pull request #1344 from tautschnig/fix-result-checking
tautschnig Sep 4, 2017
dd5adf7
Properly prepare goto model for (reachability) slice
tautschnig Sep 4, 2017
b2397e4
Merge pull request #1346 from tautschnig/slicing-prep
kroening Sep 4, 2017
59c882b
Merge pull request #1294 from diffblue/goto-gcc-fix
tautschnig Sep 5, 2017
2e04c17
Replace syntactic_difft pointer by automatic variable
Sep 1, 2017
3dd8fe5
Merge pull request #1352 from janmroczkowski/janmroczkowski/syntactic…
tautschnig Sep 6, 2017
dce6ae1
Improve filter_by_diff.py and friends
smowton Sep 5, 2017
389221e
run_diff.sh shellcheck fixes
smowton Sep 6, 2017
b28e701
fixup! variants of service functions for goto_modelt
tautschnig Sep 4, 2017
fd56921
fixup! Fix and run cbmc-cover tests
tautschnig Sep 4, 2017
8054162
fixup! Instrument string-refinement code such that null-pointer check…
tautschnig Sep 4, 2017
7d26139
fixup! Replace BV_ADDR_BITS by config setting
tautschnig Sep 4, 2017
d5db0bc
fixup! added a test case for combination use of forall/exists/not.
tautschnig Sep 5, 2017
191f371
fixup! a right place to implement the quantifier handling.
tautschnig Sep 5, 2017
24be89c
fixup! simplify \'not exists\' to the form of \'forall not\'
tautschnig Sep 5, 2017
dfd00d3
fixup! Translate exprt to/from miniBDD
tautschnig Sep 5, 2017
66719a9
fixup! goto-instrument --print-path-lengths: statistics about control…
tautschnig Sep 5, 2017
f12c790
fixup! fixup! Add --drop-unused-functions option
tautschnig Sep 5, 2017
82ab237
fixup! Split java nondet pass in two
tautschnig Sep 5, 2017
2060b34
fixup! Added __CPROVER_array_replace to complement __CPROVER_array_set
tautschnig Sep 5, 2017
9d5d907
fixup! Allow extra entry-points to be specified for CI lazy loading
tautschnig Sep 5, 2017
f72b7fc
pointer_typet now requires a width
kroening Aug 23, 2017
ce86319
pointer types now have width
kroening May 28, 2017
d3c0b57
remove legacy constructors
kroening Aug 15, 2017
02c4ac6
Merge pull request #1303 from diffblue/cleanup-goto-inline
kroening Sep 7, 2017
0423be7
Merge pull request #1351 from tautschnig/develop-cleanup
kroening Sep 7, 2017
8425bf4
Merge pull request #970 from diffblue/pointers-with-width
kroening Sep 7, 2017
34492db
Merge pull request #1350 from diffblue/smowton/feature/improved_filte…
smowton Sep 7, 2017
5648db1
Merge latest changes from develop to Security Scanner Support
NathanJPhillips Sep 7, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
fixup! Added __CPROVER_array_replace to complement __CPROVER_array_set
  • Loading branch information
@tautschnig
tautschnig committed Sep 6, 2017
commit 2060b34de7481cc9f058b374286d9f957b1070bf
7 changes: 1 addition & 6 deletions src/goto-programs/goto_convert_class.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -530,11 +530,6 @@ class goto_convertt:public messaget
const exprt &rhs,
const exprt::operandst &arguments,
goto_programt &dest);
void do_array_set(
const exprt &lhs,
const exprt &rhs,
const exprt::operandst &arguments,
goto_programt &dest);
void do_array_equal(
const exprt &lhs,
const exprt &rhs,
Expand All @@ -543,7 +538,7 @@ class goto_convertt:public messaget
void do_array_op(
const irep_idt &id,
const exprt &lhs,
const exprt &rhs,
const exprt &function,
const exprt::operandst &arguments,
goto_programt &dest);
void do_printf(
Expand Down