Skip to content

Conversation

@reuk
Copy link
Contributor

@reuk reuk commented Apr 25, 2017

The most important part of this patch is the added initialisers in symex_target_equation.h, which fix this warning:

symex_target_equation.h:167:9: runtime error: load of value 3432879264, which is not a valid value for type 'assignment_typet'

This error was observed in diffblue/platform#520, when cbmc was built using clang's undefined behaviour sanitizer.

Although only the addition on line 209 is strictly required, I've also added initializers for the other primitive data members, because objects should always be in a known state which maintains their invariants once the constructor has finished.

Finally, I changed assignment_typet into an enum class to improve its type-safety and avoid undesired conversions.

@reuk reuk mentioned this pull request Apr 25, 2017
@tautschnig
Copy link
Collaborator

Is this genuinely a test-gen-support problem only?

@reuk reuk mentioned this pull request Apr 26, 2017
@reuk
Copy link
Contributor Author

reuk commented Apr 26, 2017

Possibly not - closing this in favour of #872.

@reuk reuk closed this Apr 26, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants