Skip to content

Clarify heap types for arrays #58

@gmalecha-at-skylabs

Description

@gmalecha-at-skylabs

Unify the two functions:

  • to_heap_type ( rocq-bluerock-brick/theories/lang/cpp/syntax/types.v), and
  • heap_type_of (rocq-bluerock-brick/theories/lang/cpp/logic/initializers.v)

Further,

  1. refine the notion of heap types for arrays (maybe just heap types of the element type?) to be compatible with wp_init_well_typed. The complexity here lies in Tincomplete_array and Tvariable_array.
  2. prove that to_heap_type always produces a type that satisfies is_heap_type.

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions