[WP] Frama-C Vanadium crashes when calling RTE through WP on complicated or abstract structures
I've run into some trouble trying to parse and verify C code with complicated data structures.
Please note that I've also been able to reproduce the same error with more complex structures, but the following example only features an abstract data structure so as to keep it as minimal as (probably) possible.
Steps to reproduce the issue
Running Frama-C on the following code using the -wp-rte
option:
#include <stdint.h>
#include <string.h>
typedef struct _TEST_STRUCT BLOB;
int test_fun(int alg, uint8_t * key, size_t keySize, const char *label)
{
size_t lsize = strlen(label) + 1; //crashes frama-c if uncommented
BLOB *context;
int r = update(context);
return 0;
}
/*frama-c code.c -wp -wp-rte*/
Expected behaviour
Frama-C Vanadium parsing the code without any issue, and having WP call the RTE plugin, much like Frama-C Titanium.
Actual behaviour
Vanadium crashes when the "strlen" line is uncommented, returning the following error:
Uncaught exception:
Current source was: frama_tests/crypto_crash/crypto_crash.c:7
The full backtrace is:
Raised at file "src/kernel_services/plugin_entry_points/log.ml" (inlined), line 546, characters 24-31
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 1115, characters 17-55
Called from file "src/kernel_services/plugin_entry_points/log.ml", line 539, characters 9-23
Re-raised at file "src/kernel_services/plugin_entry_points/log.ml", line 542, characters 9-16
Called from file "src/kernel_services/ast_queries/cil_datatype.ml", line 2207, characters 34-294
Called from file "hashtbl.ml", line 512, characters 17-31
Called from file "src/libraries/project/state_builder.ml" (inlined), line 550, characters 17-34
Called from file "src/libraries/project/state_builder.ml", line 561, characters 16-24
Called from file "list.ml", line 164, characters 12-15
Called from file "src/plugins/wp/GuiSource.ml", line 111, characters 17-38
Called from file "src/plugins/gui/design.ml", line 728, characters 6-11
Frama-C aborted: internal error.
Reverting to previous state.
Check the Console tab for additional information.
Please report as 'crash' at https://git.frama-c.com/pub/frama-c/issues
Your Frama-C version is 23.0 (Vanadium).
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
https://git.frama-c.com/pub/frama-c/-/wikis/Guidelines-for-reporting-bugs
Contextual information
- Frama-C installation mode: Opam
- Frama-C version: 23.0 (Vanadium)
- Plug-in used: WP and RTE, tested both
-wp-rte
and-rte
options - OS name: Ubuntu
- OS version: 20.04.2 LTS
Additional information (optional)
In the more extensive code I'm actually working on, I've also noticed that:
- Frama-C Titanium run with the
-wp -rte
options seems to behave similarly as with the-wp -wp-rte
options, and does not crash in either of those cases. - Frama-C Vanadium run with the
-wp -rte
options does not crash, and seems to behave in a similar way to Frama-C Titanium using the previous options.
I'm actually not sure what the fundamental differences between calling the RTE plugin through the -rte
option and calling it through WP, but would it be possible to use -rte
as a temporary workaround ?
FYI @nkosmatov