ogma-cli: Augment overview command to report results of spec analysis. Refs #356.

[ivanperez-keera]

Augment ogma-core to formally analyze specs and adjust ogma-cli's overview command to report the results of the analysis to the user, as prescribed in the solution proposed for #356.

[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/22233200880/job/64318074903
      • https://github.com/nasa/ogma/actions/runs/22233200889/job/64318074902
      • https://github.com/nasa/ogma/actions/runs/22233200876/job/64318074861
      • https://github.com/nasa/ogma/actions/runs/22233200890/job/64318074848
    • Build log archives:
      • logs_58047111111.zip
      • logs_58047111121.zip
      • logs_58047111144.zip
      • logs_58047111149.zip
  • The solution proposed produces the expected result. Details:
    The following Dockerfile uses the augmented overview command to analyze a sample spec and check that Ogma can detect that one of the requirements is always true and one is always false, after which it prints the message "Success":

    FROM ubuntu:22.04
    
    ENV DEBIAN_FRONTEND=noninteractive
    
    RUN apt-get update
    SHELL ["/bin/bash", "-c"]
    
    RUN apt-get install --yes \
      alex \
      cabal-install \
      g++ \
      ghc \
      git \
      happy \
      libbz2-dev \
      libexpat1-dev \
      libz-dev \
      pkg-config \
      z3
    
    WORKDIR /root/
    
    ENV PATH=/root/.cabal-sandbox/bin:$PATH
    
    RUN cabal update
    RUN cabal v1-sandbox init
    RUN cabal v1-install BNFC
    RUN cabal v1-install copilot
    
    CMD git clone $REPO \
      && pushd $NAME \
      && git checkout $COMMIT \
      && popd \
      && cabal v1-install $NAME/ogma-**/ \
      && cabal v1-exec -- ogma overview \
           --input-file $NAME/ogma-cli/examples/analysis/expressions.json  \
           --input-format $NAME/ogma-cli/examples/analysis/json-format.cfg \
           --prop-format literal > output \
      && grep -e '1 requirement.* always true' output \
      && grep -e '1 requirement.* always false' output \
      && 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 COMMIT=68246ae52e4580b23145966db57352fa307377cc ogma-verify-356
    

• Implementation is documented. Details:
  The new module includes documentation for the module and for all top-level functions. The README is updated to document new dependencies.
• Change history is clear.
• Commit messages are clear.
• Changelogs are updated.
• Examples are updated. Details:
  A new example is included that can be used to exemplify the new feature.
• Author is internal or has provided signed CLA.
• Required version bumps are evaluated. Details:
  Bump required; types exposed by the public interface of ogma-core have changed.