Fix: Do not nondet functions and fix scoping issue #4277
Conversation
NlightNFotis
requested review from
chrisr-diffblue,
danpoe,
hannes-steffenhagen-diffblue,
martin-cs and
peterschrammel
as code owners
| @@ -24,4 +24,4 @@ if [ -e "${name}-mod.gb" ] ; then | |||
| fi | |||
|
|
|||
| $goto_harness "${name}.gb" "${name}-mod.gb" --harness-function-name $entry_point ${args} | |||
| $cbmc --function $entry_point "${name}-mod.gb" | |||
| $cbmc --function $entry_point "${name}-mod.gb" --unwind 20 --unwinding-assertions | |||
There was a problem hiding this comment.
Basically it’s a bit annoying to hardcode cbmc options here. We’ve been considering changing our chain.sh to allow us to set cbmc options per test case, but we decided to not do this as part of this PR for now.
There was a problem hiding this comment.
@hannes-steffenhagen-diffblue - Might be worth raising this point with @karkhaz as he is currently working on re-writing test.pl in Python and cleaning up a few things at the same time - could be a good time to address chain.sh as well.
There was a problem hiding this comment.
@chrisr-diffblue We were thinking as part of a later PR to change chain.sh into a python script. This would make it much easier for things like organising configuration of different tool invocations. We'll see if we can leverage the work done on that front as well.
NlightNFotis
force-pushed
the
fix-goto-harness-pointer-init
branch
from
419a958 to
595e91e
Compare
regression/goto-harness/nondet_elements_longer_lists_global/main.c
Outdated
Show resolved
Hide resolved
| // a good idea, therefore we just collect the names of globals | ||
| // we need to initialise first and then generate the | ||
| // initialisation code for all of them. | ||
| auto global_names = std::vector<irep_idt>{}; |
There was a problem hiding this comment.
std::vector<irep_idt> global_names; would do.
In goto-harness: - we used is_static && is_lvalue to determine something was global. Turns out that this also applies to extern functions for some reason, so we ended up accidentally creating nondet assignments to those. We now check type.id() != ID_code as well. - we declared pointers to local variables. In if blocks. Which went out of scope before using them. This meant we had a bunch of dangling references. We solve this by creating global variables for our pointer-pointees instead of local ones. Co-authored-by: Fotis Koutoulakis <[email protected]> Co-authored-by: Hannes Steffenhagen <[email protected]>
NlightNFotis
force-pushed
the
fix-goto-harness-pointer-init
branch
from
595e91e to
cefb1dd
Compare
There was a problem hiding this comment.
This PR failed Diffblue compatibility checks (cbmc commit: 595e91e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102196809
Status will be re-evaluated on next push.
Common spurious failures:
-
the cbmc commit has disappeared in the mean time (e.g. in a force-push)
-
the author is not in the list of contributors (e.g. first-time contributors).
-
the compatibility was already broken by an earlier merge.
There was a problem hiding this comment.
✔️
Passed Diffblue compatibility checks (cbmc commit: cefb1dd).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/102203069
In goto-harness:
Turns out that this also applies to extern functions for some reason,
so we ended up accidentally creating nondet assignments to those.
We now check type.id() != ID_code as well.
out of scope before using them. This meant we had a bunch of
dangling references. We solve this by creating global variables
for our pointer-pointees instead of local ones.
Co-authored-by: Fotis Koutoulakis [email protected]
Co-authored-by: Hannes Steffenhagen [email protected]