omit the DECLARE line in `INLINE_SPEC` clauses #70

New issue

Open

opened 2026-10-22 14:42:50 +02:00 by EatOreo · 1 comment

EatOreo commented

2026-10-22 14:42:50 +02:00

Owner

for instance in:

SPEC_INLINE  <{ 
    DECLARE _sumarray
      WITH a: val, sh : share, contents : list Z, size: Z
      ...
  }>
  unsigned sumarray(unsigned a[], int n) {
  ...

the "DECLARE _sumarray" can be infered from the function name

for instance in: ```c SPEC_INLINE <{ DECLARE _sumarray WITH a: val, sh : share, contents : list Z, size: Z ... }> unsigned sumarray(unsigned a[], int n) { ... ``` the "DECLARE _sumarray" can be infered from the function name

marfavi added this to the Release roadmap project

2026-10-22 14:51:14 +02:00

marfavi commented

2026-10-23 15:32:38 +02:00

Owner

Why not go even further and remove separate _INLINE clauses❓

  /*@
    SPEC spec.v:specification <{
      WITH a: val, sh : share, contents : list Z, size: Z
    ...
    }>
  */
  unsigned sumarray(unsigned a[], int n) {
  ...

Why not go even further and remove separate `_INLINE` clauses❓ ``` /*@ SPEC spec.v:specification <{ WITH a: val, sh : share, contents : list Z, size: Z ... }> */ unsigned sumarray(unsigned a[], int n) { ... ```

marfavi added the

quick-pick

label

2026-10-28 14:23:25 +01:00

marfavi referenced this issue from a commit

2026-10-28 14:55:26 +01:00

Infer DECLARE for SPEC_INLINE from the C function (#70)

marfavi referenced this issue from a pull request that will close it,

2026-10-28 14:55:29 +01:00

Inline SPEC/INV bodies with inferred DECLARE #86

marfavi self-assigned this

2026-10-30 13:59:19 +01:00