Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
why3
why3
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 126
    • Issues 126
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 16
    • Merge Requests 16
  • Operations
    • Operations
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
  • Why3
  • why3why3
  • Issues
  • #108

Closed
Open
Opened Apr 17, 2018 by Andrei Paskevich@paskevycOwner

[@model_trace: <name>] labels redundant?

Is there a reason to have these labels on symbols, in addition to [@model]? It seems that the name they carry always coincides with id_string of the symbol ident. If we need to change the name, e.g. for the SPARK-produced inputs, maybe we can only use [@model_trace: ...] in these cases, but not by default?

To upload designs, you'll need to enable LFS and have admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: why3/why3#108