Skip to content

unsoundness after external function call

ID0002315: This issue was created automatically from Mantis Issue 2315. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002315 Frama-C Plug-in > Eva public 2017-07-01 2017-07-03
Reporter maxime Assigned To yakobowski Resolution no change required
Priority high Severity block Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C 15-Phosphorus Target Version - Fixed in Version -

Description :

Hi everyone,

Frama-C is unsound after an external function call. See the attached file.

Running frama-c -val unsound.c gives me: [value] Called Frama_C_show_each_r({1})

This is wrong. The call to the external function f can update **x, and so *y can be anything.

At the call to f(x), I think you should grab all the base addresses that are reachable by the arguments and set them to TOP.

Steps To Reproduce :

frama-c -val unsound.c

Attachments

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information