Ceagle支持通过属性文件(.prp)、网页版界面或命令行选项来指定属性内容和验证哪个属性。

Ceagle支持验证的属性类型,包括内存安全、程序终止性、整数溢出、代码可达性、assert语句声明的安全属性等5种。

内存安全、程序终止性、整数溢出这3类属性适用于所有C程序,且不需要人工指定属性内容,属于通用属性。

内存安全属性主要包括内存释放安全、内存无野指针和内存无泄露3种。

  • 内存free安全指程序执行过程中不存在多次释放或释放了不合法内存地址的现象。
  • 内存无野指针指程序执行过程中不存在指向不合法内存地址的指针。
  • 内存无泄露指程序执行过程中所有分存的内存要么被指针指向,要么已经被释放,不存在其它情况。

程序终止性指程序所有执行路径总会执行到程序出口,不会无限地执行下去。

整数溢出特指程序中对整数的操作结果都在整数的合法表示范围之内。

代码可达性和assert则需要用户对代码有一定了解,并描述属性内容(如要检查可达性的代码行数、assert的语句表达式),由于代码可达性和assert都可以由Ceagle转化为一个有条件分支语句的error标签的可达性问题,故在指定这两类属性时,只需描述成“error标签。