Ceagle支持验证程序中的某行代码是否可达,要使用这一功能,请指定需要验证可达性的代码,然后在Ceagle中向验证任务添加代码可达性属性。指定需要验证可达性的代码的方式包括插入C语言标签、给出行号或直接在程序代码中选择(选择代码的功能仅被网页版支持)。

网页版

使用网页版的属性选择面板进行属性选择:

面板选择

命令行版

# 验证foo.c的第15行是否可达
ceagle --property.reach=foo.c:15 foo.c