seahorn
v0.1.0 Release (SV-COMP'16)
Seahorn เป็นกรอบการวิเคราะห์อัตโนมัติสำหรับภาษาที่ใช้ LLVM เวอร์ชันนี้รวบรวมกับ LLVM 14
คุณสมบัติบางอย่างที่รองรับคือ
Seahorn ได้รับการพัฒนาเป็นหลักเป็นกรอบในการดำเนินการวิจัยในการตรวจสอบอัตโนมัติ เฟรมเวิร์กให้ส่วนประกอบมากมายที่สามารถรวมเข้าด้วยกันได้หลายวิธี อย่างไรก็ตามมันไม่ได้เป็นเครื่องมือการวิเคราะห์แบบคงที่ "นอกกรอบ"
เครื่องมือและตัวอย่างการวิเคราะห์จำนวนมากมาพร้อมกับเฟรมเวิร์ก เรากำลังมองหาแอปพลิเคชันใหม่อย่างต่อเนื่องและให้การสนับสนุนผู้ใช้ใหม่ สำหรับข้อมูลเพิ่มเติมเกี่ยวกับสิ่งที่เกิดขึ้นให้ตรวจสอบบล็อก (อัปเดตไม่บ่อยนัก) ของเรา
Seahorn มีการแจกจ่ายภายใต้ใบอนุญาต BSD ที่แก้ไขแล้ว ดู License.txt สำหรับรายละเอียด
Seahorn ให้สคริปต์ Python ที่เรียกว่า sea เพื่อโต้ตอบกับผู้ใช้ ได้รับโปรแกรม C ที่มีคำอธิบายประกอบด้วยการยืนยันผู้ใช้เพียงแค่ต้องพิมพ์: sea pf file.c
ผลลัพธ์ของ sea-pf นั้น unsat หากการยืนยันทั้งหมดถือไว้ sat หากมีการละเมิดใด ๆ
ตัวเลือก pf บอกให้ Seahorn แปล file.c เป็น LLVM bitcode สร้างชุดของเงื่อนไขการตรวจสอบ (VCs) และในที่สุดก็แก้ปัญหาได้ ตัวแก้ปัญหาส่วนหลังหลักคือตัวเว้นวรรค
คำสั่ง pf ให้ตัวเลือกต่อไปนี้:
--show-invars : แสดงค่าคงที่ที่คำนวณได้หากคำตอบ unsat
--cex=FILE : เก็บตัวอย่างเคาน์เตอร์ใน FILE หากคำตอบถูก sat
-g : รวบรวมด้วยข้อมูลการดีบักสำหรับตัวอย่างที่สามารถติดตามได้มากขึ้น
--step=large : การเข้ารหัสขั้นตอนขนาดใหญ่ ความสัมพันธ์การเปลี่ยนแปลงแต่ละครั้งสอดคล้องกับชิ้นส่วนที่ปราศจากลูป
--step=small : การเข้ารหัสขั้นตอนเล็ก ๆ ความสัมพันธ์การเปลี่ยนแปลงแต่ละครั้งสอดคล้องกับบล็อกพื้นฐาน
--track=reg : โมเดล (จำนวนเต็ม) ลงทะเบียนเท่านั้น
--track=ptr : รุ่นลงทะเบียนและพอยน์เตอร์ (แต่ไม่ใช่เนื้อหาหน่วยความจำ)
--track=mem : โมเดลทั้งสเกลาร์พอยน์เตอร์และเนื้อหาหน่วยความจำ
--inline : Inlines โปรแกรมก่อนการตรวจสอบ
--crab : invariants ฉีดใน spacer ที่สร้างขึ้นโดยเครื่องมือที่ใช้การตีความบทคัดย่อปู อ่านที่นี่เพื่อดูรายละเอียดเกี่ยวกับตัวเลือกปูทั้งหมด (คำนำหน้า --crab ) คุณสามารถดูว่าค่าคงที่ใดที่จะอนุมานโดย Crab โดยการพิมพ์ตัวเลือก --log=crab
--bmc : ใช้เครื่องยนต์ BMC
sea pf เป็นไปป์ไลน์ที่เรียกใช้หลายคำสั่ง แต่ละส่วนของท่อสามารถเรียกใช้แยกกันได้เช่นกัน:
sea fe file.c -o file.bc : Frontend Seahorn แปลโปรแกรม C เป็น BitCode LLVM ที่ได้รับการปรับปรุงรวมถึงการแปลงแบบผสม -semantics
sea horn file.bc -o file.smt2 : Seahorn สร้างเงื่อนไขการตรวจสอบจาก file.bc และส่งออกในรูปแบบ Smt -Lib V2 ผู้ใช้สามารถเลือกระหว่างรูปแบบการเข้ารหัสที่แตกต่างกันด้วยความแม่นยำหลายระดับโดยการเพิ่ม:
--step={small,large,fsmall,flarge} flarge small คือการเข้ารหัสขั้นตอนเล็ก ๆ , large คือการเข้ารหัสแบบบล็อกขนาดใหญ่, fsmall เป็นขั้นตอนเล็ก ๆ ที่เข้ารหัสการสร้างข้อกำหนดของฮอร์นแบน (เช่นมันสร้างระบบการเปลี่ยนผ่าน
--track={reg,ptr,mem} โดยที่ reg เฉพาะรุ่น integer scalars, ptr models reg และที่อยู่ตัวชี้และ mem รุ่น ptr และเนื้อหาหน่วยความจำ
sea smt file.c -o file.smt2 : สร้าง CHC ในรูปแบบ SMT -LIB2 เป็นนามแฝงสำหรับ sea fe ตามด้วย sea horn Command sea pf เป็นนามแฝงสำหรับ sea smt --prove
sea clp file.c -o file.clp : สร้าง CHC ในรูปแบบ CLP
sea lfe file.c -o file.ll : รัน Front -end ดั้งเดิม
หากต้องการดูคำสั่งทั้งหมดให้พิมพ์ sea --help หากต้องการดูตัวเลือกสำหรับแต่ละคำสั่ง cmd (เช่น horn ) ให้พิมพ์ sea CMD --help (เช่น sea horn --help )
Seahorn ไม่ได้ใช้ปูตามค่าเริ่มต้น ในการเปิดใช้งานปูให้เพิ่มตัวเลือก --crab ไปยังคำสั่ง sea
ล่ามบทคัดย่อนั้นเป็นค่าเริ่มต้นภายในกระบวนการและใช้โดเมนโซนเป็นโดเมนนามธรรมเชิงตัวเลข ตัวเลือกเริ่มต้นเหล่านี้น่าจะเพียงพอสำหรับผู้ใช้ปกติ สำหรับนักพัฒนาหากคุณต้องการใช้โดเมนนามธรรมอื่น ๆ ที่คุณต้องการ:
cmake -DCRAB_USE_LDD=ON -DCRAB_USE_ELINA=ONsea ด้วยตัวเลือก --crab-dom=DOM โดยที่ DOM สามารถ:int สำหรับช่วงเวลาterm-int สำหรับช่วงเวลาที่มีฟังก์ชั่นที่ไม่ได้ตีความboxes : สำหรับช่วงเวลาที่แยกออกจากกันoct สำหรับ octagonspk สำหรับ Polyhedra ในการใช้การวิเคราะห์ระหว่างกระบวนการปูคุณต้องเรียกใช้ sea ด้วยตัวเลือก --crab-inter
โดยค่าเริ่มต้นล่ามนามธรรมเพียงเหตุผลเกี่ยวกับตัวแปรสเกลาร์ (เช่นการลงทะเบียน LLVM) เรียกใช้ sea ด้วยตัวเลือก --crab-track=mem --crab-singleton-aliases=true กับเหตุผลเกี่ยวกับเนื้อหาหน่วยความจำ
ปูส่วนใหญ่เป็นเส้นทางที่ไม่รู้สึกในขณะที่ตัวเว้นวรรคผู้แก้ปัญหาเสียงแตรของเรานั้นมีความอ่อนไหวต่อเส้นทาง แม้ว่าการวิเคราะห์ที่ไม่ได้รับความรู้สึกจะมีประสิทธิภาพมากขึ้น สิ่งนี้กระตุ้นการตัดสินใจของเราในการใช้งานปูแรก (ถ้าตัวเลือก --crab ) จากนั้นส่งผ่านค่าคงที่ที่สร้างขึ้นไปยัง spacer ขณะนี้มีสองวิธีสำหรับตัวเว้นวรรคที่จะใช้ค่าคงที่ที่สร้างโดยปู ตัวเลือก sea --horn-use-invs=VAL บอก spacer วิธีใช้ค่าคงที่เหล่านั้น:
VAL เท่ากับ bg จะใช้ค่าคงที่เพียงเพื่อช่วย spacer ในการพิสูจน์บทแทรกเป็นอุปนัยVAL เท่ากับ always พฤติกรรมจะคล้ายกับ bg แต่นอกจากนี้ค่าคงที่ยังใช้เพื่อช่วยให้ spacer บล็อกเคาน์เตอร์ ค่าเริ่ม bg แน่นอนว่าถ้าปูสามารถพิสูจน์ได้ว่าโปรแกรมนั้นปลอดภัยแล้ว Spacer จะไม่เสียค่าใช้จ่ายเพิ่มเติมใด ๆ
คุณสมบัติจะถือว่าเป็นการยืนยัน Seahorn ให้คำสั่งการยืนยันแบบคงที่ sassert ดังแสดงในตัวอย่างต่อไปนี้
/* verification command: sea pf --horn-stats test.c */
#include "seahorn/seahorn.h"
extern int nd ();
int main ( void ) {
int k = 1 ;
int i = 1 ;
int j = 0 ;
int n = nd ();
while ( i < n ) {
j = 0 ;
while ( j < i ) {
k += ( i - j );
j ++ ;
}
i ++ ;
}
sassert ( k >= n );
} ภายใน Seahorn ตามอนุสัญญา SV-comp ของการเข้ารหัสตำแหน่งข้อผิดพลาดโดยการเรียกไปยังฟังก์ชั่นข้อผิดพลาดที่กำหนด __VERIFIER_error() Seahorn ส่งคืน unsat เมื่อ __VERIFIER_error() ไม่สามารถเข้าถึงได้และโปรแกรมถือว่าปลอดภัย Seahorn กลับมา sat เมื่อ __VERIFIER_error() สามารถเข้าถึงได้และโปรแกรมไม่ปลอดภัย วิธี sassert() ถูกกำหนดไว้ใน seahorn/seahorn.h
นอกเหนือจากการพิสูจน์คุณสมบัติหรือการผลิตตัวอย่างบางครั้งก็มีประโยชน์ในการตรวจสอบรหัสภายใต้การวิเคราะห์เพื่อให้เข้าใจถึงความซับซ้อนของมัน สำหรับสิ่งนี้ Seahorn ให้ sea inspect ตัวอย่างเช่นได้รับโปรแกรม C ex.c Type:
sea inspect ex.c --sea-dsa=cs+t --mem-dot
ตัวเลือก --sea-dsa=cs+t เปิดใช้งานการวิเคราะห์บริบทใหม่-ไวรัส SEA-DSA ที่ไวต่อการพิมพ์ที่อธิบายไว้ใน FMCAD19 คำสั่งนี้สร้างไฟล์ FUN.mem.dot สำหรับแต่ละฟังก์ชั่น FUN ในโปรแกรมอินพุต ในการแสดงภาพกราฟของฟังก์ชั่นหลักให้ใช้อินเตอร์เฟส web graphivz หรือคำสั่งต่อไปนี้:
$ dot -Tpdf main.mem.dot -o main.mem.pdfรายละเอียดเพิ่มเติมเกี่ยวกับกราฟหน่วยความจำอยู่ในที่เก็บ Seadsa: ที่นี่
ใช้ sea inspect --help ช่วยดูตัวเลือกทั้งหมด ปัจจุบันตัวเลือกที่มีอยู่คือ:
sea inspect --profiler พิมพ์จำนวนฟังก์ชั่นบล็อกพื้นฐานลูป ฯลฯsea inspect --mem-callgraph-dot เพื่อจัดรูป dot กราฟการโทรที่สร้างโดย SEADSAsea inspect --mem-callgraph-stats พิมพ์ไปยังเอาต์พุตมาตรฐานบางส่วนเกี่ยวกับการก่อสร้างกราฟการโทรที่ทำโดย SEADSAsea inspect --mem-smc-stats พิมพ์จำนวนการเข้าถึงหน่วยความจำที่สามารถพิสูจน์ได้ว่าปลอดภัยโดย SEADSAวิธีที่ง่ายที่สุดในการเริ่มต้นกับ Seahorn คือการกระจายตัวของนักเทียบท่า
$ docker pull seahorn/seahorn-llvm10:nightly
$ docker run --rm -it seahorn/seahorn-llvm10:nightly เริ่มต้นด้วยการสำรวจว่าคำสั่ง sea สามารถทำอะไรได้บ้าง:
$ sea --help
$ sea pf --help แท็ก nightly จะได้รับการรีเฟรชโดยอัตโนมัติทุกวันและมีเวอร์ชันการพัฒนาล่าสุด เรารักษาแท็กอื่น ๆ ทั้งหมด (ที่ต้องมีการอัปเดตด้วยตนเอง) ไม่บ่อยนัก ตรวจสอบวันที่บน DockerHub และบันทึกปัญหาเกี่ยวกับ GitHub หากพวกเขาค้างมากเกินไป
ตัวอย่างเพิ่มเติมและตัวเลือกการกำหนดค่าอยู่ในบล็อก บล็อกได้รับการอัปเดตไม่บ่อยนัก โดยเฉพาะอย่างยิ่งการเปลี่ยนแปลงตัวเลือกคุณสมบัติจะถูกเพิ่มขึ้นมีการเพิ่มสิ่งใหม่ ๆ หากคุณพบปัญหาในบล็อกโปรดแจ้งให้เราทราบ อย่างน้อยเราจะอัปเดตโพสต์บล็อกเพื่อระบุว่าไม่คาดว่าจะทำงานกับรหัสเวอร์ชันล่าสุด
นอกจากนี้คุณยังสามารถติดตั้งด้วยตนเองโดย:
ทำตามคำแนะนำในไฟล์ Docker Dockerfile: docker/seahorn-builder.Dockerfile
หากสิ่งนี้ไม่ทำงานให้เรียกใช้:
$ wget https://apt.llvm.org/llvm.sh
$ chmod +x llvm.sh
$ sudo ./llvm.sh 14
$ apt download libpolly-14-dev && sudo dpkg --force-all -i libpolly-14-dev *คำสั่ง 3 คำแรกจะติดตั้ง LLVM 14, 4th จะติดตั้ง libpolly ซึ่งถูกละเว้นอย่างไม่ถูกต้องจาก LLVM 14 (แต่รวมอยู่ในรุ่นต่อ ๆ ไป)
ถัดไปทำตามคำแนะนำในไฟล์ Docker ด้านบน
ข้อมูลจากจุดนี้ไปมีไว้สำหรับนักพัฒนาเท่านั้น หากคุณต้องการมีส่วนร่วมใน Seahorn ให้สร้างเครื่องมือของคุณเองตามมันหรือเพียงแค่สนใจว่ามันทำงานภายในอ่านต่อไปเรื่อย ๆ
Seahorn ต้องการ LLVM, Z3 และ Boost ห้องสมุดเวอร์ชันที่แน่นอนเปลี่ยนไปเรื่อย ๆ แต่ CMake Craft ใช้เพื่อตรวจสอบเวอร์ชันที่เหมาะสม
ในการระบุเวอร์ชันเฉพาะของการพึ่งพาใด ๆ ให้ใช้ <PackageName>_ROOT และ/หรือ <PackageName>_DIR (ดู find_package () สำหรับรายละเอียด) ตัวแปร cmake
Seahorn แบ่งออกเป็นหลายองค์ประกอบที่อาศัยอยู่ในที่เก็บข้อมูลที่แตกต่างกัน (ภายใต้องค์กร Seahorn) กระบวนการสร้างจะตรวจสอบทุกอย่างโดยอัตโนมัติตามความจำเป็น สำหรับคำแนะนำการสร้างปัจจุบันให้ตรวจสอบสคริปต์ CI
นี่คือขั้นตอนทั่วไป อย่า ใช้พวกเขา อ่านต่อไปเพื่อวิธีที่ดีกว่า:
cd seahorn ; mkdir build ; cd build (ไดเรกทอรี Build สามารถอยู่นอกไดเรกทอรีต้นฉบับได้)cmake -DCMAKE_INSTALL_PREFIX=run ../ ( จำเป็นต้องติดตั้ง! )cmake --build . --target extra && cmake .. (ส่วนประกอบโคลนที่อาศัยอยู่ที่อื่น)cmake --build . --target crab && cmake .. (ห้องสมุดปูโคลน)cmake --build . --target install (สร้างและติดตั้งทุกอย่างภายใต้ run )cmake --build . --target test-all (เรียกใช้การทดสอบ)หมายเหตุ : จำเป็นต้อง ติด ตั้งเป้าหมายเพื่อทดสอบการทำงาน!
สำหรับประสบการณ์การพัฒนาที่ได้รับการปรับปรุง:
clanglld linkercompile_commands.json บน Linux เราขอแนะนำการกำหนดค่า cmake ต่อไปนี้:
$ cd build
$ cmake -DCMAKE_INSTALL_PREFIX=run
-DCMAKE_BUILD_TYPE=RelWithDebInfo
-DCMAKE_CXX_COMPILER="clang++-14"
-DCMAKE_C_COMPILER="clang-14"
-DSEA_ENABLE_LLD=ON
-DCMAKE_EXPORT_COMPILE_COMMANDS=1
../
-DZ3_ROOT=<Z3_ROOT>
-DLLVM_DIR=<LLMV_CMAKE_DIR>
-GNinja
$ (cd .. && ln -sf build/compile_commands.json .)
โดยที่ <Z3_ROOT เป็นไดเรกทอรีที่มีการกระจายไบนารี Z3 และ LLMV_CMAKE_DIR เป็นไดเรกทอรีที่มี LLVMConfig.cmake
ตัวเลือกทางกฎหมายอื่น ๆ สำหรับ CMAKE_BUILD_TYPE คือ Debug และ Coverage โปรดทราบว่า CMAKE_BUILD_TYPE จะต้องเข้ากันได้กับอันที่ใช้ในการรวบรวม LLVM โดยเฉพาะอย่างยิ่งคุณจะต้องมี Debug สร้าง LLVM เพื่อรวบรวม SeaHorn ในโหมด `debug ** ตรวจสอบให้แน่ใจว่าคุณมีความอดทนพื้นที่ดิสก์และเวลามากมายหากคุณตัดสินใจไปเส้นทางนี้
อีกทางเลือกหนึ่งโครงการสามารถกำหนดค่าได้โดยใช้ CMake ที่ตั้งไว้ล่วงหน้า ในการทำเช่นนี้เพียงเรียกใช้คำสั่งต่อไปนี้:
$ cmake --preset < BUILD_TYPE > - < PRESET_NAME > ในการกำหนดค่า cmake โดยที่ <BUILD_TYPE> เป็นหนึ่งใน: Debug , RelWithDebInfo หรือ Coverage และ <PRESET_NAME> เป็นค่าที่ตั้งไว้ล่วงหน้าที่คุณต้องการใช้ ค่าที่ตั้งล่วงหน้าที่มีอยู่ในปัจจุบันคือ: jammy ค่าที่ตั้งไว้ล่วงหน้าเหล่านี้สันนิษฐานว่าคุณติดตั้ง Z3 ใน /opt/z3-4.8.9 และติดตั้ง yices ใน /opt/yices-2.6.1
สิ่งนี้จะช่วยให้โครงการได้รับการกำหนดค่าและรวบรวมภายในรหัส VS โดยใช้ส่วนขยายเครื่องมือ CMake
หากคุณต้องการใช้การตั้งค่าการรวบรวมที่แตกต่างกันหรือหากคุณติดตั้ง Z3 หรือ Yices ในไดเรกทอรีอื่น ๆ คุณจะต้องสร้างไฟล์ CMakeUserPresets.json ของคุณเองด้วยค่าที่ตั้งไว้ล่วงหน้าของคุณเอง
อย่ารวม -DSEA_ENABLE_LLD=ON คอมไพเลอร์เริ่มต้นเป็นเสียงดังก้องดังนั้นคุณอาจไม่จำเป็นต้องตั้งค่าไว้อย่างชัดเจน
Seahorn ให้ส่วนประกอบหลายอย่างที่ถูกโคลนและติดตั้งโดยอัตโนมัติผ่านเป้าหมาย extra ส่วนประกอบเหล่านี้สามารถใช้งานได้โดยโครงการอื่น ๆ นอก Seahorn
Sea-dsa: git clone https://github.com/seahorn/sea-dsa.git
sea-dsa เป็นการวิเคราะห์กอง DSA ใหม่ ซึ่งแตกต่างจาก llvm-dsa , sea-dsa นั้นมีความอ่อนไหวตามบริบทดังนั้นจึงสามารถสร้างพาร์ติชันที่ละเอียดกว่าของกองฮีปต่อหน้าฟังก์ชั่น
หอย: git clone https://github.com/seahorn/crab-llvm.git
clam ให้ค่าคงที่อุปนัยโดยใช้เทคนิคการตีความนามธรรมไปยังส่วนที่เหลือของแบ็กเอนด์ของ Seahorn
llvm-seahorn: git clone https://github.com/seahorn/llvm-seahorn.git
llvm-seahorn ให้บริการที่เหมาะกับการตรวจสอบของ InstCombine และ IndVarSimplify LLVM ผ่านเช่นเดียวกับ LLVM ผ่านเพื่อแปลงค่าที่ไม่ได้กำหนดเป็นการโทรแบบไม่ใช้งาน
Seahorn ไม่ได้มาพร้อมกับ Clang เวอร์ชันของตัวเองและคาดว่าจะพบทั้งในไดเรกทอรี Build ( run/bin ) หรือในเส้นทาง ตรวจสอบให้แน่ใจว่ารุ่นของเสียงดังก้องตรงกับเวอร์ชันของ LLVM ที่ใช้ในการรวบรวม Seahorn (ปัจจุบัน LLVM14) วิธีที่ง่ายที่สุดในการจัดหา Clang เวอร์ชันที่เหมาะสมคือการดาวน์โหลดจาก LLVM.Org โดยไม่ทำอะไรสักแห่งและสร้างลิงค์สัญลักษณ์ไปยัง clang และ clang++ ใน run/bin
$ cd seahorn/build/run/bin
$ ln -s < CLANG_ROOT > /bin/clang clang
$ ln -s < CLANG_ROOT > /bin/clang++ clang++ โดยที่ <CLANG_ROOT> เป็นที่ตั้งของเสียงดังก้อง
การทดสอบโครงสร้างพื้นฐานขึ้นอยู่กับแพ็คเกจ Python หลายแห่ง สิ่งเหล่านี้มีการพึ่งพาของตัวเอง หากคุณไม่สามารถคิดออกได้ให้ใช้ Docker แทน
$ pip install lit OutputCheck networkx pygraphviz เราสามารถใช้ gcov และ lcov เพื่อสร้างข้อมูลการทดสอบสำหรับ Seahorn ในการสร้างด้วยการเปิดใช้งานความคุ้มครองเราจำเป็นต้องเรียกใช้การสร้างภายใต้ไดเรกทอรีที่แตกต่างกันและตั้งค่า CMAKE_BUILD_TYPE เพื่อ Coverage ในระหว่างการกำหนดค่า CMake
ขั้นตอนตัวอย่างสำหรับการสร้างรายงานความครอบคลุมสำหรับเป้าหมาย test-opsem :
mkdir coverage; cd coverage สร้างและป้อนไดเรกทอรี Build Coveragecmake -DCMAKE_BUILD_TYPE=Coverage <other flags as you wish> ../cmake --build . --target test-opsem ตอนนี้ไฟล์ .gcda และ .gcno ควรสร้างในไดเรกทอรี CMakeFiles ที่เกี่ยวข้องlcov -c --directory lib/seahorn/CMakeFiles/seahorn.LIB.dir/ -o coverage.info รวบรวมข้อมูลความคุ้มครองจากโมดูลที่ต้องการหากใช้ clang เป็นคอมไพเลอ llvm-gcov.sh แทน gcc #! /bin/bash
exec llvm-cov gcov " $@ " $ chmod +x llvm-gcov.sh จากนั้นผนวก --gcov-tool <path_to_wrapper_script>/llvm-gcov.sh ไปยังคำสั่ง lcov -c ... 6. แยกข้อมูลจากไดเรกทอรีที่ต้องการและสร้างรายงาน HTML:
lcov --extract coverage.info " */lib/seahorn/* " -o lib.info
lcov --extract coverage.info " */include/seahorn/* " -o header.info
cat header.info lib.info > all.info
genhtml all.info --output-directory coverage_report จากนั้นเปิด coverage_report/index.html ในเบราว์เซอร์เพื่อดูรายงานความครอบคลุม
ดู scripts/coverage สำหรับสคริปต์ที่ใช้โดย CI รายงานความครอบคลุมสำหรับการสร้างยามค่ำคืนมีอยู่ที่ Codecov
ฐานข้อมูลการรวบรวมสำหรับโครงการ Seahorn และโครงการย่อยทั้งหมดถูกสร้างขึ้นโดยใช้ -DCMAKE_EXPORT_COMPILE_COMMANDS=ON ตัวเลือกสำหรับ cmake
วิธีที่ง่ายในการรับการจัดทำดัชนีรหัสเพื่อทำงานกับการสนับสนุนฐานข้อมูลการรวบรวมคือการเชื่อมโยงไฟล์ compilation_database.json ลงในไดเรกทอรีโครงการหลักและทำตามคำแนะนำเฉพาะกับตัวแก้ไขของคุณ
lsp-ui กับ clangd ซึ่งมีอยู่ใน Spacemacs พัฒนาสาขา สำหรับคู่มือโดยละเอียดสำหรับเวิร์กโฟลว์ระยะไกลพร้อมการตรวจสอบการกำหนดค่า clion clion
ใช้ส้อมของเมนเฟิลของเรา อย่าพลาดการกำหนดค่าตัวอย่าง
