ptest doesn't abort tests for which the command is incorrect
ID0002054: This issue was created automatically from Mantis Issue 2054. Further discussion may take place here.
|Product Version||Frama-C GIT, precise the release id||Target Version||-||Fixed in Version||-|
ptest has the following behavior when the command used to invoke frama-c is incorrect. First, the command is executed and the error reported by the shell. ptest continues using a previously generated output for the test. If the previous output was correct, it concludes that all tests passed.
When the command is put directly in the test file, tests update may introduce errors in this command line. It should be reported that the test does not pass due to incorrect command provided.