转载至：https://source2014.hackpad.com/seL4--IJItb9IDncR
取得核心程式碼
- 預先設定好 Toolchain: http://sel4.systems/Download/DebianToolChain.pml
- 取得原始程式碼: http://sel4.systems/Download/
- mkdir -p seL4-test && cd seL4-test
- repo init -u https://github.com/seL4/sel4test-manifest.git
KZM-ARM11-01
- ARM1136 532MHz (Freescale i.MX31) based evaluation board
- make kzm_simulation_release_xml_defconfig
- TOOLPREFIX=arm-none-eabi- ARCH=arm make
參考執行輸出:
...
<testcase classname="sel4test" name="TEST_IPC0001">
INFO :sel4utils_elf_load_record_regions:276: * Loading segment 00008000-->000445e4
INFO :sel4utils_elf_load_record_regions:276: * Loading segment 0004d000-->00165df8
<system-out> TEST_IPC0001
</system-out>
...
<testcase classname="sel4test" name="TEST_CNODEOP00012">
INFO :sel4utils_elf_load_record_regions:276: * Loading segment 00008000-->000445e4
INFO :sel4utils_elf_load_record_regions:276: * Loading segment 0004d000-->00165df8
<system-out> TEST_CNODEOP0001
</system-out>
</testcase>
</testsuite>
126/126 tests passed.
All is well in the universe.
這時候可以準備執行 pkill qemu-system-arm
seL4 Tests
seL4 Verification
- mkdir -p verification &&cd verification
- repo init -u https://github.com/seL4/verification-manifest.git
- sudo apt-get install libwww-perl texlive-bibtex-extra texlive-latex-extra
- sudo apt-get install python-lxml
- sudo apt-get install mlton python-tempita
- 由於 Isabelle 需要額外的套件如 jdk7, jfreechart, scala, xz-java，得自網路抓取
- cp -i misc/etc/settings ~/.isabelle/etc/settings
- ./isabelle/bin/isabelle components -a
- Try 'dirname --help' for more information.
- 這過程相當耗時，解決方式為預先將檔案置放於 ~/.isabelle/contrib/ 目錄
- Automated theorem proving! 確保可用的記憶體 > 2 GB
- ./isabelle/bin/isabelle jedit -bf
- ./isabelle/bin/isabelle build -bv HOL-Word
ML_PLATFORM="x86_64-linux"
ML_HOME="/home/jserv/.isabelle/contrib/polyml-5.5.1-1/x86_64-linux"
ML_SYSTEM="polyml-5.5.1"
ML_OPTIONS="-H 2000"
Session Pure/Pure
Session HOL/HOL (main)
Session HOL/HOL-Word (main)
Building Pure ...
Finished Pure (1:36:49 elapsed time, 0:00:51 cpu time, factor 0.00)
Building HOL ...
HOL: theory Code_Generator
HOL: theory HOL
HOL: theory SATz
Running 31 test(s)...
running isabelle ... pass
running CamkesAdlSpec ... pass
running CamkesGlueSpec ...
...
running CamkesAdlSpec ... FAILED *
running CamkesGlueSpec ... FAILED *
所有的 Test 都是一定會過 ?
要安裝 mlton (已送 pull request)
Issues
- arm926ej_s is not officially supported
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
