C++: Add a new test to test assignment certainty (i.e., whether the entire buffer is overwritten).

This commit is contained in:
Mathias Vorreiter Pedersen
2026-05-12 11:11:44 +01:00
parent b753e7d228
commit e77d85f23e
3 changed files with 86 additions and 0 deletions

View File

@@ -0,0 +1,64 @@
void use(...);
void test1() {
int x = 0; // $ certain="SSA def(&x)" certain="SSA def(x)"
use(x);
x = 1; // $ certain="SSA def(x)"
use(x);
int* p = &x; // $ certain="SSA def(&p)" certain="SSA def(p)" certain="SSA def(*p)"
use(p);
*p = 2; // $ certain="SSA def(*p)"
use(p);
p = nullptr; // $ certain="SSA def(p)" certain="SSA def(*p)"
use(p);
*p = 2; // $ uncertain="SSA def(*p)"
use(p);
}
void test2(bool b) { // $ certain="SSA def(&b)" certain="SSA def(b)"
{
int x; // $ certain="SSA def(&x)"
if(b) {
x = 0; // $ certain="SSA def(x)"
} else {
x = 1; // $ certain="SSA def(x)"
}
use(x); // $ uncertain="SSA phi(x)"
}
{
int x; // $ certain="SSA def(&x)" certain="SSA def(x)"
if(b) {
x = 0; // $ certain="SSA def(x)"
} else {
}
use(x); // $ uncertain="SSA phi(x)"
}
{
int x; // $ certain="SSA def(&x)" certain="SSA def(x)"
int* p = &x; // $ certain="SSA def(&p)" certain="SSA def(p)" certain="SSA def(*p)"
if(b) {
*p = 0; // $ certain="SSA def(*p)"
} else {
*(p + 1) = 1; // $ uncertain="SSA def(*p)"
}
use(p); // $ uncertain="SSA phi(*p)"
}
}
void test3(bool b) { // $ certain="SSA def(&b)" certain="SSA def(b)"
for(int i = 0; i < 10;) { // $ certain="SSA def(&i)" certain="SSA def(i)" uncertain="SSA phi(i)"
if(b) {
++i; // $ certain="SSA def(i)"
}
use(i); // $ uncertain="SSA phi(i)"
}
}

View File

@@ -0,0 +1,22 @@
import cpp
import utils.test.InlineExpectationsTest
import semmle.code.cpp.dataflow.new.DataFlow::DataFlow
bindingset[s]
string quote(string s) { if s.matches("% %") then result = "\"" + s + "\"" else result = s }
module AsDefinitionTest implements TestSig {
string getARelevantTag() { result = ["certain", "uncertain"] }
predicate hasActualResult(Location location, string element, string tag, string value) {
exists(Ssa::Definition d |
location = d.getLocation() and
element = d.toString() and
value = quote(d.toString())
|
if d.isCertain() then tag = "certain" else tag = "uncertain"
)
}
}
import MakeTest<AsDefinitionTest>