Incompatibility between -inout-callwise and failing built-ins.
ID0001637: This issue was created automatically from Mantis Issue 1637. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001637 | Frama-C | Plug-in > Eva | public | 2014-01-30 | 2014-02-06 |
| Reporter | pascal | Assigned To | yakobowski | Resolution | won't fix |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | - |
Description :
The test below, called with the corresponding commandline, causes a crash.
$ cat tests/misc/outside_builtin_callwise.i /* run.config OPT: -inout-callwise -val-builtin strlen:Frama_C_strlen -val t.c */
int strlen () { return 0; }
int main () { strlen(); // note that we pass the wrong number of arguments, // causing Db.Value.Outside_builtin_possibilities to be raised. }
The causes appears to be that Value tells Inout that strlen is the sort of function that is analyzed as built-in and that inout should analyze from specs instead of code, although the built-in failed and strlen() was actually analyzed from code.
If this diagnostic is correctish, a solution might be for Value to pass a boolean to registered hooks instead of having them call a function !Db.Value.use_spec_instead_of_definition that does not know the answer. This could be solved with a change of API on the side of Value.
Crash:
[kernel] Current source was: tests/misc/outside_builtin_callwise.i:12 The full backtrace is: Raised at file "pervasives.ml", line 20, characters 22-33 Called from file "src/inout/operational_inputs.ml", line 576, characters 31-56 Called from file "src/inout/operational_inputs.ml", line 327, characters 30-47 Called from file "src/inout/operational_inputs.ml", line 325, characters 15-939 Called from file "src/inout/operational_inputs.ml", line 380, characters 34-59 Called from file "cil/src/ext/dataflows.ml", line 310, characters 12-42 Called from file "cil/src/ext/dataflows.ml", line 318, characters 19-30 Called from file "cil/src/ext/dataflows.ml", line 319, characters 5-14 Called from unknown location Called from unknown location Called from unknown location Called from file "src/inout/operational_inputs.ml", line 600, characters 16-69 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/value/eval_slevel.ml", line 198, characters 5-326 Called from file "src/value/eval_funs.ml", line 78, characters 2-27 Called from file "src/value/eval_funs.ml", line 307, characters 8-61 Called from file "src/value/eval_funs.ml", line 380, characters 10-110 Called from file "src/value/eval_funs.ml", line 659, characters 11-40 Re-raised at file "src/value/eval_funs.ml", line 678, characters 47-50 Called from file "src/project/state_builder.ml", line 841, characters 9-13 Re-raised at file "src/project/state_builder.ml", line 849, characters 15-18 Called from file "src/value/register.ml", line 83, characters 4-24 Called from file "queue.ml", line 134, characters 6-20 Called from file "src/kernel/boot.ml", line 37, characters 4-20 Called from file "src/kernel/cmdline.ml", line 735, characters 2-9 Called from file "src/kernel/cmdline.ml", line 214, characters 4-8
Unexpected error (Failure("hd")).
Please report as 'crash' at http://bts.frama-c.com/.
Your Frama-C version is Fluorine-20130601+dev.
Note that a version and a backtrace alone often do not contain enough
information to understand the bug. Guidelines for reporting bugs are at:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:bug_reporting_guidelines