ogma-core: Comment is inaccurate

[ivanperez-keera]

Description

The Copilot spec generated by Ogma includes the following comment for a spec:

-- | Complete specification. Calls the C function void handler(); when
-- the property is violated.

That comment is inaccurate, since the name of the function executed may not be handler.

Type

• Bug: Error in comment in generated code.

Additional context

None.

Requester

• Ivan Perez.

Method to check presence of bug

Error is in a comment. Check by visual inspection of the Copilot code generated by Ogma.

Expected result

The comment in the code generated by Copilot states that handlers are executed, not that a specific function handler(); is called.

Desired result

The comment in the code generated by Copilot states that handlers are executed, not that a specific function handler(); is called.

Proposed solution

Modify comment in https://github.com/nasa/ogma/blob/develop/ogma-core/src/Language/Trans/Spec2Copilot.hs#L201 to state that handlers are executed upon property violations.

Further notes

None.

[ivanperez-keera]

Change Manager: Confirmed that the issue exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Issue scheduled for fixing in Ogma 1.5.

Fix assigned to: @ivanperez-keera .

[ivanperez-keera]

Implementor: Solution implemented, review requested.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:
  • The code proposed compiles and passes all tests. Details:
    • Build logs:
      • https://github.com/nasa/ogma/actions/runs/11963632175/job/33354425316
      • https://github.com/nasa/ogma/actions/runs/11963632174/job/33354425323
    • Build log archives:
      • logs_31193480821.zip
      • logs_31193480824.zip
  • The solution proposed produces the expected result. Details:
    Evaluated by visual inspection running the spec backend and looking at the output. Additionally, the following dockerfile runs the spec backend and checks that the output no longer contains the fixed string "handler();", in which case it prints the message "Success":

    FROM ubuntu:trusty
    
    ENV DEBIAN_FRONTEND=noninteractive
    
    RUN apt-get update
    
    RUN apt-get install --yes software-properties-common
    RUN add-apt-repository ppa:hvr/ghc
    RUN apt-get update
    
    RUN apt-get install --yes ghc-8.6.5 cabal-install-2.4
    RUN apt-get install --yes libz-dev
    
    ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH
    
    RUN cabal update
    RUN cabal v1-sandbox init
    RUN cabal v1-install alex happy
    RUN apt-get install --yes git
    
    SHELL ["/bin/bash", "-c"]
    CMD git clone $REPO \
        && cd $NAME \
        && git checkout $COMMIT \
        && cd .. \
        && cabal v1-sandbox init \
        && cabal v1-install $NAME/$PAT**/ --constraint="aeson>=2.0.3.0" \
        && ./.cabal-sandbox/bin/ogma fret-component-spec --fret-file-name $NAME/ogma-cli/examples/fret.json > Spec.hs \
        && ! grep 'handler();' Spec.hs \
        && echo "Success"

    Command (substitute variables based on new path after merge):

    $ docker run -e "REPO=https://github.com/ivanperez-keera/ogma" -e "NAME=ogma" -e "PAT=ogma"  -e "COMMIT=69e128c1a71a61ffbb46daf52f0a48826360c80a" -it ogma-verify-164
    

• Implementation is documented. Details:
  No updates needed. Change is to a comment in the output code.
• Change history is clear.
• Commit messages are clear.
• Changelogs are updated.
• Examples are updated. Details:
  No updates needed.
• Required version bumps are evaluated. Details:
  No bump needed. Change is to a comment in the output code.

[ivanperez-keera]

Change Manager: Implementation ready to be merged.