atelierb_read_file
Returns verbatim content of B source files, C code, or Makefiles from the workspace for inspection. For .pmi files, maps each entry to its proof obligation labels.
Instructions
Read the content of a B source file (.mch, .ref, .imp, etc.), C code (.c, .h), or Makefile from the workspace. Content is returned verbatim. For a .pmi file, a 'po_labels' list names the proof obligation each entry of its flat theories (ProofState, MethodList, PassList) belongs to; those entries carry no operation name of their own, so do not try to infer it from their position.
Input Schema
| Name | Required | Description | Default |
|---|---|---|---|
| file_path | Yes | Relative path from workspace root to the file |