Skip to content

GitLab

  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 204
    • Issues 204
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #1815
Closed
Open
Created Jan 30, 2014 by Pascal Cuoq@pascal

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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking