check_c
Read-onlyIdempotent
Verify C functions against written contracts with ESBMC or CBMC, returning valid results or failing-call values; unclaused functions are checked for overflow, division by zero, and pointer safety.
Instructions
Check each function of a C file (text or a file path) against the
contract written in its clauses (see parse_c), one call at a time, with
ESBMC or CBMC (whichever is installed): valid, or invalid with the values
of a failing call. A function with no clause is checked as code alone
(safe: no overflow, division by zero, or bad pointer). functions: the
ones to check (default: all).
Tool call template
This tool declares no required parameters. Add optional parameters from the input schema as needed.
{
"id": 1,
"jsonrpc": "2.0",
"method": "tools/call",
"params": {
"arguments": {},
"name": "check_c"
}
}Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| path | No | ||
| text | No | ||
| timeout | No | ||
| functions | No |