Skip to content

helper for getting the function type used in function_application_exprt #5737

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.

Sign up for GitHub

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

Jump to bottom
Merged
merged 1 commit into from
Jan 12, 2021
Merged

helper for getting the function type used in function_application_exprt #5737

merged 1 commit into from
Jan 12, 2021

Conversation

kroening
Copy link
Member

This commit

  1. adds a comment to the constructor of function_application_exprt that
    clarifies the (already existing) requirements on the first argument of the
    constructor.

and

  1. adds a helper for obtaining the type of the function that is applied.
  • 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.

tautschnig
tautschnig approved these changes Jan 12, 2021
View reviewed changes
src/util/mathematical_expr.h Outdated
/// \brief Application of (mathematical) function
class function_application_exprt : public binary_exprt
{
public:
using argumentst = exprt::operandst;

/// \a _function must be known to have \ref mathematical_function_typet type.
Copy link
Collaborator

Choose a reason for hiding this comment

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

I think we've elsewhere used \p when referring to parameters.

src/util/mathematical_expr.h Outdated
@@ -204,6 +207,9 @@ class function_application_exprt : public binary_exprt
return op0();
}

/// the type of the expression returned by \ref function
Copy link
Collaborator

Choose a reason for hiding this comment

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

I'm not sure we are perfectly consistent about this, but I'd think we use a full sentence here (i.e., uppercase the first word and end with a full stop.).

@kroening kroening force-pushed the mathematical_function_applicationt branch 2 times, most recently from e943d68 to da5d07e Compare January 12, 2021 15:24
@kroening kroening marked this pull request as ready for review January 12, 2021 15:33
@kroening
helper for getting the function type used in function_application_exprt
25ed1d7 
This commit

1) adds a comment to the constructor of function_application_exprt that
clarifies the (already existing) requirements on the first argument of the
constructor.

and

2) adds a helper for obtaining the type of the function that is applied.

and

3) uses the helper in goto-symex.
@kroening kroening force-pushed the mathematical_function_applicationt branch from da5d07e to 25ed1d7 Compare January 12, 2021 15:35
@codecov
Copy link

codecov bot commented Jan 12, 2021 •
edited
Loading

Codecov Report

Merging #5737 (25ed1d7) into develop (caf309e) will increase coverage by 0.00%.
The diff coverage is 100.00%.

Impacted file tree graph

@@           Coverage Diff            @@
##           develop    #5737   +/-   ##
========================================
  Coverage    69.54%   69.54%           
========================================
  Files         1243     1243           
  Lines       100700   100702    +2     
========================================
+ Hits         70036    70038    +2     
  Misses       30664    30664
Flag Coverage Δ
cproversmt2 43.29% <21.42%> (+<0.01%) ⬆️
regression 66.45% <100.00%> (+<0.01%) ⬆️
unit 32.23% <21.42%> (+<0.01%) ⬆️

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

Impacted Files Coverage Δ
src/util/mathematical_expr.h 91.66% <ø> (ø)
src/goto-symex/goto_symex.cpp 99.71% <100.00%> (ø)
src/util/mathematical_expr.cpp 100.00% <100.00%> (ø)

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 caf309e...25ed1d7. Read the comment docs.

@tautschnig
Copy link
Collaborator

The CodeBuild failure is an issue with Maven downloads, which the GitHub actions also temporarily had (but restarting them solved the problem). Thus ignoring and merging.

@tautschnig tautschnig merged commit 67b36f0 into develop Jan 12, 2021
@tautschnig tautschnig deleted the mathematical_function_applicationt branch January 12, 2021 21:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tautschnig tautschnig tautschnig approved these changes

@peterschrammel peterschrammel peterschrammel approved these changes

@romainbrenguier romainbrenguier Awaiting requested review from romainbrenguier

@smowton smowton Awaiting requested review from smowton

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@kroening @tautschnig @peterschrammel