GitLab

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