Run check on a C source file and return analysis results

Create a verification sandbox for a specific function

Retrieve runtime error alarms from analysis

Retrieve WP proof goals from analysis

Inject ACSL annotations into a project

Load or reload a Frama-C project from source files

Run EVA analysis on a sandbox function

Run WP prover on a sandbox function

Check server health and Frama-C compatibility

Execute one step of program verification FSM