cbmc:icnf

Branch merges

Related source package recipes

No recipes using this branch. (?)

Create packaging recipe

Related snap packages

Related charm recipes

e491441... by Daniel Kroening <email address hidden> on 2019-04-23

add --icnf option to cbmc

7c32e71... by Daniel Kroening <email address hidden> on 2019-04-23

add icnf solver class

01255db... by Daniel Kroening <email address hidden> on 2019-04-18

avoid access to exprt::opX

This avoids out-of-bounds accesses to the operands() vector.

95b1101... by Daniel Kroening <email address hidden> on 2019-04-19

introduce a ranged for

dc67638... by Daniel Kroening <email address hidden> on 2019-04-18

avoid access to exprt::opX

This prevents out-of-bounds accesses to the operands() vector.

65e6b6a... by Michael Tautschnig on 2019-04-18

Merge pull request #4547 from danpoe/feature/sharing-map-unit-tests

Add unit tests for sharing map that check that views are not invalidated by modifications

620e27d... by Michael Tautschnig <email address hidden> on 2019-04-18

C++ front-end: store typedef names

This is already supported in the C front-end, and we should not
unnecessarily deviate in behaviour between the C and C++ front-ends.

44bbea0... by Daniel Kroening <email address hidden> on 2019-04-18

move goto_functionst::validate into .cpp file

The function is large, and thus, this improves compile times.

2b4f0ae... by Daniel Poetzl <email address hidden> on 2019-04-18

Use REQUIRE_THROWS_AS() in sharing map unit tests

2d29291... by Daniel Poetzl <email address hidden> on 2019-04-17

Refactor existing tests of error cases to use cbmc_invariants_should_throwt

This adds sharing map unit tests to check that operations fail as expected. For
example, calling map.replace(key, value) when the key does not exist in the map
should fail.