Feature cbmc bump #235
Feature cbmc bump #235
Conversation
| @@ -164,6 +191,75 @@ package body Driver is | |||
| Append_Op (Start_Body, Initialization_Statement); | |||
| end Initialize_CProver_Rounding_Mode; | |||
|
|
|||
| procedure Initialize_CProver_Dead_Object; | |||
There was a problem hiding this comment.
So these three procedures only differ in the Identifier?
There was a problem hiding this comment.
pretty much. I can abstract if if you prefer?
There was a problem hiding this comment.
Looks good to me - but could you make sure that @martin-cs is OK with bumping CBMC before you merge - he has some work built on top of the CBMC submodule so we'll need to make sure he's OK to rebase before we merge this gnat2goto CBMC submodule bump
|
I've confirmed with @martin-cs that it's ok to bump the submodule - so just needs CI sorting and second review. |
|
BTW - If there is a specific reason for the submodule bump, (e.g. to pickup a fix/feature we need) it would be fantastic if that reason was included in the commit message for the commit that actually moves the submodule pointer :-) |
This gives us symbol table linking support in CBMC, so we should be able to do more complicated test scenarios now.
hannes-steffenhagen-diffblue
force-pushed
the
feature-cbmc_bump
branch
from
97e9496 to
708efba
Compare
Bump CBMC and fix issues arising from it