Skip to content

GraphML fixes to ensure SV-COMP compatibility #5660

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Dec 14, 2020

Conversation

tautschnig
Copy link
Collaborator

The witness linter exposed two bugs in our GraphML output. (See the individual commit messages.)

  • 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 Dec 14, 2020

Codecov Report

Merging #5660 (50868ca) into develop (f85b11d) will increase coverage by 0.81%.
The diff coverage is 100.00%.

Impacted file tree graph

@@             Coverage Diff             @@
##           develop    #5660      +/-   ##
===========================================
+ Coverage    68.60%   69.42%   +0.81%     
===========================================
  Files         1243     1243              
  Lines       100621   100626       +5     
===========================================
+ Hits         69027    69855     +828     
+ Misses       31594    30771     -823     
Flag Coverage Δ
cproversmt2 43.15% <100.00%> (?)
regression 66.31% <100.00%> (+<0.01%) ⬆️
unit 32.26% <0.00%> (-0.01%) ⬇️

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

Impacted Files Coverage Δ
src/xmllang/graphml.cpp 68.66% <100.00%> (+0.68%) ⬆️
src/util/simplify_expr_int.cpp 80.08% <0.00%> (+0.27%) ⬆️
src/solvers/lowering/byte_operators.cpp 83.96% <0.00%> (+0.38%) ⬆️
src/cbmc/cbmc_parse_options.cpp 77.62% <0.00%> (+0.44%) ⬆️
src/util/mp_arith.cpp 48.59% <0.00%> (+0.70%) ⬆️
src/solvers/flattening/boolbv.cpp 69.09% <0.00%> (+0.90%) ⬆️
src/util/std_expr.h 89.90% <0.00%> (+1.10%) ⬆️
src/util/std_types.h 94.39% <0.00%> (+1.17%) ⬆️
src/solvers/smt2/smt2_solver.cpp 83.01% <0.00%> (+1.25%) ⬆️
src/util/pointer_offset_size.cpp 94.85% <0.00%> (+1.28%) ⬆️
... and 11 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 f85b11d...50868ca. Read the comment docs.

@tautschnig tautschnig self-assigned this Dec 14, 2020
SV-COMP requires that this is set, which we take care of in your sv-comp
wrapper script.
@tautschnig tautschnig merged commit db24a7c into diffblue:develop Dec 14, 2020
@tautschnig tautschnig deleted the graphml-fixes branch December 14, 2020 15:49
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants