Skip to content

Commit 8bfceae

Browse files
committed
[test, WIP] Added tests on LI and SymSize Array for SARIF reports. Removed printing of __klee_posix_wrapped_main function.
1 parent 1969095 commit 8bfceae

25 files changed

Lines changed: 254 additions & 27 deletions

File tree

lib/Core/Executor.cpp

Lines changed: 19 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2614,8 +2614,15 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
26142614
terminateStateOnExit(state);
26152615
} else {
26162616
if (kmodule->inMainModule(*i)) {
2617+
KFunction *callerFunction = kcaller->parent->parent;
2618+
2619+
if (kmodule->WithPOSIXRuntime() &&
2620+
callerFunction->getName() == "__klee_posix_wrapped_main") {
2621+
callerFunction = state.stack.callStack().front().kf;
2622+
}
2623+
26172624
state.eventsRecorder.record(
2618-
new ReturnEvent(locationOf(state), kcaller->parent->parent));
2625+
new ReturnEvent(locationOf(state), callerFunction));
26192626
}
26202627

26212628
state.popFrame();
@@ -6607,14 +6614,17 @@ void Executor::executeMemoryOperation(
66076614
// Obtain memory object
66086615
const ObjectPair baseObjectPair =
66096616
unbound->addressSpace.findObject(baseID);
6610-
// Termiante with source event
6611-
terminateStateOnProgramError(
6612-
*unbound,
6613-
new ErrorEvent(new AllocEvent(baseObjectPair.first->allocSite),
6614-
locationOf(*unbound), StateTerminationType::Ptr,
6615-
"memory error: out of bound pointer"),
6616-
getAddressInfo(*unbound, address));
6617-
return;
6617+
6618+
if (!baseObjectPair.first->isLazyInitialized) {
6619+
// Termiante with source event
6620+
terminateStateOnProgramError(
6621+
*unbound,
6622+
new ErrorEvent(new AllocEvent(baseObjectPair.first->allocSite),
6623+
locationOf(*unbound), StateTerminationType::Ptr,
6624+
"memory error: out of bound pointer"),
6625+
getAddressInfo(*unbound, address));
6626+
return;
6627+
}
66186628
}
66196629

66206630
terminateStateOnProgramError(

lib/Core/Executor.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -256,6 +256,7 @@ class Executor : public Interpreter {
256256

257257
bool hasStateWhichCanReachSomeTarget = false;
258258

259+
/// @brief SARIF report for all exploration paths.
259260
SarifReportJson sarifReport;
260261

261262
/// Return the typeid corresponding to a certain `type_info`

test/SARIF/GSAC/ContextSensitive/pattern.sarif

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,4 +54,4 @@
5454
}
5555
],
5656
"version": "2.1.0"
57-
}
57+
}

test/SARIF/GSAC/EASY02/EASY02.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,4 +20,4 @@ int main() {
2020
// Access is out of bounds
2121
arr[size] = 4; // buffer-overflow
2222
free(arr);
23-
}
23+
}

test/SARIF/GSAC/EASY02/pattern.sarif

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,4 +54,4 @@
5454
}
5555
],
5656
"version": "2.1.0"
57-
}
57+
}

test/SARIF/GSAC/EASY02_fix/EASY02_fix.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,4 +19,4 @@ int main() {
1919
int *arr = malloc(size * sizeof(int));
2020
arr[size - 1] = 4;
2121
free(arr);
22-
}
22+
}

test/SARIF/GSAC/EASY03/pattern.sarif

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,4 +54,4 @@
5454
}
5555
],
5656
"version": "2.1.0"
57-
}
57+
}

test/SARIF/GSAC/FieldSensitive/pattern.sarif

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,4 +54,4 @@
5454
}
5555
],
5656
"version": "2.1.0"
57-
}
57+
}

test/SARIF/GSAC/FlowSensitive/pattern.sarif

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,4 +54,4 @@
5454
}
5555
],
5656
"version": "2.1.0"
57-
}
57+
}

test/SARIF/GSAC/HARD01/pattern.sarif

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -54,4 +54,4 @@
5454
}
5555
],
5656
"version": "2.1.0"
57-
}
57+
}

0 commit comments

Comments
 (0)