Change Details

If a constraint violation was found the already applied other constraints were already added and analysis was continuing on this path even if bug is reported. After the fix the error node is added as the last node on the current path.

The checker applies constraints in a sequence and adds new nodes for these states. If a constraint violation is found this sequence should be stopped with a sink (error) node. Instead the `generateErrorNode` did add a new error node as a new branch that is parallel to the other node sequence, the other branch was not stopped and analysis was continuing on that invalid branch. To add an error node after any previous node a new version of `generateErrorNode` is needed, this function is added here and used by `StdLibraryFunctionsChecker`. The added test executes a situation where the checker adds a number of constraints before it finds a constraint violation.

The checker applies constraints in a sequence and adds new nodes for these states. If a constraint violation was found the already applied other constraints were already added is found this sequence should be stopped with a sink (error) node. Instead the `generateErrorNode` did add a new error node as a new branch that is parallel to the other node sequence, the other branch was not stopped and analysis was continuing on this path even if bug is reported.that invalid branch. To add an error node after any previous node a new version of `generateErrorNode` is needed, After the fix the error node is added as the last node on the current paththis function is added here and used by `StdLibraryFunctionsChecker`. The added test executes a situation where the checker adds a number of constraints before it finds a constraint violation.