轉載至: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
-
- repo sync
KZM-ARM11-01
- ARM1136 532MHz (Freescale i.MX31) based evaluation board
- 通過 QEMU 模拟和驗證
-
- make kzm_simulation_release_xml_defconfig
-
- TOOLPREFIX=arm-none-eabi- ARCH=arm make
-
- make simulate-kzm
參考執行輸出:這時候可以準備執行 pkill qemu-system-arm... <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.
seL4 Tests
- BSD License
- Directory
-
- apps/sel4test-driver
-
- apps/sel4test-tests
seL4 Verification
- 取得原始程式碼
-
- mkdir -p verification &&cd verification
-
- repo init -u https://github.com/seL4/verification-manifest.git
-
- repo sync
- 準備相關套件
-
- 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,得自網路抓取
-
- cd l4v
-
- mkdir -p ~/.isabelle/etc
-
- cp -i misc/etc/settings ~/.isabelle/etc/settings
-
- ./isabelle/bin/isabelle components -a
- 遇到以下的小錯誤,可繼續
-
- dirname: 缺少運算元
-
- Try 'dirname --help' for more information.
- 這過程相當耗時,解決方式為預先將檔案置放於 ~/.isabelle/contrib/ 目錄
-
- cvc3-2.4.1
-
- e-1.8
-
- exec_process-1.0.3
-
- Haskabelle-2013
-
- jdk-7u40
-
- jedit_build-20131106
-
- jfreechart-1.0.14-1
-
- kodkodi-1.5.2
-
- polyml-5.5.1-1
-
- scala-2.10.3
-
- spass-3.8ds
-
- z3-3.2
-
- xz-java-1.2-1
-
- ProofGeneral-4.2
- 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
- 執行證明 (相當慢)
- ./run_tests
參考輸出:
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