Skip to content

add a 'language feature' detection facility for goto programs #7771

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 1 commit into from
Nov 2, 2023

Conversation

kroening
Copy link
Member

This adds a facility to detect the usage of specific language features by a goto program. The features are detected by iterating over the functions of the program.

Checks for three language features not supported by goto symex are added (assembler, function pointers, vectors).

  • Each commit message has a non-empty body, explaining why the change was made.
  • 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.

@kroening kroening force-pushed the goto-language-feature-tests branch from 7fdbd05 to 43f63dc Compare June 19, 2023 12:49
@codecov
Copy link

codecov bot commented Jun 19, 2023

Codecov Report

Patch coverage: 77.14% and project coverage change: +0.51 🎉

Comparison is base (b1d78e2) 78.06% compared to head (43f63dc) 78.57%.

❗ Current head 43f63dc differs from pull request most recent head 4408b1f. Consider uploading reports for the commit 4408b1f to get more accurate results

Additional details and impacted files
@@             Coverage Diff             @@
##           develop    #7771      +/-   ##
===========================================
+ Coverage    78.06%   78.57%   +0.51%     
===========================================
  Files         1693     1693              
  Lines       193308   193343      +35     
===========================================
+ Hits        150899   151919    +1020     
+ Misses       42409    41424     -985     
Impacted Files Coverage Δ
src/goto-programs/remove_vector.cpp 95.26% <63.63%> (-1.74%) ⬇️
src/assembler/remove_asm.cpp 77.91% <77.77%> (-0.01%) ⬇️
src/goto-programs/remove_function_pointers.cpp 94.09% <83.33%> (-0.63%) ⬇️
src/goto-checker/multi_path_symex_checker.cpp 95.83% <100.00%> (+0.18%) ⬆️

... and 54 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

This adds a facility to detect the usage of specific language features by a
goto program.  The features are detected by iterating over the functions
of the program.

Checks for three language features not supported by goto symex are added
(assembler, function pointers, vectors).
@kroening kroening force-pushed the goto-language-feature-tests branch from 43f63dc to 4408b1f Compare June 19, 2023 17:18
@kroening kroening marked this pull request as ready for review June 19, 2023 20:37
@kroening kroening requested review from a team, peterschrammel, TGWDB and tautschnig as code owners June 19, 2023 20:37
@TGWDB
Copy link
Contributor

TGWDB commented Jul 19, 2023

Maybe we should also check for vectors (see #7736)? If this is out of the scope of this PR then it would be nice to confirm at least before merging.

Copy link
Contributor

@TGWDB TGWDB left a comment

Choose a reason for hiding this comment

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

As discussed, some follow-up documentation and notes to come (likely next week).

@tautschnig tautschnig merged commit cb62568 into develop Nov 2, 2023
@tautschnig tautschnig deleted the goto-language-feature-tests branch November 2, 2023 15:05
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.

4 participants