Skip to content
GitLab
Projects Groups Topics 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
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • 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
  • #1764

Bug in slicing -- required C-statements getting knocked off from sliced code

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


Id Project Category View Due Date Updated
ID0000709 Frama-C Plug-in > slicing public 2011-02-08 2014-02-12
Reporter tukarammuske Assigned To Anne Resolution fixed
Priority normal Severity major Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Boron-20100401 Target Version - Fixed in Version Frama-C Nitrogen-20111001

Description :

The frama-c is used for slicing of the attached testcase. The required C-statements, nondets of var1 and var2 (line 54 & 55, function inputsOf_testcase_func) are getting removed from sliced code. Actually they should not. Looks like theres bug in the frama-c slicing.

Also, it is observed that if any one of the block of code ( three blocks are mentioned in the testcase with comment Block-1,2 or 3) is deleted, the required nondets of var1 and var2 are seen in the sliced code (that is slicing is done correctly!!!)

Additional Information :

The command used to run frama-c is --

frama-c -slice-print -no-unicode -slice-pragma func testcase.c

The required details like problem, the blocks affecting the slicing, the knocked off c statements are described with comments in the attached test case.

Attachments

  • testcase.c
  • Snapshot_2011-02-08_11-31-04
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking