GitLab

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