Skip to content

Conversation

@tautschnig
Copy link
Collaborator

The nondet symbol factory uses "tmp" as a default basename prefix, and
in all other places already generated unique names using
get_fresh_aux_symbol. This function, however, will happily use exactly
that basename when there wouldn't be a conflict. The code fixed in this
commit, however, did not yet use this facility, and just assumed that
each parameter of the target function would result in a unique local
name. A parameter named "tmp," then, resulted in a conflict.
Consistently using get_fresh_aux_symbol addresses this problem.

Fixes: #6566

Co-authored-by: Matthias Güdemann matthias.guedemann@hm.edu

  • Each commit message has a non-empty body, explaining why the change was made.
  • n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@codecov
Copy link

codecov bot commented Jan 11, 2022

Codecov Report

Merging #6569 (de5bbd1) into develop (9ba013d) will decrease coverage by 0.00%.
The diff coverage is 88.46%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #6569      +/-   ##
===========================================
- Coverage    76.01%   76.01%   -0.01%     
===========================================
  Files         1579     1579              
  Lines       181304   181288      -16     
===========================================
- Hits        137819   137799      -20     
- Misses       43485    43489       +4     
Impacted Files Coverage Δ
src/goto-checker/multi_path_symex_checker.cpp 91.30% <ø> (ø)
src/goto-instrument/contracts/assigns.h 100.00% <ø> (ø)
src/goto-instrument/contracts/contracts.h 100.00% <ø> (ø)
...trument/contracts/havoc_assigns_clause_targets.cpp 97.72% <ø> (-0.72%) ⬇️
src/goto-instrument/goto_program2code.cpp 68.32% <0.00%> (ø)
src/goto-programs/allocate_objects.h 100.00% <ø> (ø)
src/goto-symex/solver_hardness.cpp 52.73% <ø> (ø)
src/goto-symex/symex_target_equation.cpp 95.06% <ø> (ø)
src/solvers/flattening/boolbv_member.cpp 97.56% <ø> (ø)
src/solvers/flattening/boolbv_struct.cpp 100.00% <ø> (ø)
... and 39 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 08d5056...de5bbd1. Read the comment docs.

@kroening kroening assigned tautschnig and unassigned kroening Jan 12, 2022
The nondet symbol factory uses "tmp" as a default basename prefix, and
in all other places already generated unique names using
`get_fresh_aux_symbol`. This function, however, will happily use exactly
that basename when there wouldn't be a conflict. The code fixed in this
commit, however, did not yet use this facility, and just assumed that
each parameter of the target function would result in a unique local
name. A parameter named "tmp," then, resulted in a conflict.
Consistently using `get_fresh_aux_symbol` addresses this problem.

Fixes: diffblue#6566

Co-authored-by: Matthias Güdemann <matthias.guedemann@hm.edu>

fixup! C nondet factory: Ensure parameter initialisers use unique symbol names
Use references and symbol names to track created symbols rather than
pointers. This avoids the risk of dereferencing pointers to objects that
have been deallocated by the time dereferencing takes place.

This is just defensive programming, no known bugs fixes or changes in
behaviour intended.
@tautschnig tautschnig merged commit 9f9ee07 into diffblue:develop Jan 12, 2022
@tautschnig tautschnig deleted the bugfixes/6566 branch January 12, 2022 18:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Invariant violation parsing simple C program

3 participants