Skip to content

Commit

Permalink
Merge branch 'develop-comment-handler' into develop. Close #164.
Browse files Browse the repository at this point in the history
**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.

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":

```Dockerfile
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):

```sh
$ docker run -e "REPO=https://github.com/NASA/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=<HASH>" -it ogma-verify-164
```

**Expected result**

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

Running the dockerfile above prints "Success", indicating that the
specific string "handler();" is no longer part of the output.

**Solution implemented**

Modify comment in `ogma-core/src/Language/Trans/Spec2Copilot.hs#L201` to
state that handlers (plural) are executed upon property violations.

**Further notes**

None.
  • Loading branch information
ivanperez-keera committed Nov 22, 2024
2 parents 6325b1d + 69e128c commit 743eacc
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 4 deletions.
3 changes: 2 additions & 1 deletion ogma-core/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,10 +1,11 @@
# Revision history for ogma-core

## [1.X.Y] - 2024-11-20
## [1.X.Y] - 2024-11-21

* Fix incorrect path when using Space ROS humble-2024.10.0 (#158).
* Use template expansion system to generate cFS monitoring application (#157).
* Use template expansion system to generate ROS monitoring application (#162).
* Fix comment in generated Copilot spec (#164).

## [1.4.1] - 2024-09-21

Expand Down
6 changes: 3 additions & 3 deletions ogma-core/src/Language/Trans/Spec2Copilot.hs
Original file line number Diff line number Diff line change
Expand Up @@ -197,9 +197,9 @@ spec2Copilot specName typeMaps exprTransform showExpr spec =
-- Main specification
copilotSpec :: [String]
copilotSpec = [ ""
, "-- | Complete specification. Calls the C function void "
++ " handler(); when"
, "-- the property is violated."
, "-- | Complete specification. Calls C handler functions"
++ " when"
, "-- properties are violated."
, "spec :: Spec"
, "spec = do"
]
Expand Down

0 comments on commit 743eacc

Please sign in to comment.