allow contracts on function declarations

[kroening]

This changes the grammar of the C frontend to allow contracts on function
declarations. This also removes the requirement that the contract clauses
appear in any particular order.

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

This looks nice, but given that tests are failing there obviously are some problems left to be fixed. Nothing blatantly obvious while reviewing the source code, thus requires more debugging.

[feliperodri]

This looks nice, but given that tests are failing there obviously are some problems left to be fixed. Nothing blatantly obvious while reviewing the source code, thus requires more debugging.

All code contracts are failing, which is expected since the regression suite also need to be updated (i.e., move all contracts to function declarations).

[kroening]

The bit that is missing is to change the scope to the scope used for the parameters when parsing the contract expressions.

There should not be a need to change any of the existing tests, the existing syntax continues to work.

[martin-cs]

On Wed, 2021-03-17 at 08:09 -0700, Felipe R. Monteiro wrote: > This looks nice, but given that tests are failing there obviously > are some problems left to be fixed. Nothing blatantly obvious while > reviewing the source code, thus requires more debugging. All code contracts are failing, which is expected since the regression suite also need to be updated (i.e., move all contracts to function declarations).

I don't know your use-case fully but one cute feature SPARK has is that you can put preconditions and postconditions on both the declaration and definitions of functions. You need that they imply each other but it allows you to separate the pre/post you use to prove the function and the pre/post you use as an abstraction in proving other code. It is really more useful when the code base gets larger but if we are in a place where we /could/ implement this maybe we should think about if we /should/. Cheers, - Martin

[codecov]

Codecov Report

Merging #5946 (4a50ac1) into develop (867168c) will increase coverage by 0.77%.
The diff coverage is 92.94%.

@@             Coverage Diff             @@
##           develop    #5946      +/-   ##
===========================================
+ Coverage    74.24%   75.01%   +0.77%     
===========================================
  Files         1431     1431              
  Lines       155290   155276      -14     
===========================================
+ Hits        115290   116483    +1193     
+ Misses       40000    38793    -1207     

Impacted Files	Coverage Δ
src/ansi-c/c_typecheck_base.h	100.00% <ø> (ø)
src/ansi-c/c_typecheck_code.cpp	77.91% <ø> (+0.28%)	⬆️
src/ansi-c/expr2c.cpp	68.62% <33.33%> (-0.15%)	⬇️
src/ansi-c/ansi_c_convert_type.cpp	78.67% <100.00%> (+0.81%)	⬆️
src/ansi-c/ansi_c_convert_type.h	100.00% <100.00%> (ø)
src/ansi-c/ansi_c_declaration.cpp	72.89% <100.00%> (+0.78%)	⬆️
src/ansi-c/c_typecheck_base.cpp	78.23% <100.00%> (-0.87%)	⬇️
src/ansi-c/parser.y	77.72% <100.00%> (-0.05%)	⬇️
src/ansi-c/parser_static.inc	96.58% <100.00%> (+0.12%)	⬆️
src/symtab2gb/symtab2gb_parse_options.cpp	60.65% <100.00%> (+1.33%)	⬆️
... and 26 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 e166f4c...4a50ac1. Read the comment docs.

[tautschnig]

Looks good to me, but it would be nice to modify some of the existing tests in regression/contract to make use of the new feature. Ideally with all the options now newly available: mixing contracts on declarations and definitions, mixing up their order. Also, what should we expect to happen when both a declaration and a definition have a contract (cf. @martin-cs' comment) - this might mean adding a KNOWNBUG test.