frama-c -wp - Error
When calling the Frama-C tool with option -wp, a series of faults is generated and the proof is not done: The compile command is wrong. It should invoke 'frama-c -wp' instead of c++ (see warning line 5 below).
_id: "60ae471a862de1005567f0fc" tool: "Frama-C" nature of report: "Proof report" start running time: "2021-05-26T13:03:22.000Z" end running time: "2021-05-26T13:03:22.000Z" messages: 0: "[FileSystem] Creating temporary root directory" 1: "[FileSystem] Created temporary root Directory '/tmp/pkm-ayJXcJ'" 2: "[FileSystem] Creating Directory '/tmp/pkm-ayJXcJ/src/java/main/com/devonfw/application/mtsj/usermanagement/service/api/rest'" 3: "[FileSystem] Creating Directory '/tmp/pkm-ayJXcJ'" 4: "[FileSystem] Created Directory '/tmp/pkm-ayJXcJ'" 5: "[FileSystem] Writing File '/tmp/pkm-ayJXcJ/examples_vector2.c' (utf-8 encoding)" 6: "[FileSystem] Wrote File '/tmp/pkm-ayJXcJ/examples_vector2.c'" 7: "[FileSystem] Created Directory '/tmp/pkm-ayJXcJ/src/java/main/com/devonfw/application/mtsj/usermanagement/service/api/rest'" 8: "[FileSystem] Writing File '/tmp/pkm-ayJXcJ/src/java/main/com/devonfw/application/mtsj/usermanagement/service/api/rest/UsermanagementRestService.java' (utf-8 encoding)" 9: "[FileSystem] Wrote File '/tmp/pkm-ayJXcJ/src/java/main/com/devonfw/application/mtsj/usermanagement/service/api/rest/UsermanagementRestService.java'" 10: "[FileSystem] Creating Directory '/tmp/pkm-ayJXcJ'" 11: "[FileSystem] Created Directory '/tmp/pkm-ayJXcJ'" 12: "[FileSystem] Writing File '/tmp/pkm-ayJXcJ/compile_commands.json' (utf8 encoding)" 13: "[FileSystem] Wrote File '/tmp/pkm-ayJXcJ/compile_commands.json'" 14: "Running 'frama-c' '-print-share-path'" 15: "Frama-C share path is '/pkm-api/.opam/4.08.1/share/frama-c'" 16: "[FileSystem] Deleting root Directory '/tmp/pkm-ayJXcJ'" 17: "[FileSystem] Deleted root Directory '/tmp/pkm-ayJXcJ'" 18: "putting a Log document" warnings: 0: "compile command for 'examples_vector2.c' not found" 1: "defaulting to {" 2: " "directory": "/tmp/pkm-ayJXcJ"," 3: " "file": "examples_vector2.c"," 4: " "arguments": [" 5: " "/usr/bin/c++"," 6: " "-I."" 7: " ]" 8: "} as compile command" status: false errors: 0: "{"name":"TypeError","message":"Cannot read property 'join' of undefined"}" type: "Log"