Skip to content

Conversation

@tautschnig
Copy link
Collaborator

The parser happily accepts the syntax shown in the regression test
included, but type checking strictly expects code instead of an
initializer list. Report a proper error message, like GCC does, instead
of failing an invariant.

Test generated using C-Reduce starting from an SV-COMP task.

  • 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.

…nition

The parser happily accepts the syntax shown in the regression test
included, but type checking strictly expects code instead of an
initializer list. Report a proper error message, like GCC does, instead
of failing an invariant.

Test generated using C-Reduce starting from an SV-COMP task.
@codecov
Copy link

codecov bot commented Dec 17, 2020

Codecov Report

Merging #5674 (5233796) into develop (e23bf5c) will increase coverage by 0.00%.
The diff coverage is 100.00%.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #5674   +/-   ##
========================================
  Coverage    69.45%   69.46%           
========================================
  Files         1243     1243           
  Lines       100614   100621    +7     
========================================
+ Hits         69886    69893    +7     
  Misses       30728    30728           
Flag Coverage Δ
cproversmt2 43.14% <22.22%> (-0.01%) ⬇️
regression 66.35% <100.00%> (+<0.01%) ⬆️
unit 32.28% <22.22%> (-0.01%) ⬇️

Flags with carried forward coverage won't be shown. Click here to find out more.

Impacted Files Coverage Δ
src/ansi-c/c_typecheck_base.cpp 81.52% <100.00%> (+0.20%) ⬆️
src/cpp/cpp_typecheck_function.cpp 94.82% <100.00%> (+0.38%) ⬆️

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 e23bf5c...5233796. Read the comment docs.

Copy link
Collaborator

@martin-cs martin-cs left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"Giving a helpful error message rather than an assertion failure on user input" is a great look!

@kroening kroening merged commit 4c3a0a6 into diffblue:develop Dec 23, 2020
@tautschnig tautschnig deleted the invalid-fn branch December 23, 2020 10:52
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.

3 participants