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 209
    • Issues 209
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #2572

Closed
Open
Created Sep 10, 2021 by Andreas Werner@Werner2005

[WP] Lange Projekt course Stack Overflow in WP Plugin since 23.0

Hi for some time I Analyse a big Embedded Software Projekt for my Dissertation Project, the project has over 3000 LOCs. Until Version 23.0 we have a Stack Overflow Error in the WP Plugin. The Proof is currently Work-in-Progress.

Steps to reproduce the issue

I am unable to reproduce the bug in a small Projekt, to verify the Projekt you can use the Offizial docker container. To reproduce the bug you can clone the whole Projekt:

Small Script to clone the whole Projekt:

git clone https://gitlab.cs.hs-rm.de/CaroloCup/carolocupFirmware.git --recurse-submodules
cd carolocupFirmware
git remote add diss https://gitlab.cs.hs-rm.de/projekte_werner/carolocupFirmware.git
git fetch
git pull diss master
git submodule update
make carFramaC_defconfig # Init Config
make silentoldconfig # Fix Error in Config
FRAMAC=1 make # Run Frama-C

Our CI Server run an Verifikation automatically, we use the Offizial docker container. We test the bug under differierend Version of Frama-C here the result:

  • Frama-C Version 22.0: https://gitlab.cs.hs-rm.de/projekte_werner/carolocupFirmware/-/jobs/20042
  • Frama-C Version 23.1: https://gitlab.cs.hs-rm.de/projekte_werner/carolocupFirmware/-/jobs/20043
  • Frama-C Version Dev: https://gitlab.cs.hs-rm.de/projekte_werner/carolocupFirmware/-/jobs/20044

On the Version 22.0 Frama-C run to completion, on the latest Release and on the latest dev build a Stack Overflow occurred on the same code.

Expected behaviour

Run without Stack Overflow link in Frama-C Version 22.0

Actual behaviour

Stack Overflow in Version 23, 23.1 and dev.

Contextual information

  • Frama-C installation mode: Offizial Docker Container
  • Frama-C version: 22.0, 23.0, 23.1, 23.1-dev
  • Plug-in used: WP, EVA, RTE
  • OS name: Docker
  • OS version: Docker

Additional information (optional)

I tried to increase the stack size with ulimit (Until 8GB) same result.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking