Automated String Constraints Solving for Programs Containing String Manipulation Functions

解决各种各样的限制的能力是自动限制解答者的一个主要因素。最面向对象的语言把特性绳当作被绳图书馆功能操作的一种原始数据类型。大多数限制解答者在他们的输入限制上有限制，例如限制的表现力或解决混合限制的能力的缺乏上的强壮的限制。这些限制为包含字符串和字符串操作函数的程序在程序分析技术上妨碍适用的自动化限制解答者。我们建议一条途径自动地解决包含绳和绳操作功能的程序限制。基于字符数组模型，我们设计包含原始操作精确描述通常使用的字符串操作函数的限制的一种限制语言。和数字限制的翻译的绳限制然后被一个二阶段的测试产生过程解决：第一，一个部分解决方案被获得满足位置变量的算术限制，并且解决方案被利用简化字符串限制进纯字符数组限制；第二，纯数组限制被一个现成的数组特定的理论解决基于的限制解答者。我们把途径集成到一个自动化严峻的工具支持绳测试用例的产生，然后执行实验。实验的结果证明建议途径的集成支持存在测试工具，和综合工具的严峻的范围有与一个存在的绳解答者相比处理特定的绳操作功能的一个优点。