adding expected generated code. #34
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: CI | |
| on: | |
| push: | |
| pull_request: | |
| defaults: | |
| run: | |
| shell: bash | |
| jobs: | |
| main: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v3 | |
| - uses: cda-tum/setup-z3@main | |
| with: | |
| version: 4.13.3 | |
| - name: Get submodules | |
| run: | | |
| git submodule init | |
| git submodule update --depth 1 | |
| - name: Read submodule commit hashes | |
| id: commits | |
| run: | | |
| C=$(git -C external/llvm-project rev-parse HEAD) | |
| echo "LLVMCOMMIT=$C" >>"$GITHUB_OUTPUT" | |
| C=$(git -C external/FStar rev-parse HEAD) | |
| echo "FSTARCOMMIT=$C" >>"$GITHUB_OUTPUT" | |
| C=$(git -C external/pulse rev-parse HEAD) | |
| echo "PULSECOMMIT=$C" >>"$GITHUB_OUTPUT" | |
| - name: Set-up OCaml | |
| uses: ocaml/setup-ocaml@v3 | |
| with: | |
| ocaml-compiler: 5 | |
| - name: Install some dependencies | |
| run: | | |
| sudo apt update | |
| sudo apt install -y lld | |
| opam install --deps-only external/FStar/fstar.opam | |
| - name: Obtain cached ccache | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: ccache | |
| key: ccache-${{ runner.os }}-${{ runner.arch }} | |
| - name: Set up ccache compiler | |
| run: | | |
| echo "CCACHE_DIR=$(pwd)/ccache" | sudo tee -a $GITHUB_ENV | |
| sudo apt-get install -y ccache | |
| mkdir -p $HOME/bin | |
| echo "PATH=${HOME}/bin:$PATH" | sudo tee -a $GITHUB_ENV | |
| sudo ln -s $(which ccache) $HOME/bin/gcc | |
| sudo ln -s $(which ccache) $HOME/bin/g++ | |
| sudo ln -s $(which ccache) $HOME/bin/cc | |
| sudo ln -s $(which ccache) $HOME/bin/cc1 | |
| sudo ln -s $(which ccache) $HOME/bin/cc1plus | |
| sudo ln -s $(which ccache) $HOME/bin/c++ | |
| - name: Try fetch built LLVM/Clang | |
| id: cache-llvm | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: external/llvm-project/build | |
| key: llvm-${{ runner.os }}-${{ runner.arch }}-${{ steps.commits.outputs.LLVMCOMMIT }} | |
| - name: Build LLVM/Clang | |
| if: steps.cache-llvm.outputs.cache-hit != 'true' | |
| run: | | |
| C2PULSE_BUILD_TYPE=MinSizeRel ./build_clang.sh | |
| - name: Save built LLVM/Clang | |
| if: steps.cache-llvm.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@v4 | |
| with: | |
| path: external/llvm-project/build | |
| key: llvm-${{ runner.os }}-${{ runner.arch }}-${{ steps.commits.outputs.LLVMCOMMIT }} | |
| - name: Try fetch built F* | |
| id: cache-fstar | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: external/FStar | |
| key: FStar-${{ runner.os }}-${{ runner.arch }}-${{ steps.commits.outputs.FSTARCOMMIT }} | |
| - name: Build F* | |
| if: steps.cache-fstar.outputs.cache-hit != 'true' | |
| run: | | |
| eval $(opam env) | |
| make -C external/FStar -skj$(nproc) ADMIT=1 | |
| - name: Save built F* | |
| if: steps.cache-fstar.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@v4 | |
| with: | |
| path: external/FStar | |
| key: FStar-${{ runner.os }}-${{ runner.arch }}-${{ steps.commits.outputs.FSTARCOMMIT }} | |
| - name: Try fetch built Pulse | |
| id: cache-pulse | |
| uses: actions/cache/restore@v4 | |
| with: | |
| path: external/pulse | |
| key: pulse-${{ runner.os }}-${{ runner.arch }}-${{ steps.commits.outputs.FSTARCOMMIT}}-${{ steps.commits.outputs.PULSECOMMIT }} | |
| - name: Build Pulse | |
| if: steps.cache-pulse.outputs.cache-hit != 'true' | |
| run: | | |
| eval $(opam env) | |
| make -C external/pulse -skj$(nproc) ADMIT=1 FSTAR_EXE=$(pwd)/external/FStar/bin/fstar.exe | |
| - name: Save built Pulse | |
| if: steps.cache-pulse.outputs.cache-hit != 'true' | |
| uses: actions/cache/save@v4 | |
| with: | |
| path: external/pulse | |
| key: pulse-${{ runner.os }}-${{ runner.arch }}-${{ steps.commits.outputs.FSTARCOMMIT}}-${{ steps.commits.outputs.PULSECOMMIT }} | |
| - name: Build c2pulse | |
| run: | | |
| eval $(opam env) | |
| ./build.sh | |
| - name: Run tests | |
| run: | | |
| eval $(opam env) | |
| ./run-lit.sh test/*.c | |
| ./run.sh test/*.c | |
| - name: Save ccache | |
| if: always() | |
| uses: actions/cache/save@v4 | |
| with: | |
| path: ccache | |
| key: ccache-${{ runner.os }}-${{ runner.arch }} |