Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
    • Switch to GitLab Next
  • Sign in / Register
CPAchecker
CPAchecker
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 301
    • Issues 301
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 13
    • Merge Requests 13
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Operations
    • Operations
    • Incidents
    • Environments
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • SoSy-Lab
  • Software
  • CPAcheckerCPAchecker
  • Issues
  • #580

Closed
Open
Opened Apr 18, 2019 by Evgeny Novikov@enovikovReporter

BAM (LDV BAM) performs unsound analysis

For cil.i with: scripts/cpa.sh -setprop parser.readLineDirectives=true -setprop counterexample.export.extendedWitnessFile=witness.%d.graphml -setprop counterexample.export.exportExtendedWitness=true -setprop counterexample.export.compressWitness=false -setprop cpa.arg.witness.exportSourcecode=true -setprop cpa.arg.witness.removeInsufficientEdges=false -heap 2400m -ldv-bam -setprop analysis.machineModel=LINUX64 -setprop coverage.file=coverage.info -stats -spec test/programs/benchmarks/properties/unreach-call.prp cil.i

there is true although, say, with -predicateAnalysis-bam-rec and -valueAnalysis-bam-rec there is false as expected.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: sosy-lab/software/cpachecker#580